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

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

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

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

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

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

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

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

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

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

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

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)

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

Первый:
$(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)$

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

(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)

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

[(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))

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

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)

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

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)

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

Первый:
$\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

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

Первый: ^[5]^[6]^[7]
$((((A\to B)\to (C\to \bot ))\to D)\to E)\to ((E\to A)\to (C\to A))$
Второй: ^[5]
$((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

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

Первый:
$\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 в качестве правила вывода. В своей книге ^[9] он использовал импликацию, чтобы представить свои схемы аксиом. " $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}}.

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

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

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

Первый:
$(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)])]$

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

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

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

Первый:

(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)]

^[10]

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

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

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

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

A\to (B\to A)

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

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

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

Первый: ^[11]
$[(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]
$[(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)))$

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

((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) представляет собой расширение интуиционистской логики, которую можно аксиоматизировать с помощью интуиционистской системы аксиом плюс аксиома ^[13]

\neg A\lor \neg \neg A.

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

(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)))$ ^[14]

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

Первый:
$(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)

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

(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

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

\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}}.

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

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

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

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

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)$

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

Первый:
$(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))$

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

Первый:
$((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)$

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

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

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

Первый:
$A\equiv ((B\equiv C)\equiv ((A\equiv C)\equiv B))$
Второй:
$A\equiv ((B\equiv C)\equiv ((C\equiv A)\equiv B))$

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

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

См. также

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

Ссылки

^ Jump up to: ^а ^б ^с ^д ^и Ясуюки Имаи, Киёси Исэки, Об аксиомных системах исчисления высказываний, I, Труды Японской академии. Том 41, номер 6 (1965), 436–439.
^ Ёсинари Араи, Об аксиомных системах исчисления высказываний, II, Труды Японской академии. Том 41, номер 6 (1965), 440–442.
^ Часть XIII: Сётаро Танака. О системах аксиом исчисления высказываний, XIII. Учеб. Японская академия, том 41, номер 10 (1965), 904–907.
^ Эллиот Мендельсон, Введение в математическую логику , Ван Ностранд, Нью-Йорк, 1979, с. 31.
^ Jump up to: ^а ^б ^с ^д ^и ^ж [Фительсон, 2001] «Новые элегантные аксиоматизации некоторых логических выводов» Брэндена Фительсона.
^ (Компьютерный анализ Аргонна показал, что это самая короткая одиночная аксиома с наименьшим количеством переменных для исчисления высказываний).
^ Jump up to: ^а ^б «Некоторые новые результаты в логических исчислениях, полученные с помощью автоматизированного рассуждения», Зак Эрнст, Кен Харрис и Брэнден Фительсон, http://www.mcs.anl.gov/research/projects/AR/award-2001/fitelson.pdf
^ К. Мередит, Одиночные аксиомы для систем (C, N), (C, 0) и (A, N) двузначного исчисления высказываний , Журнал вычислительных систем, стр. 155–164, 1954.
^ Россер Дж. Баркли, «Логика для математиков», Нью-Йорк, McGraw-Hill, 1953. [1]
^ , с. 9, Спектр применения автоматизированного мышления , Ларри Вос; arXiv:cs/0205078v1
^ Jump up to: ^а ^б ^с ^д Исследования исчисления предложений в логике, семантике, метаматематике: статьи Альфреда Тарского с 1923 по 1938 год , Коркоран, Дж., Изд. Хакетт. 1-е издание отредактировано и переведено Дж. Х. Вудгером, Оксфордский университет. Нажимать. (1956)
^ Лукасевич, Дж. (1948). Кратчайшая аксиома импликативного исчисления высказываний. Труды Королевской ирландской академии. Раздел А: Математические и физические науки, 52, 25–33. Получено с https://www.jstor.org/stable/20488489.
^ Jump up to: ^а ^б А. Чагров, М. Захарьящев, Модальная логика , Oxford University Press, 1997.
^ К. Мередит, Единственная аксиома позитивной логики , Журнал вычислительных систем, с. 169–170, 1954.
^ Jump up to: ^а ^б Л. Х. Хакстафф, Системы формальной логики , Springer, 1966.
^ Киёси Исеки, Об аксиомных системах исчисления высказываний, XV, Труды Японской академии. Том 42, номер 3 (1966), 217–220.
^ Ёсинари Араи, Об аксиомных системах исчисления высказываний, XVII, Труды Японской академии. Том 42, номер 4 (1966), 351–354.
^ Jump up to: ^а ^б ^с ^д ^и XCB, последняя из кратчайших одиночных аксиом классического эквивалентного исчисления , ЛАРРИ УОС, ДОЛЬФ УЛЬРИХ,БРАНДЕН ФИТЕЛСОН; arXiv:cs/0211015v1

[Pro_I-1] Jump up to: ^а ^б ^с ^д ^и Ясуюки Имаи, Киёси Исэки, Об аксиомных системах исчисления высказываний, I, Труды Японской академии. Том 41, номер 6 (1965), 436–439.

[Pro_II-2] Ёсинари Араи, Об аксиомных системах исчисления высказываний, II, Труды Японской академии. Том 41, номер 6 (1965), 440–442.

[Pro_XIII-3] Часть XIII: Сётаро Танака. О системах аксиом исчисления высказываний, XIII. Учеб. Японская академия, том 41, номер 10 (1965), 904–907.

[4] Эллиот Мендельсон, Введение в математическую логику , Ван Ностранд, Нью-Йорк, 1979, с. 31.

[Fit-5] Jump up to: ^а ^б ^с ^д ^и ^ж [Фительсон, 2001] «Новые элегантные аксиоматизации некоторых логических выводов» Брэндена Фительсона.

[6] (Компьютерный анализ Аргонна показал, что это самая короткая одиночная аксиома с наименьшим количеством переменных для исчисления высказываний).

[AR-7] Jump up to: ^а ^б «Некоторые новые результаты в логических исчислениях, полученные с помощью автоматизированного рассуждения», Зак Эрнст, Кен Харрис и Брэнден Фительсон, http://www.mcs.anl.gov/research/projects/AR/award-2001/fitelson.pdf

[8] К. Мередит, Одиночные аксиомы для систем (C, N), (C, 0) и (A, N) двузначного исчисления высказываний , Журнал вычислительных систем, стр. 155–164, 1954.

[9] Россер Дж. Баркли, «Логика для математиков», Нью-Йорк, McGraw-Hill, 1953. [1]

[10] , с. 9, Спектр применения автоматизированного мышления , Ларри Вос; arXiv:cs/0205078v1

[ISC-11] Jump up to: ^а ^б ^с ^д Исследования исчисления предложений в логике, семантике, метаматематике: статьи Альфреда Тарского с 1923 по 1938 год , Коркоран, Дж., Изд. Хакетт. 1-е издание отредактировано и переведено Дж. Х. Вудгером, Оксфордский университет. Нажимать. (1956)

[12] Лукасевич, Дж. (1948). Кратчайшая аксиома импликативного исчисления высказываний. Труды Королевской ирландской академии. Раздел А: Математические и физические науки, 52, 25–33. Получено с https://www.jstor.org/stable/20488489.

[CZ-13] Jump up to: ^а ^б А. Чагров, М. Захарьящев, Модальная логика , Oxford University Press, 1997.

[14] К. Мередит, Единственная аксиома позитивной логики , Журнал вычислительных систем, с. 169–170, 1954.

[Hackstaff-15] Jump up to: ^а ^б Л. Х. Хакстафф, Системы формальной логики , Springer, 1966.

[16] Киёси Исеки, Об аксиомных системах исчисления высказываний, XV, Труды Японской академии. Том 42, номер 3 (1966), 217–220.

[XVII-17] Ёсинари Араи, Об аксиомных системах исчисления высказываний, XVII, Труды Японской академии. Том 42, номер 4 (1966), 351–354.

[XCB-18] Jump up to: ^а ^б ^с ^д ^и XCB, последняя из кратчайших одиночных аксиом классического эквивалентного исчисления , ЛАРРИ УОС, ДОЛЬФ УЛЬРИХ,БРАНДЕН ФИТЕЛСОН; arXiv:cs/0211015v1

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]