Система Гильберта - Hilbert system
- В математической физике , Гильберт система редко используется термин для физической системы , описываемого C * -алгебра .
В логике , особенно математическая логика , система Гильберта , которую иногда называют Гильберт исчисление , Гильберта-стиль дедуктивная система или система Гильберта-Аккермана , представляет собой тип системы формального вычета связано с Фреге и Давида Гильберта . Эти дедуктивные системы чаще всего изучаются для логики первого порядка , но представляют интерес и для других логик.
Большинство вариантов систем Гильберта используют характерную тактику в том, как они уравновешивают компромисс между логическими аксиомами и правилами вывода . Системы Гильберта можно охарактеризовать выбором большого количества схем логических аксиом и небольшого набора правил вывода . Системы естественной дедукции придерживаются противоположной линии, включая множество правил дедукции, но очень мало схем аксиом или их отсутствие. Наиболее часто изучаемые системы Гильберта имеют либо только одно правило вывода - modus ponens для логики высказываний, либо два - с обобщением , также для обработки логики предикатов , - и несколько бесконечных схем аксиом. Гильберт система для пропозициональных модальных логик , иногда называемые системами Гильберта-Льюис , как правило , axiomatised с двумя дополнительными правилами, в правиле усиления и равномерной замена правила.
Характерной чертой многих вариантов систем Гильберта является то, что контекст не изменяется ни в одном из их правил вывода, в то время как как естественный вывод, так и исчисление секвенций содержат некоторые правила, изменяющие контекст. Таким образом, если кого-то интересует только выводимость тавтологий , а не гипотетические суждения, то можно формализовать систему Гильберта таким образом, чтобы ее правила вывода содержали только суждения довольно простой формы. То же самое нельзя сделать с двумя другими системами дедукции: поскольку контекст изменяется в некоторых из их правил умозаключений, они не могут быть формализованы так, чтобы можно было избежать гипотетических суждений - даже если мы хотим использовать их только для доказательства выводимости тавтологий. .
Формальные вычеты
В системе дедукции в стиле Гильберта формальный вывод - это конечная последовательность формул, в которой каждая формула является либо аксиомой, либо получена из предыдущих формул с помощью правила вывода. Эти формальные выводы предназначены для отражения доказательств на естественном языке, хотя они гораздо более подробны.
Предположим , это набор формул, рассматриваемых как гипотезы . Например, это может быть набор аксиом теории групп или теории множеств . Обозначение означает, что существует дедукция, которая заканчивается использованием в качестве аксиом только логических аксиом и элементов . Таким образом, неформально означает, что это доказуемо, предполагая, что все формулы в .
Системы вывода в гильбертовом стиле характеризуются использованием многочисленных схем логических аксиом . Схема аксиом - это бесконечный набор аксиом, полученный путем подстановки всех формул некоторой формы в определенный образец. Набор логических аксиом включает не только аксиомы, порожденные этим шаблоном, но также любое обобщение одной из этих аксиом. Обобщение формулы получается путем добавления в формулу нуля или нескольких универсальных кванторов; например , это обобщение .
Логические аксиомы
Существует несколько вариантов аксиоматизации логики предикатов, поскольку для любой логики существует свобода выбора аксиом и правил, характеризующих эту логику. Мы описываем здесь систему Гильберта с девятью аксиомами и просто правилом modus ponens, которое мы называем аксиоматизацией одного правила и которое описывает классическую эквациональную логику. Мы имеем дело с минимальным языком для этой логики, где формулы используют только связки и и только квантор . Позже мы покажем, как можно расширить систему, включив в нее дополнительные логические связки, такие как и , без расширения класса выводимых формул.
Первые четыре схемы логических аксиом позволяют (вместе с modus ponens) манипулировать логическими связками.
- P1.
- P2.
- P3.
- P4.
Аксиома P1 избыточна, как следует из P3, P2 и modus ponens (см. Доказательство ). Эти аксиомы описывают классическую логику высказываний ; без аксиомы P4 мы получаем позитивную импликационную логику . Минимальная логика достигается либо путем добавления аксиомы P4m, либо путем определения as .
- P4m.
Интуиционистская логика достигается добавлением аксиом P4i и P5i к позитивной импликационной логике или добавлением аксиомы P5i к минимальной логике. И P4i, и P5i являются теоремами классической логики высказываний.
- P4i.
- P5i.
Обратите внимание, что это схемы аксиом, которые представляют бесконечно много конкретных примеров аксиом. Например, P1 может представлять конкретный экземпляр аксиомы или может представлять : это место, где может быть размещена любая формула. Такая переменная, которая находится в пределах формул, называется «схематической переменной».
С помощью второго правила равномерной подстановки (US) мы можем преобразовать каждую из этих схем аксиом в единую аксиому, заменяя каждую схематическую переменную некоторой пропозициональной переменной, которая не упоминается ни в одной аксиоме, чтобы получить то, что мы называем аксиоматизацией подстановки. Обе формализации имеют переменные, но там, где аксиоматизация с одним правилом имеет схематические переменные, которые находятся за пределами языка логики, аксиоматизация подстановки использует пропозициональные переменные, которые выполняют ту же работу, выражая идею переменной, переходящей в формулы с правилом, использующим подстановку.
- НАС. Позвольте быть формулой с одним или несколькими экземплярами пропозициональной переменной , и пусть будет другой формулой. Потом из , сделаем .
Следующие три схемы логических аксиом предоставляют способы добавления, изменения и удаления универсальных кванторов.
- Q5. где t можно заменить на x в
- Q6.
- Q7. где x не свободен .
Эти три дополнительных правила расширяют систему высказываний, чтобы аксиоматизировать классическую логику предикатов . Точно так же эти три правила расширяют систему интуиционистской логики высказываний (с P1-3, P4i и P5i) до интуиционистской логики предикатов .
Универсальной количественной оценке часто дается альтернативная аксиоматизация с использованием дополнительного правила обобщения (см. Раздел о метатеоремах), и в этом случае правила Q6 и Q7 являются избыточными.
Окончательные схемы аксиом требуются для работы с формулами, содержащими символ равенства.
- I8. для каждой переменной x .
- I9.
Консервативные расширения
Обычно в систему дедукции в стиле Гильберта включаются только аксиомы импликации и отрицания. Учитывая эти аксиомы, можно сформировать консервативные расширения этого теорема дедукции , которые позволяют использовать дополнительные связки. Эти расширения называются консервативными, потому что если формула φ, включающая новые связки, переписывается как логически эквивалентная формула θ, включающая только отрицание, импликацию и универсальную квантификацию, то φ выводима в расширенной системе тогда и только тогда, когда θ выводима в исходной системе. . При полном расширении система в стиле Гильберта будет больше напоминать систему естественной дедукции .
Экзистенциальная количественная оценка
- Вступление
- Устранение
- где не свободная переменная из .
Конъюнкция и дизъюнкция
- Введение и устранение соединения
- вступление:
- осталось исключение:
- право исключения:
- Введение и устранение дизъюнкции
- Введение осталось:
- вводное право:
- устранение:
Метатеоремы
Поскольку в системах в стиле Гильберта очень мало правил дедукции, принято доказывать метатеоремы, которые показывают, что дополнительные правила дедукции не добавляют дедуктивной силы в том смысле, что дедукция с использованием новых правил дедукции может быть преобразована в дедукцию с использованием только исходной дедукции. правила.
Вот некоторые общие метатеоремы этой формы:
- Теорема дедукции : тогда и только тогда, когда .
- тогда и только тогда, когда и .
- Противопоставление: Если, то .
- Обобщение : If и x не встречается в любой формуле then .
Некоторые полезные теоремы и их доказательства
Ниже приведены несколько теорем в логике высказываний, а также их доказательства (или ссылки на эти доказательства в других статьях). Заметим, что, поскольку само (P1) может быть доказано с использованием других аксиом, на самом деле (P2), (P3) и (P4) достаточно для доказательства всех этих теорем.
- (HS1) - Гипотетический силлогизм , см. Доказательство .
- (L1) - доказательство:
- (1) (экземпляр (P3))
- (2) (экземпляр (P1))
- (3) (из (2) и (1) по modus ponens )
- (4) (экземпляр (HS1))
- (5) (из (3) и (4) по modus ponens)
- (6) (пример (P2))
- (7) (из (6) и (5) по modus ponens)
Следующие две теоремы вместе известны как двойное отрицание :
- (DN1)
- (DN2)
- Смотрите доказательства .
- (L2) - для этого доказательства мы используем метод метатеоремы гипотетического силлогизма как сокращение для нескольких шагов доказательства:
- (1) (экземпляр (P3))
- (2) (экземпляр (HS1))
- (3) (из (1) и (2) с использованием гипотетической метатеоремы силлогизма)
- (4) (пример (P3))
- (5) (из (3) и (4) с использованием modus ponens)
- (6) (пример (P2))
- (7) (пример (P2))
- (8) (из (6) и (7) с использованием modus ponens)
- (9) (из (8) и (5) с использованием modus ponens)
- (HS2) - альтернативная форма гипотетического силлогизма . доказательство:
- (1) (экземпляр (HS1))
- (2) (экземпляр (L2))
- (3) (из (1) и (2) по modus ponens)
- (TR1) - Транспонирование, см. Доказательство (другое направление транспонирования - (P4)).
- (TR2) - другая форма транспозиции; доказательство:
- (1) (экземпляр (TR1))
- (2) (экземпляр (DN1))
- (3) (экземпляр (HS1))
- (4) (из (2) и (3) по modus ponens)
- (5) (из (1) и (4) с использованием гипотетической метатеоремы силлогизма)
- (L3) - доказательство:
- (1) (пример (P2))
- (2) (экземпляр (P4))
- (3) (из (1) и (2) с использованием гипотетической метатеоремы силлогизма)
- (4) (пример (P3))
- (5) (из (3) и (4) с использованием режимов ponens)
- (6) (пример (P4))
- (7) (из (5) и (6) с использованием гипотетической метатеоремы силлогизма)
- (8) (пример (P1))
- (9) (пример (L1))
- (10) (из (8) и (9) с использованием мод ponens)
- (11) (из (7) и (10) с использованием гипотетической метатеоремы силлогизма)
Альтернативные аксиоматизации
Приведенная выше аксиома 3 принадлежит Лукасевичу . Исходная система Фреге имела аксиомы P2 и P3, но четыре других аксиомы вместо аксиомы P4 (см . Исчисление высказываний Фреге ). Рассел и Уайтхед также предложили систему с пятью пропозициональными аксиомами.
Дальнейшие связи
Аксиомы P1, P2 и P3 с правилом дедукции modus ponens (формализация интуиционистской логики высказываний ) соответствуют комбинаторам базовых комбинаторов I , K и S комбинаторной логики с оператором приложения. Тогда доказательства в системе Гильберта соответствуют комбинаторным членам комбинаторной логики. См. Также переписку Карри – Ховарда .
Смотрите также
Примечания
использованная литература
- Карри, Haskell B .; Роберт Фейс (1958). Комбинаторная логика. Я . 1 . Амстердам: Северная Голландия.
- Монк, Дж. Дональд (1976). Математическая логика . Тексты для выпускников по математике. Берлин, Нью-Йорк: Springer-Verlag . ISBN 978-0-387-90170-1.CS1 maint: postscript ( ссылка )
- Ружа, Имре; Мате, Андраш (1997). Bevezetés - современная логика (на венгерском). Будапешт: Осирис Киадо.
- Тарский, Альфред (1990). Bizonyítás és igazság (на венгерском языке). Будапешт: гондолат.Это венгерский перевод избранных работ Альфреда Тарского по семантической теории истины .
- Дэвид Гильберт (1927) «Основы математики», переведенный Стефаном Бауэр-Менглербергом и Дагфинном Фёллесдалом (стр. 464–479). в:
- ван Хейеноорт, Жан (1967). От Фреге до Гёделя: Справочник по математической логике, 1879–1931 гг. (3-е издание, изд. 1976 г.). Кембридж, Массачусетс: Издательство Гарвардского университета. ISBN 0-674-32449-8.
- В работе Гильберта 1927 года, основанной на лекции по «основам» более ранней 1925 года (стр. 367–392), представлены его 17 аксиом - аксиомы импликации №1-4, аксиомы о & и V №5-10, аксиомы отрицания №11- 12, его логическая ε-аксиома № 13, аксиомы равенства № 14-15 и аксиомы числа № 16-17 - вместе с другими необходимыми элементами его формалистской «теории доказательства» - например, аксиомами индукции, аксиомами рекурсии, так далее; он также предлагает энергичную защиту от интуиции Л. Дж. Брауэра. Также см. Комментарии и опровержение Германа Вейля (1927) (стр. 480–484), приложение Пола Берне (1927) к лекции Гильберта (стр. 485–489) и ответ Люитцена Эгбертуса Яна Брауэра (1927) (стр. 490–495)
-
Клини, Стивен Коул (1952). Введение в метаматематику (10-е оттиск с исправлениями 1971 г.). Амстердам, штат Нью-Йорк: Издательская компания Северной Голландии. ISBN 0-7204-2103-9.
- См., В частности, главу IV «Формальная система» (стр. 69–85), в которой Клини представляет подглавы §16 Формальные символы, §17 правила формирования, §18 Свободные и связанные переменные (включая подстановку), §19 правила преобразования (например, modus ponens) - и из них он представляет 21 "постулат" - 18 аксиом и 3 отношения "непосредственного следствия", разделенных следующим образом: постулаты для исчисления предложений № 1-8, Дополнительные постулаты для исчисления предикатов № 9-12 и Дополнительные постулаты для исчисления предикатов № 9-12. теория чисел # 13-21.
внешние ссылки
- Гайфман, Хаим. "Дедуктивная система типа Гильберта для сентенциальной логики, полноты и компактности" (pdf) .
- Фармер, WM "Логика высказываний" (pdf) .Он описывает (среди прочего) часть системы дедукции в стиле Гильберта (ограниченную исчислением высказываний ).