Список систем Гильберта

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

Классические системы исчисления высказываний

Классическое исчисление высказываний является стандартной логикой высказываний. Ее предполагаемая семантика бивалентна , а ее основное свойство состоит в том, что она является строго полной , иначе говоря, всякий раз, когда формула семантически следует из набора посылок, она также следует из этого набора синтаксически. Было сформулировано множество различных эквивалентных полных систем аксиом. Они отличаются выбором используемых базовых связок , которые во всех случаях должны быть функционально полными (т. е. способны выражать композицией все n -арные таблицы истинности ), и точным полным выбором аксиом по выбранному базису связок.

Импликация и отрицание

В формулировках здесь используются импликация и отрицание. $\{\to ,\neg \}$ как функционально полный набор основных связок. Каждая логическая система требует хотя бы одного ненулевого правила вывода . Классическое исчисление высказываний обычно использует правило modus ponens :

${\frac {A,A\to B}{B}}.$

Мы предполагаем, что это правило включено во все приведенные ниже системы, если не указано иное.

Фреге : Система аксиом

$A\to (B\to A)$

$(A\to (B\to C))\to ((A\to B)\to (A\to C))$

$(A\to (B\to C))\to (B\to (A\to C))$

$(A\to B)\to (\neg B\to \neg A)$

$\neg \neg A\to A$

$A\to \neg \neg A$

: Система аксиом Гильберта

$A\to (B\to A)$

$(A\to (B\to C))\to (B\to (A\to C))$

$(B\to C)\to ((A\to B)\to (A\to C))$

$A\to (\neg A\to B)$

$(A\to B)\to ((\neg A\to B)\to B)$

: Системы аксиом Лукасевича

• Первый:

  $(A\to B)\to ((B\to C)\to (A\to C))$

  $(\neg A\to A)\to A$

  $A\to (\neg A\to B)$

• Второй:

  $((A\to B)\to C)\to (\neg A\to C)$

  $((A\to B)\to C)\to (B\to C)$

  $(\neg A\to C)\to ((B\to C)\to ((A\to B)\to C))$

• Третий:

  $A\to (B\to A)$

  $(A\to (B\to C))\to ((A\to B)\to (A\to C))$

  $(\neg A\to \neg B)\to (B\to A)$

• Четвертое:

  $(A\to B)\to ((B\to C)\to (A\to C))$

  $A\to (\neg A\to B)$

  $(\neg A\to B)\to ((B\to A)\to A)$

Лукасевича и Тарского : Система аксиом

$[(A\to (B\to A))\to ([(\neg C\to (D\to \neg E))\to [(C\to (D\to F))\to ((E\to D)\to (E\to F))]]\to G)]\to (H\to G)$

Мередит Система аксиом :

$((((A\to B)\to (\neg C\to \neg D))\to C)\to E)\to ((E\to A)\to (D\to A))$

: Система аксиом Мендельсона

$A\to (B\to A)$

$(A\to (B\to C))\to ((A\to B)\to (A\to C))$

$(\neg A\to \neg B)\to ((\neg A\to B)\to A)$

Рассела : Система аксиом

$A\to (B\to A)$

$(A\to B)\to ((B\to C)\to (A\to C))$

$(A\to (B\to C))\to (B\to (A\to C))$

$\neg \neg A\to A$

$(A\to \neg A)\to \neg A$

$(A\to \neg B)\to (B\to \neg A)$

: Системы аксиом Собочинского

• Первый:

  $\neg A\to (A\to B)$

  $A\to (B\to (C\to A))$

  $(\neg A\to C)\to ((B\to C)\to ((A\to B)\to C))$

• Второй:

  $(A\to B)\to (\neg B\to (A\to C))$

  $A\to (B\to (C\to A))$

  $(\neg A\to B)\to ((A\to B)\to B)$

Импликация и ложность

Вместо отрицания классическую логику можно сформулировать и с использованием функционально полного набора $\{\to ,\bot \}$ из связок.

Тарского– Бернейса – Вайсберга Система аксиом :

$(A\to B)\to ((B\to C)\to (A\to C))$

$A\to (B\to A)$

$((A\to B)\to A)\to A$

$\bot \to A$

Чёрча Система аксиом :

$A\to (B\to A)$

$(A\to (B\to C))\to ((A\to B)\to (A\to C))$

$((A\to \bot )\to \bot )\to A$

Системы аксиом Мередит:

• Первый:

  $((((A\to B)\to (C\to \bot ))\to D)\to E)\to ((E\to A)\to (C\to A))$

• Второй:

  $((A\to B)\to ((\bot \to C)\to D))\to ((D\to A)\to (E\to (F\to A)))$

Отрицание и дизъюнкция

Вместо импликации классическую логику можно сформулировать и с использованием функционально полного набора $\{\neg ,\lor \}$ из связок. В этих формулировках используется следующее правило вывода;

${\frac {A,\neg A\lor B}{B}}.$

Система аксиом Рассела – Бернейса:

$\neg (\neg B\lor C)\lor (\neg (A\lor B)\lor (A\lor C))$

$\neg (A\lor B)\lor (B\lor A)$

$\neg A\lor (B\lor A)$

$\neg (A\lor A)\lor A$

Системы аксиом Мередит:

• Первый:

  $\neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg D\lor A)\lor (C\lor (E\lor A)))$

• Второй:

  $\neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg E\lor D)\lor (C\lor (A\lor D)))$

• Третий:

  $\neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg C\lor A)\lor (E\lor (D\lor A)))$

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

Союз и отрицание

Россер Дж. Баркли создал систему, основанную на соединении и отрицании. $\{\wedge ,\neg \}$, с modus ponens в качестве правила вывода. В своей книге он использовал импликацию, чтобы представить свои схемы аксиом. " $C\rightarrow D$"это сокращение от " $\neg (C\wedge \neg D)$":

• $A\rightarrow A\wedge A$
• $A\wedge B\rightarrow A$
• $\left(A\rightarrow B\right)\rightarrow \left(\neg \left(B\wedge C\right)\rightarrow \neg \left(C\wedge A\right)\right)$

Если не использовать аббревиатуру, получим схемы аксиом в следующем виде:

• $\neg (A\wedge \neg (A\wedge A))$
• $\neg ((A\wedge B)\wedge \neg A)$
• $\neg \left(\neg \left(A\wedge \neg B\right)\wedge \neg \neg \left(\neg \left(B\wedge C\right)\wedge \neg \neg \left(C\wedge A\right)\right)\right)$

Также вам станет доступен режим настройки:

• ${\frac {A,\neg \left(A\wedge \neg B\right)}{B}}$

Sheffer's stroke

Поскольку штрих Шеффера (также известный как оператор И-НЕ) функционально завершен , его можно использовать для создания полной формулировки исчисления высказываний. В формулировках NAND используется правило вывода, называемое Никода modus ponens :

${\frac {A,A\mid (B\mid C)}{C}}.$

Система аксиом Никода:

$(A\mid (B\mid C))\mid [(E\mid (E\mid E))\mid ((D\mid B)\mid [(A\mid D)\mid (A\mid D)])]$

Системы аксиом Лукасевича:

• Первый:

  $(A\mid (B\mid C))\mid [(D\mid (D\mid D))\mid ((D\mid B)\mid [(A\mid D)\mid (A\mid D)])]$

• Второй:

  $(A\mid (B\mid C))\mid [(A\mid (C\mid A))\mid ((D\mid B)\mid [(A\mid D)\mid (A\mid D)])]$

Система аксиом Вайсберга:

$(A\mid (B\mid C))\mid [((D\mid C)\mid [(A\mid D)\mid (A\mid D)])\mid (A\mid (A\mid B))]$

Аргоннские системы аксиом:

• Первый:

$(A\mid (B\mid C))\mid [(A\mid (B\mid C))\mid ((D\mid C)\mid [(C\mid D)\mid (A\mid D)])]$

• Второй:

$(A\mid (B\mid C))\mid [([(B\mid D)\mid (A\mid D)]\mid (D\mid B))\mid ((C\mid B)\mid A)]$

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

Импликативное исчисление высказываний

Импликационное исчисление высказываний — это фрагмент классического исчисления высказываний, который допускает только импликационную связку. Он не является функционально полным (поскольку ему не хватает способности выражать ложность и отрицание), но тем не менее синтаксически завершен . В приведенных ниже импликационных исчислениях в качестве правила вывода используется modus ponens.

Система аксиом Бернейса – Тарского:

$A\to (B\to A)$

$(A\to B)\to ((B\to C)\to (A\to C))$

$((A\to B)\to A)\to A$

Системы аксиом Лукасевича и Тарского:

• Первый:

  $[(A\to (B\to A))\to [([((C\to D)\to E)\to F]\to [(D\to F)\to (C\to F)])\to G]]\to G$

• Второй:

  $[(A\to B)\to ((C\to D)\to E)]\to ([F\to ((C\to D)\to E)]\to [(A\to F)\to (D\to E)])$

• Третий:

  $((A\to B)\to (C\to D))\to (E\to ((D\to A)\to (C\to A)))$

• Четвертое:

  $((A\to B)\to (C\to D))\to ((D\to A)\to (E\to (C\to A)))$

Система аксиом Лукасевича:

$((A\to B)\to C)\to ((C\to A)\to (D\to A))$

и

Интуиционистская логика является подсистемой классической логики. Обычно его формулируют с помощью $\{\to ,\land ,\lor ,\bot \}$ как совокупность (функционально законченных) основных связок. Он не является синтаксически полным, поскольку в нем отсутствует исключенное среднее A∨¬A или закон Пирса ((A→B)→A)→A, которые можно добавить, не делая логику противоречивой. В качестве правила вывода он имеет modus ponens и следующие аксиомы:

$A\to (B\to A)$

$(A\to (B\to C))\to ((A\to B)\to (A\to C))$

$(A\land B)\to A$

$(A\land B)\to B$

$A\to (B\to (A\land B))$

$A\to (A\lor B)$

$B\to (A\lor B)$

$(A\to C)\to ((B\to C)\to ((A\lor B)\to C))$

$\bot \to A$

Альтернативно, интуиционистская логика может быть аксиоматизирована с использованием $\{\to ,\land ,\lor ,\neg \}$ как набор основных связок, заменив последнюю аксиому на

$(A\to \neg A)\to \neg A$

$\neg A\to (A\to B)$

Промежуточные логики находятся между интуиционистской логикой и классической логикой. Вот несколько промежуточных логик:

• Логика Янкова (KC) представляет собой расширение интуиционистской логики, которую можно аксиоматизировать с помощью интуиционистской системы аксиом плюс аксиома

$\neg A\lor \neg \neg A.$

• Логику Гёделя – Даммета (LC) можно аксиоматизировать по сравнению с интуиционистской логикой, добавив аксиому

$(A\to B)\lor (B\to A).$

исчисление

Позитивное импликационное исчисление — это импликативный фрагмент интуиционистской логики. В приведенных ниже исчислениях в качестве правила вывода используется modus ponens.

Система аксиом Лукасевича:

$A\to (B\to A)$

$(A\to (B\to C))\to ((A\to B)\to (A\to C))$

Системы аксиом Мередит:

• Первый:

  $E\to ((A\to B)\to (((D\to A)\to (B\to C))\to (A\to C)))$

• Второй:

  $A\to (B\to A)$

  $(A\to B)\to ((A\to (B\to C))\to (A\to C))$

• Третий:

  $((A\to B)\to C)\to (D\to ((B\to (C\to E))\to (B\to E)))$

Системы аксиом Гильберта:

• Первый:

  $(A\to (A\to B))\to (A\to B)$

  $(B\to C)\to ((A\to B)\to (A\to C))$

  $(A\to (B\to C))\to (B\to (A\to C))$

  $A\to (B\to A)$

• Второй:

  $(A\to (A\to B))\to (A\to B)$

  $(A\to B)\to ((B\to C)\to (A\to C))$

  $A\to (B\to A)$

• Третий:

  $A\to A$

  $(A\to B)\to ((B\to C)\to (A\to C))$

  $(B\to C)\to ((A\to B)\to (A\to C))$

  $(A\to (A\to B))\to (A\to B)$

Позитивное исчисление высказываний

Позитивное исчисление высказываний - это фрагмент интуиционистской логики, использующий только (функционально неполные) связки. $\{\to ,\land ,\lor \}$. Оно может быть аксиоматизировано любым из вышеупомянутых исчислений для положительного импликационного исчисления вместе с аксиомами.

$(A\land B)\to A$

$(A\land B)\to B$

$A\to (B\to (A\land B))$

$A\to (A\lor B)$

$B\to (A\lor B)$

$(A\to C)\to ((B\to C)\to ((A\lor B)\to C))$

По желанию мы можем также включить соединительный элемент $\leftrightarrow$ и аксиомы

$(A\leftrightarrow B)\to (A\to B)$

$(A\leftrightarrow B)\to (B\to A)$

$(A\to B)\to ((B\to A)\to (A\leftrightarrow B))$

может Йоханссона Минимальная логика быть аксиоматизирована с помощью любой системы аксиом позитивного исчисления высказываний и расширения его языка с помощью нулевой связки. $\bot$, без каких-либо дополнительных схем аксиом. Альтернативно, это также может быть аксиоматизировано на языке $\{\to ,\land ,\lor ,\neg \}$ расширив положительное исчисление высказываний аксиомой

$(A\to \neg B)\to (B\to \neg A)$

или пара аксиом

$(A\to B)\to (\neg B\to \neg A)$

$A\to \neg \neg A$

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

$(A\to \neg B)\to (B\to \neg A)$

$\neg A\to (A\to B)$

или пара аксиом

$(A\to \neg A)\to \neg A$

$\neg A\to (A\to B)$

Классическая логика в языке $\{\to ,\land ,\lor ,\neg \}$ можно получить из положительного исчисления высказываний, добавив аксиому

$(\neg A\to \neg B)\to (B\to A)$

или пара аксиом

$(A\to \neg B)\to (B\to \neg A)$

$\neg \neg A\to A$

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

$\neg A\to (A\to B)$

$A\leftrightarrow \neg \neg A$

$\neg (A\lor B)\leftrightarrow (\neg A\land \neg B)$

$\neg (A\land B)\leftrightarrow (\neg A\lor \neg B)$

Заметим, что первая и третья аксиомы справедливы и в интуиционистской логике.

Эквивалентное исчисление

Эквивалентное исчисление - это подсистема классического исчисления высказываний, которая допускает только (функционально неполную) связку эквивалентности , обозначенную здесь как $\equiv$. Правило вывода, используемое в этих системах, следующее:

${\frac {A,A\equiv B}{B}}.$

Система аксиом Исеки:

$((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)$

$(A\equiv (B\equiv C))\equiv ((A\equiv B)\equiv C)$

Система аксиом Исеки – Араи:

$A\equiv A$

$(A\equiv B)\equiv (B\equiv A)$

$(A\equiv B)\equiv ((B\equiv C)\equiv (A\equiv C))$

системы аксиом Араи;

• Первый:

  $(A\equiv (B\equiv C))\equiv ((A\equiv B)\equiv C)$

  $((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)$

• Второй:

  $(A\equiv B)\equiv (B\equiv A)$

  $((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)$

Системы аксиом Лукасевича:

• Первый:

  $(A\equiv B)\equiv ((C\equiv B)\equiv (A\equiv C))$

• Второй:

  $(A\equiv B)\equiv ((A\equiv C)\equiv (C\equiv B))$

• Третий:

  $(A\equiv B)\equiv ((C\equiv A)\equiv (B\equiv C))$

Системы аксиом Мередит:

• Первый:

  $((A\equiv B)\equiv C)\equiv (B\equiv (C\equiv A))$

• Второй:

  $A\equiv ((B\equiv (A\equiv C))\equiv (C\equiv B))$

• Третий:

  $(A\equiv (B\equiv C))\equiv (C\equiv (A\equiv B))$

• Четвертое:

  $(A\equiv B)\equiv (C\equiv ((B\equiv C)\equiv A))$

• Пятое:

  $(A\equiv B)\equiv (C\equiv ((C\equiv B)\equiv A))$

• Шестое:

  $((A\equiv (B\equiv C))\equiv C)\equiv (B\equiv A)$

• Седьмой:

  $((A\equiv (B\equiv C))\equiv B)\equiv (C\equiv A)$

: Система аксиом Калмана

$A\equiv ((B\equiv (C\equiv A))\equiv (C\equiv B))$

: Системы аксиом Уинкера

• Первый:

  $A\equiv ((B\equiv C)\equiv ((A\equiv C)\equiv B))$

• Второй:

  $A\equiv ((B\equiv C)\equiv ((C\equiv A)\equiv B))$

Система аксиом XCB:

$A\equiv (((A\equiv B)\equiv (C\equiv B))\equiv C)$

См. также

• Паранепротиворечивая логика § Включено - список схем аксиом для паранепротиворечивой логики стиля Гильберта.