Система Гильберта - 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 комбинаторной логики с оператором приложения. Тогда доказательства в системе Гильберта соответствуют комбинаторным членам комбинаторной логики. См. Также переписку Карри – Ховарда .

Смотрите также

Примечания

  1. ^ a b Máté & Ruzsa 1997: 129
  2. ^ А. Тарский, Логика, семантика, метаматематика, Оксфорд, 1956

использованная литература

  • Карри, 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.

внешние ссылки