Список аксиоматических систем в логике

Для проверки этой статьи нужны дополнительные цитаты . Помогите улучшить эту статью , добавив ссылки на надежные источники . Материалы без источников могут быть оспорены и удалены. Найти источники:  «Список аксиоматических систем в логике» – новости  · газеты  · книги  · ученый  · JSTOR ( сентябрь 2010 г. ) ( Узнайте, как и когда удалять это сообщение )

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

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

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

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

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

Система аксиом Фреге : ^[1]

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

${\displaystyle (A\to (B\to C))\to (B\to (A\to C))}$

${\displaystyle (A\to B)\to (\neg B\to \neg A)}$

${\displaystyle \neg \neg A\to A}$

${\displaystyle A\to \neg \neg A}$

Система аксиом Гильберта: [ ^1]

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to (B\to (A\to C))}$

${\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}$

${\displaystyle A\to (\neg A\to B)}$

${\displaystyle (A\to B)\to ((\neg A\to B)\to B)}$

Системы аксиом Лукасевича: [ ^1]

• Первый:

  ${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

  ${\displaystyle (\neg A\to A)\to A}$

  ${\displaystyle A\to (\neg A\to B)}$

• Второй:

  ${\displaystyle ((A\to B)\to C)\to (\neg A\to C)}$

  ${\displaystyle ((A\to B)\to C)\to (B\to C)}$

  ${\displaystyle (\neg A\to C)\to ((B\to C)\to ((A\to B)\to C))}$

• Третий:

  ${\displaystyle A\to (B\to A)}$

  ${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

  ${\displaystyle (\neg A\to \neg B)\to (B\to A)}$

Система аксиом Араи: ^[2]

${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

${\displaystyle A\to (\neg A\to B)}$

${\displaystyle (\neg A\to B)\to ((B\to A)\to A)}$

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

${\displaystyle [(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)}$

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

${\displaystyle ((((A\to B)\to (\neg C\to \neg D))\to C)\to E)\to ((E\to A)\to (D\to A))}$

Система аксиом Мендельсона: [ ^4]

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

${\displaystyle (\neg A\to \neg B)\to ((\neg A\to B)\to A)}$

Система аксиом Рассела : ^[1]

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

${\displaystyle (A\to (B\to C))\to (B\to (A\to C))}$

${\displaystyle \neg \neg A\to A}$

${\displaystyle (A\to \neg A)\to \neg A}$

${\displaystyle (A\to \neg B)\to (B\to \neg A)}$

Системы аксиом Собочинского: ^[1]

• Первый:

  ${\displaystyle \neg A\to (A\to B)}$

  ${\displaystyle A\to (B\to (C\to A))}$

  ${\displaystyle (\neg A\to C)\to ((B\to C)\to ((A\to B)\to C))}$

• Второй:

  ${\displaystyle (A\to B)\to (\neg B\to (A\to C))}$

  ${\displaystyle A\to (B\to (C\to A))}$

  ${\displaystyle (\neg A\to B)\to ((A\to B)\to B)}$

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

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

${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

${\displaystyle A\to (B\to A)}$

${\displaystyle ((A\to B)\to A)\to A}$

${\displaystyle \bot \to A}$

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

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

${\displaystyle ((A\to \bot )\to \bot )\to A}$

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

• Первый: ^{[5] [6] [7]}

  ${\displaystyle ((((A\to B)\to (C\to \bot ))\to D)\to E)\to ((E\to A)\to (C\to A))}$

• Второе: ^[5]

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

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

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

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

${\displaystyle \neg (\neg B\lor C)\lor (\neg (A\lor B)\lor (A\lor C))}$

${\displaystyle \neg (A\lor B)\lor (B\lor A)}$

${\displaystyle \neg A\lor (B\lor A)}$

${\displaystyle \neg (A\lor A)\lor A}$

Системы аксиом Мередита: ^[8]

• Первый:

  ${\displaystyle \neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg D\lor A)\lor (C\lor (E\lor A)))}$

• Второй:

  ${\displaystyle \neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg E\lor D)\lor (C\lor (A\lor D)))}$

• Третий:

  ${\displaystyle \neg (\neg (\neg A\lor B)\lor (C\lor (D\lor E)))\lor (\neg (\neg C\lor A)\lor (E\lor (D\lor A)))}$

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

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

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

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

• ${\displaystyle \neg (A\wedge \neg (A\wedge A))}$
• ${\displaystyle \neg ((A\wedge B)\wedge \neg A)}$
• ${\displaystyle \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)}$

Кроме того, modus ponens становится:

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

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

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

Система аксиом Никода: ^[5]

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

Системы аксиом Лукасевича: ^[5]

• Первый:

  ${\displaystyle (A\mid (B\mid C))\mid [(D\mid (D\mid D))\mid ((D\mid B)\mid [(A\mid D)\mid (A\mid D)])]}$

• Второй:

  ${\displaystyle (A\mid (B\mid C))\mid [(A\mid (C\mid A))\mid ((D\mid B)\mid [(A\mid D)\mid (A\mid D)])]}$

Система аксиом Вайсберга: ^[5]

${\displaystyle (A\mid (B\mid C))\mid [((D\mid C)\mid [(A\mid D)\mid (A\mid D)])\mid (A\mid (A\mid B))]}$

Системы аксиом Аргонна : ^[5]

• Первый:

${\displaystyle (A\mid (B\mid C))\mid [(A\mid (B\mid C))\mid ((D\mid C)\mid [(C\mid D)\mid (A\mid D)])]}$

• Второй:

${\displaystyle (A\mid (B\mid C))\mid [([(B\mid D)\mid (A\mid D)]\mid (D\mid B))\mid ((C\mid B)\mid A)]}$^[10]

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

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

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

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

${\displaystyle ((A\to B)\to A)\to A}$

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

• Первое: ^[11]

  ${\displaystyle [(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}$

• Второе: ^[11]

  ${\displaystyle [(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)])}$

• Третий:

  ${\displaystyle ((A\to B)\to (C\to D))\to (E\to ((D\to A)\to (C\to A)))}$

• Четвертое:

  ${\displaystyle ((A\to B)\to (C\to D))\to ((D\to A)\to (E\to (C\to A)))}$

Система аксиом Лукасевича: ^{[12] [11]}

${\displaystyle ((A\to B)\to C)\to ((C\to A)\to (D\to A))}$

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

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

${\displaystyle (A\land B)\to A}$

${\displaystyle (A\land B)\to B}$

${\displaystyle A\to (B\to (A\land B))}$

${\displaystyle A\to (A\lor B)}$

${\displaystyle B\to (A\lor B)}$

${\displaystyle (A\to C)\to ((B\to C)\to ((A\lor B)\to C))}$

${\displaystyle \bot \to A}$

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

${\displaystyle (A\to \neg A)\to \neg A}$

${\displaystyle \neg A\to (A\to B)}$

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

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

${\displaystyle \neg A\lor \neg \neg A.}$

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

${\displaystyle (A\to B)\lor (B\to A).}$

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

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

${\displaystyle A\to (B\to A)}$

${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

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

• Первый:

  ${\displaystyle E\to ((A\to B)\to (((D\to A)\to (B\to C))\to (A\to C)))}$

• Второй:

  ${\displaystyle A\to (B\to A)}$

  ${\displaystyle (A\to B)\to ((A\to (B\to C))\to (A\to C))}$

• Третий:

  ${\displaystyle ((A\to B)\to C)\to (D\to ((B\to (C\to E))\to (B\to E)))}$^[14]

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

• Первый:

  ${\displaystyle (A\to (A\to B))\to (A\to B)}$

  ${\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}$

  ${\displaystyle (A\to (B\to C))\to (B\to (A\to C))}$

  ${\displaystyle A\to (B\to A)}$

• Второй:

  ${\displaystyle (A\to (A\to B))\to (A\to B)}$

  ${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

  ${\displaystyle A\to (B\to A)}$

• Третий:

  ${\displaystyle A\to A}$

  ${\displaystyle (A\to B)\to ((B\to C)\to (A\to C))}$

  ${\displaystyle (B\to C)\to ((A\to B)\to (A\to C))}$

  ${\displaystyle (A\to (A\to B))\to (A\to B)}$

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

${\displaystyle (A\land B)\to A}$

${\displaystyle (A\land B)\to B}$

${\displaystyle A\to (B\to (A\land B))}$

${\displaystyle A\to (A\lor B)}$

${\displaystyle B\to (A\lor B)}$

${\displaystyle (A\to C)\to ((B\to C)\to ((A\lor B)\to C))}$

По желанию мы также можем включить связку и аксиомы.${\displaystyle \leftrightarrow }$

${\displaystyle (A\leftrightarrow B)\to (A\to B)}$

${\displaystyle (A\leftrightarrow B)\to (B\to A)}$

${\displaystyle (A\to B)\to ((B\to A)\to (A\leftrightarrow B))}$

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

${\displaystyle (A\to \neg B)\to (B\to \neg A)}$

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

${\displaystyle (A\to B)\to (\neg B\to \neg A)}$

${\displaystyle A\to \neg \neg A}$

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

${\displaystyle (A\to \neg B)\to (B\to \neg A)}$

${\displaystyle \neg A\to (A\to B)}$

или пара аксиом ^[15]

${\displaystyle (A\to \neg A)\to \neg A}$

${\displaystyle \neg A\to (A\to B)}$

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

${\displaystyle (\neg A\to \neg B)\to (B\to A)}$

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

${\displaystyle (A\to \neg B)\to (B\to \neg A)}$

${\displaystyle \neg \neg A\to A}$

Исчисление Фитча берет любую из систем аксиом для позитивного пропозиционального исчисления и добавляет аксиомы ^[15]

${\displaystyle \neg A\to (A\to B)}$

${\displaystyle A\leftrightarrow \neg \neg A}$

${\displaystyle \neg (A\lor B)\leftrightarrow (\neg A\land \neg B)}$

${\displaystyle \neg (A\land B)\leftrightarrow (\neg A\lor \neg B)}$

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

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

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

Система аксиом Исэки: ^[16]

${\displaystyle ((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)}$

${\displaystyle (A\equiv (B\equiv C))\equiv ((A\equiv B)\equiv C)}$

Система аксиом Исеки – Араи: ^[17]

${\displaystyle A\equiv A}$

${\displaystyle (A\equiv B)\equiv (B\equiv A)}$

${\displaystyle (A\equiv B)\equiv ((B\equiv C)\equiv (A\equiv C))}$

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

• Первый:

  ${\displaystyle (A\equiv (B\equiv C))\equiv ((A\equiv B)\equiv C)}$

  ${\displaystyle ((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)}$

• Второй:

  ${\displaystyle (A\equiv B)\equiv (B\equiv A)}$

  ${\displaystyle ((A\equiv C)\equiv (B\equiv A))\equiv (C\equiv B)}$

Системы аксиом Лукасевича: ^[18]

• Первый:

  ${\displaystyle (A\equiv B)\equiv ((C\equiv B)\equiv (A\equiv C))}$

• Второй:

  ${\displaystyle (A\equiv B)\equiv ((A\equiv C)\equiv (C\equiv B))}$

• Третий:

  ${\displaystyle (A\equiv B)\equiv ((C\equiv A)\equiv (B\equiv C))}$

Системы аксиом Мередита: ^[18]

• Первый:

  ${\displaystyle ((A\equiv B)\equiv C)\equiv (B\equiv (C\equiv A))}$

• Второй:

  ${\displaystyle A\equiv ((B\equiv (A\equiv C))\equiv (C\equiv B))}$

• Третий:

  ${\displaystyle (A\equiv (B\equiv C))\equiv (C\equiv (A\equiv B))}$

• Четвертое:

  ${\displaystyle (A\equiv B)\equiv (C\equiv ((B\equiv C)\equiv A))}$

• Пятое:

  ${\displaystyle (A\equiv B)\equiv (C\equiv ((C\equiv B)\equiv A))}$

• Шестое:

  ${\displaystyle ((A\equiv (B\equiv C))\equiv C)\equiv (B\equiv A)}$

• Седьмой:

  ${\displaystyle ((A\equiv (B\equiv C))\equiv B)\equiv (C\equiv A)}$

Система аксиом Калмана: ^[18]

${\displaystyle A\equiv ((B\equiv (C\equiv A))\equiv (C\equiv B))}$

Системы аксиом Винкера: ^[18]

• Первый:

  ${\displaystyle A\equiv ((B\equiv C)\equiv ((A\equiv C)\equiv B))}$

• Второй:

  ${\displaystyle A\equiv ((B\equiv C)\equiv ((C\equiv A)\equiv B))}$

Система аксиом XCB: ^[18]

${\displaystyle A\equiv (((A\equiv B)\equiv (C\equiv B))\equiv C)}$

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