Система гильберта - Hilbert system

В математическая физика, Система гильберта - редко используемый термин для обозначения физической системы, описываемой C * -алгебра.

В логика, особенно математическая логика, а Система гильбертаиногда называют Исчисление Гильберта, Дедуктивная система Гильберта или Система Гильберта – Аккермана, это тип системы формальный вычет приписывается Готтлоб Фреге^[1] и Дэвид Гильберт. Эти дедуктивные системы чаще всего изучаются для логика первого порядка, но представляют интерес и для других логик.

Большинство вариантов систем Гильберта используют характерную тактику в том, как они уравновешивают компромисс между логические аксиомы и правила вывода.^[1] Системы Гильберта можно охарактеризовать выбором большого числа схемы логических аксиом и небольшой набор правила вывода. Системы естественный вычет примите противоположный курс, включая множество правил дедукции, но очень мало схем аксиом или их отсутствие. Наиболее часто изучаемые системы Гильберта имеют либо одно правило вывода: modus ponens, для пропозициональная логика - или два - с обобщение, обрабатывать логика предикатов, а также - и несколько бесконечных схем аксиом. Системы Гильберта для пропозициональной модальная логика иногда называют Системы Гильберта-Льюиса, обычно аксиоматизируются двумя дополнительными правилами: правило необходимости и равномерная замена правило.

Характерной чертой многих вариантов систем Гильберта является то, что контекст не изменяется ни в одном из их правил вывода, в то время как оба естественный вычет и последовательное исчисление содержат некоторые правила, изменяющие контекст. Таким образом, если вас интересует только выводимость тавтологии, никаких гипотетических суждений, то можно формализовать систему Гильберта таким образом, чтобы ее правила вывода содержали только суждения довольно простой формы. То же самое нельзя сделать с двумя другими системами вычетов:^{[нужна цитата ]} поскольку в некоторых из их правил вывода изменяется контекст, их нельзя формализовать так, чтобы можно было избежать гипотетических суждений - даже если мы хотим использовать их только для доказательства выводимости тавтологий.

Формальные вычеты

В дедуктивной системе Гильберта формальный вычет представляет собой конечную последовательность формул, в которой каждая формула является либо аксиомой, либо получена из предыдущих формул с помощью правила вывода. Эти формальные выводы предназначены для отражения доказательств на естественном языке, хотя они гораздо более подробны.

Предположим ${\displaystyle \Gamma }$ набор формул, рассматриваемых как гипотезы. Например, ${\displaystyle \Gamma }$ может быть набором аксиом для теория групп или теория множеств. Обозначение ${\displaystyle \Gamma \vdash \phi }$ означает, что есть вычет, который заканчивается на ${\displaystyle \phi }$ используя только как аксиомы логические аксиомы и элементы ${\displaystyle \Gamma }$. Таким образом, неофициально ${\displaystyle \Gamma \vdash \phi }$ Значит это ${\displaystyle \phi }$ доказуемо, если предположить, что все формулы в ${\displaystyle \Gamma }$.

Системы дедукции в гильбертовом стиле характеризуются использованием многочисленных схем логические аксиомы. An схема аксиом представляет собой бесконечный набор аксиом, получаемых путем подстановки всех формул той или иной формы в определенный образец. Набор логических аксиом включает не только аксиомы, порожденные этим шаблоном, но также любое обобщение одной из этих аксиом. Обобщение формулы получается путем добавления в формулу нуля или нескольких универсальных кванторов; Например ${\displaystyle \forall y(\forall xPxy\to Pty)}$ является обобщением ${\displaystyle \forall xPxy\to Pty}$.

Логические аксиомы

Существует несколько вариантов аксиоматизации логики предикатов, поскольку для любой логики существует свобода выбора аксиом и правил, характеризующих эту логику. Мы описываем здесь систему Гильберта с девятью аксиомами и просто правилом modus ponens, которое мы называем аксиоматизацией с одним правилом и которое описывает классическую эквациональную логику. Мы имеем дело с минимальным языком этой логики, где в формулах используются только связки ${\displaystyle \lnot }$ и ${\displaystyle \to }$ и только квантор ${\displaystyle \forall }$. Позже мы покажем, как можно расширить систему, включив в нее дополнительные логические связки, такие как ${\displaystyle \land }$ и ${\displaystyle \lor }$, не расширяя класс выводимых формул.

Первые четыре схемы логических аксиом позволяют (вместе с modus ponens) манипулировать логическими связками.

P1. ${\displaystyle \phi \to \phi }$

P2. ${\displaystyle \phi \to \left(\psi \to \phi \right)}$

P3. ${\displaystyle \left(\phi \to \left(\psi \rightarrow \xi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)}$

P4. ${\displaystyle \left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)}$

Аксиома P1 избыточна, как следует из P3, P2 и modus ponens (см. доказательство ). Эти аксиомы описывают классическая логика высказываний; без аксиомы P4 получаем положительная импликационная логика. Минимальная логика достигается либо добавлением аксиомы P4m, либо определением ${\displaystyle \lnot \phi }$ так как ${\displaystyle \phi \to \bot }$.

P4m. ${\displaystyle \left(\phi \to \psi \right)\to \left(\left(\phi \to \lnot \psi \right)\to \lnot \phi \right)}$

Интуиционистская логика достигается добавлением аксиом P4i и P5i к позитивной импликационной логике или добавлением аксиомы P5i к минимальной логике. И P4i, и P5i являются теоремами классической логики высказываний.

P4i. ${\displaystyle \left(\phi \to \lnot \phi \right)\to \lnot \phi }$

P5i. ${\displaystyle \lnot \phi \to \left(\phi \to \psi \right)}$

Обратите внимание, что это схемы аксиом, которые представляют бесконечно много конкретных примеров аксиом. Например, P1 может представлять конкретный экземпляр аксиомы ${\displaystyle p\to p}$, или он может представлять ${\displaystyle \left(p\to q\right)\to \left(p\to q\right)}$: the ${\displaystyle \phi }$ это место, где можно разместить любую формулу. Такая переменная, которая находится в пределах формулы, называется «схемной переменной».

Со вторым правилом равномерная замена (США), мы можем преобразовать каждую из этих схем аксиом в одну аксиому, заменив каждую схематическую переменную некоторой пропозициональной переменной, которая не упоминается ни в одной аксиоме, чтобы получить то, что мы называем аксиоматизацией подстановки. Обе формализации имеют переменные, но там, где аксиоматизация с одним правилом имеет схематические переменные, которые находятся за пределами языка логики, аксиоматизация подстановки использует пропозициональные переменные, которые выполняют ту же работу, выражая идею переменной, переходящей в формулы с правилом, использующим подстановку.

НАС. Позволять ${\displaystyle \phi (p)}$ быть формулой с одним или несколькими экземплярами пропозициональной переменной ${\displaystyle p}$, и разреши ${\displaystyle \psi }$ быть другой формулой. Тогда из ${\displaystyle \phi (p)}$, сделать вывод ${\displaystyle \phi (\psi )}$.^{[сомнительный ]}

Следующие три схемы логических аксиом предоставляют способы добавления, управления и удаления универсальных кванторов.

Q5. ${\displaystyle \forall x\left(\phi \right)\to \phi [x:=t]}$ где т может быть заменен на Икс в ${\displaystyle \,\!\phi }$

Q6. ${\displaystyle \forall x\left(\phi \to \psi \right)\to \left(\forall x\left(\phi \right)\to \forall x\left(\psi \right)\right)}$

Q7. ${\displaystyle \phi \to \forall x\left(\phi \right)}$ где Икс не бесплатно в ${\displaystyle \phi }$.

Эти три дополнительных правила расширяют систему высказываний до аксиоматизации. классическая логика предикатов. Точно так же эти три правила расширяют систему интуитивной логики высказываний (с P1-3, P4i и P5i) до интуиционистская логика предикатов.

Универсальной количественной оценке часто дается альтернативная аксиоматизация с использованием дополнительного правила обобщения (см. Раздел о метатеоремах), и в этом случае правила Q6 и Q7 являются избыточными.^{[сомнительный ]}

Окончательные схемы аксиом необходимы для работы с формулами, содержащими символ равенства.

I8. ${\displaystyle x=x}$ для каждой переменной Икс.

I9. ${\displaystyle \left(x=y\right)\to \left(\phi [z:=x]\to \phi [z:=y]\right)}$

Консервативные расширения

Обычно в систему дедукции в стиле Гильберта включаются только аксиомы импликации и отрицания. Учитывая эти аксиомы, можно сформировать консервативные расширения из теорема дедукции которые позволяют использовать дополнительные связки. Эти расширения называются консервативными, потому что если формулу φ, содержащую новые связки, переписать как логически эквивалентный формула θ, включающая только отрицание, импликацию и универсальную квантификацию, то φ выводима в расширенной системе тогда и только тогда, когда θ выводима в исходной системе. При полном расширении система гильбертова будет больше напоминать систему естественный вычет.

Экзистенциальная количественная оценка

• Введение

${\displaystyle \forall x(\phi \to \exists y(\phi [x:=y]))}$

• Устранение

${\displaystyle \forall x(\phi \to \psi )\to \exists x(\phi )\to \psi }$ где ${\displaystyle x}$ это не свободная переменная из ${\displaystyle \psi }$.

Конъюнкция и дизъюнкция

• Введение и устранение союзов

введение: ${\displaystyle \alpha \to \beta \to \alpha \land \beta }$

осталось исключение: ${\displaystyle \alpha \wedge \beta \to \alpha }$

право исключения: ${\displaystyle \alpha \wedge \beta \to \beta }$

• Введение и устранение дизъюнкции

Введение осталось: ${\displaystyle \alpha \to \alpha \vee \beta }$

вводное право: ${\displaystyle \beta \to \alpha \vee \beta }$

устранение: ${\displaystyle (\alpha \to \gamma )\to (\beta \to \gamma )\to \alpha \vee \beta \to \gamma }$

Метатеоремы

Поскольку системы гильбертова имеют очень мало правил дедукции, принято доказывать метатеоремы которые показывают, что дополнительные правила дедукции не добавляют дедуктивной силы в том смысле, что вычет с использованием новых правил вычета может быть преобразован в вычет с использованием только исходных правил вычета.

Некоторые распространенные метатеоремы этой формы:

• В теорема дедукции: ${\displaystyle \Gamma ;\phi \vdash \psi }$ если и только если ${\displaystyle \Gamma \vdash \phi \to \psi }$.
• ${\displaystyle \Gamma \vdash \phi \leftrightarrow \psi }$ если и только если ${\displaystyle \Gamma \vdash \phi \to \psi }$ и ${\displaystyle \Gamma \vdash \psi \to \phi }$.
• Противопоставление: Если ${\displaystyle \Gamma ;\phi \vdash \psi }$ тогда ${\displaystyle \Gamma ;\lnot \psi \vdash \lnot \phi }$.
• Обобщение: Если ${\displaystyle \Gamma \vdash \phi }$ и Икс не встречается свободно ни в одной формуле ${\displaystyle \Gamma }$ тогда ${\displaystyle \Gamma \vdash \forall x\phi }$.

Некоторые полезные теоремы и их доказательства

Ниже приведены несколько теорем в логике высказываний, а также их доказательства (или ссылки на эти доказательства в других статьях). Заметим, что, поскольку само (P1) может быть доказано с использованием других аксиом, на самом деле (P2), (P3) и (P4) достаточно для доказательства всех этих теорем.

(HS1) ${\displaystyle (q\to r)\to ((p\to q)\to (p\to r))}$ - Гипотетический силлогизм, увидеть доказательство.

(L1) ${\displaystyle p\to ((p\to q)\to q)}$ - доказательство:

(1) ${\displaystyle ((p\to q)\to (p\to q))\to (((p\to q)\to p)\to ((p\to q)\to q))}$ (экземпляр (P3))

(2) ${\displaystyle (p\to q)\to (p\to q)}$ (экземпляр (P1))

(3) ${\displaystyle ((p\to q)\to p)\to ((p\to q)\to q)}$ (из (2) и (1) по modus ponens )

(4) ${\displaystyle (((p\to q)\to p)\to ((p\to q)\to q))\to ((p\to ((p\to q)\to p))\to (p\to ((p\to q)\to q)))}$ (экземпляр (HS1))

(5) ${\displaystyle (p\to ((p\to q)\to p))\to (p\to ((p\to q)\to q))}$ (из (3) и (4) по modus ponens)

(6) ${\displaystyle p\to ((p\to q)\to p)}$ (пример (P2))

(7) ${\displaystyle p\to ((p\to q)\to q)}$ (из (6) и (5) по modus ponens)

Следующие две теоремы вместе известны как Двойное отрицание:

(DN1)${\displaystyle \neg \neg p\to p}$

(DN2) ${\displaystyle p\to \neg \neg p}$

Увидеть доказательства.

(L2) ${\displaystyle (p\to (q\to r))\to (q\to (p\to r))}$ - для этого доказательства мы используем метод гипотетический силлогизм, метатеорема как сокращение для нескольких шагов проверки:

(1) ${\displaystyle (p\to (q\to r))\to ((p\to q)\to (p\to r))}$ (экземпляр (P3))

(2) ${\displaystyle ((p\to q)\to (p\to r))\to ((q\to (p\to q))\to (q\to (p\to r)))}$ (экземпляр (HS1))

(3) ${\displaystyle (p\to (q\to r))\to ((q\to (p\to q))\to (q\to (p\to r)))}$ (из (1) и (2) с использованием гипотетической метатеоремы силлогизма)

(4) ${\displaystyle ((p\to (q\to r))\to ((q\to (p\to q))\to (q\to (p\to r))))\to (((p\to (q\to r))\to (q\to (p\to q)))\to ((p\to (q\to r))\to (q\to (p\to r))))}$ (экземпляр (P3))

(5) ${\displaystyle ((p\to (q\to r))\to (q\to (p\to q)))\to ((p\to (q\to r))\to (q\to (p\to r)))}$ (из (3) и (4) с использованием modus ponens)

(6) ${\displaystyle q\to (p\to q)}$ (пример (P2))

(7) ${\displaystyle (q\to (p\to q))\to ((p\to (q\to r))\to (q\to (p\to q)))}$ (пример (P2))

(8) ${\displaystyle (p\to (q\to r))\to (q\to (p\to q))}$ (из (6) и (7) с использованием modus ponens)

(9) ${\displaystyle (p\to (q\to r))\to (q\to (p\to r))}$ (из (8) и (5) с использованием modus ponens)

(HS2) ${\displaystyle (p\to q)\to ((q\to r)\to (p\to r))}$ - альтернативная форма гипотетический силлогизм. доказательство:

(1) ${\displaystyle (q\to r)\to ((p\to q)\to (p\to r))}$ (экземпляр (HS1))

(2) ${\displaystyle ((q\to r)\to ((p\to q)\to (p\to r)))\to ((p\to q)\to ((q\to r)\to (p\to r)))}$ (экземпляр (L2))

(3) ${\displaystyle (p\to q)\to ((q\to r)\to (p\to r))}$ (из (1) и (2) по modus ponens)

(TR1) ${\displaystyle (p\to q)\to (\neg q\to \neg p)}$ - Транспонирование, см. доказательство (другое направление транспонирования - (P4)).

(TR2) ${\displaystyle (\neg p\to q)\to (\neg q\to p)}$ - другая форма транспозиции; доказательство:

(1) ${\displaystyle (\neg p\to q)\to (\neg q\to \neg \neg p)}$ (экземпляр (TR1))

(2) ${\displaystyle \neg \neg p\to p}$ (экземпляр (DN1))

(3) ${\displaystyle (\neg \neg p\to p)\to ((\neg q\to \neg \neg p)\to (\neg q\to p))}$ (экземпляр (HS1))

(4) ${\displaystyle (\neg q\to \neg \neg p)\to (\neg q\to p)}$ (из (2) и (3) по modus ponens)

(5) ${\displaystyle (\neg p\to q)\to (\neg q\to p)}$ (из (1) и (4) с использованием гипотетической метатеоремы силлогизма)

(L3) ${\displaystyle (\neg p\to p)\to p}$ - доказательство:

(1) ${\displaystyle \neg p\to (\neg \neg (q\to q)\to \neg p)}$ (пример (P2))

(2) ${\displaystyle (\neg \neg (q\to q)\to \neg p)\to (p\to \neg (q\to q))}$ (экземпляр (P4))

(3) ${\displaystyle \neg p\to (p\to \neg (q\to q))}$ (из (1) и (2) с использованием гипотетической метатеоремы силлогизма)

(4) ${\displaystyle (\neg p\to (p\to \neg (q\to q)))\to ((\neg p\to p)\to (\neg p\to \neg (q\to q)))}$ (экземпляр (P3))

(5) ${\displaystyle (\neg p\to p)\to (\neg p\to \neg (q\to q))}$ (из (3) и (4) с использованием режимов ponens)

(6) ${\displaystyle (\neg p\to \neg (q\to q))\to ((q\to q)\to p)}$ (экземпляр (P4))

(7) ${\displaystyle (\neg p\to p)\to ((q\to q)\to p)}$ (из (5) и (6) с использованием гипотетической метатеоремы силлогизма)

(8) ${\displaystyle q\to q}$ (экземпляр (P1))

(9) ${\displaystyle (q\to q)\to (((q\to q)\to p)\to p)}$ (экземпляр (L1))

(10) ${\displaystyle ((q\to q)\to p)\to p}$ (из (8) и (9) с использованием режимов ponens)

(11) ${\displaystyle (\neg p\to p)\to p}$ (из (7) и (10) с использованием метатеоремы гипотетического силлогизма)

Альтернативные аксиоматизации

Дальнейшая информация: Список логических систем

Аксиома 3 выше приписывается Лукасевич.^[2] Оригинальная система Frege имел аксиомы P2 и P3, но четыре другие аксиомы вместо аксиомы P4 (см. Исчисление высказываний Фреге ).Рассел и Уайтхед также предложил систему с пятью пропозициональными аксиомами.

Дальнейшие связи

Аксиомы P1, P2 и P3 с правилом дедукции modus ponens (формализация интуиционистская логика высказываний ), соответствуют комбинаторная логика базовые комбинаторы я, K и S с оператором приложения. Доказательства в системе Гильберта соответствуют комбинаторным членам комбинаторной логики. Смотрите также Переписка Карри – Ховарда.

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

• Список систем Гильберта
• Естественный вычет

Заметки

1. Мате и Ружа 1997: 129
2. А. Тарский, Логика, семантика, метаматематика, Оксфорд, 1956.

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

• Карри, Haskell B .; Роберт Фейс (1958). Комбинаторная логика Vol. я. 1. Амстердам: Северная Голландия.
• Монк, Дж. Дональд (1976). Математическая логика. Тексты для выпускников по математике. Берлин, Нью-Йорк: Springer-Verlag. ISBN  978-0-387-90170-1.
• Ружа, Имре; Мате, Андраш (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 - вместе с другими необходимыми элементами его формалистской «теории доказательства», например аксиомы индукции, аксиомы рекурсии и др .; он также предлагает энергичную защиту от L.E.J. Интуиционизм Брауэра. Также см. Комментарии и опровержение Германа Вейля (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 и Дополнительные постулаты для теория чисел # 13-21.

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

• Гайфман, Хаим. "Дедуктивная система типа Гильберта для сентенциальной логики, полноты и компактности" (pdf).
• Фармер, В. М. "Логика высказываний" (pdf). Он описывает (среди прочего) часть системы дедукции в стиле Гильберта (ограниченная пропозициональное исчисление ).