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

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

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

Классическое исчисление высказываний является стандартной логикой высказываний. Ее предполагаемая семантика бивалентна , а ее основное свойство состоит в том, что она является строго полной , иначе говоря, всякий раз, когда формула семантически следует из набора посылок, она также следует из этого набора синтаксически. Было сформулировано множество различных эквивалентных полных систем аксиом. Они отличаются выбором используемых базовых связок , которые во всех случаях должны быть функционально полными (т. е. способны выражать композицией все 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)$
Четвертое: ^{[ нужна цитата ]}
$(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)$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Первый:

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

^[9]

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

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

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

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

A\to (B\to A)

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

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

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

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

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

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

\neg A\lor \neg \neg A.

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

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

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

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

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

(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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

См. также [ править ]

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

Ссылки [ править ]

^ Перейти обратно: ^а ^б ^с ^д ^Это Ясуюки Имаи, Киёси Исэки, Об аксиомных системах исчисления высказываний, I, Труды Японской академии. Том 41, номер 6 (1965), 436–439.
^ Часть XIII: Сётаро Танака. О системах аксиом исчисления высказываний, XIII. Учеб. Японская академия, том 41, номер 10 (1965), 904–907.
^ Эллиот Мендельсон, Введение в математическую логику , Ван Ностранд, Нью-Йорк, 1979, с. 31.
^ Перейти обратно: ^а ^б ^с ^д ^Это ^ж [Фительсон, 2001] «Новые элегантные аксиоматизации некоторых логических выводов» Брэндена Фительсона.
^ (Компьютерный анализ Аргонна показал, что это самая короткая одиночная аксиома с наименьшим количеством переменных для исчисления высказываний).
^ Перейти обратно: ^а ^б «Некоторые новые результаты в логических исчислениях, полученные с помощью автоматического рассуждения», Зак Эрнст, Кен Харрис и Брэнден Фительсон, 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
^ Перейти обратно: ^а ^б ^с ^д Исследования исчисления предложений в 1923–1938 гг логике, семантике, метаматематике: статьи Альфреда Тарского , Дж. Коркорана, изд. . Хакетт. 1-е издание отредактировано и переведено Дж. Х. Вудгером, Оксфордский университет. Нажимать. (1956)
^ Лукасевич, Дж. (1948). Кратчайшая аксиома импликативного исчисления высказываний. Труды Королевской ирландской академии. Раздел А: Математические и физические науки, 52, 25–33. Получено с https://www.jstor.org/stable/20488489.
^ Перейти обратно: ^а ^б А. Чагров, М. Захарьящев, Модальная логика , Oxford University Press, 1997.
^ К. Мередит, Единственная аксиома позитивной логики , Журнал вычислительных систем, стр. 169–170, 1954.
^ Перейти обратно: ^а ^б Л. Х. Хакстафф, Системы формальной логики , Springer, 1966.
^ Киёси Исеки, Об аксиомных системах исчисления высказываний, XV, Труды Японской академии. Том 42, номер 3 (1966), 217–220.
^ Ёсинари Араи, Об аксиомных системах исчисления высказываний, XVII, Труды Японской академии. Том 42, номер 4 (1966), 351–354.
^ Перейти обратно: ^а ^б ^с ^д ^Это XCB, последняя из кратчайших одиночных аксиом классического эквивалентного исчисления , ЛАРРИ УОС, ДОЛЬФ УЛЬРИХ, БРАНДЕН ФИТЕЛСОН; arXiv:cs/0211015v1

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]