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

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

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

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

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

Импликация и отрицание [ править ]

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

${\ displaystyle A, A \ до B \ vdash B.}$

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

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

${\ Displaystyle А \ к (В \ к А)}$

${\ Displaystyle (А \ К (В \ К С)) \ К ((А \ К В) \ К (А \ К С))}$

${\ Displaystyle (от А \ к В) \ к (\ отр В \ к \ от А)}$

${\ Displaystyle \ neg \ neg от А \ до А}$

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

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

${\ Displaystyle А \ к (В \ к А)}$

${\ Displaystyle (А \ К (В \ К С)) \ К (В \ К (А \ К С))}$

${\ Displaystyle (В \ к С) \ к ((от А \ к В) \ к (от А \ к С))}$

${\ Displaystyle А \ к (\ от А \ к В)}$

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

• Четвертый: ^{[ необходима цитата ]}

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

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

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

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

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

Sobociński «S системы аксиом: ^[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}$

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

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

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

• Второй: ^[4]

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

Отрицание и дизъюнкция [ править ]

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

${\displaystyle A,\neg A\lor B\vdash 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}$

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

• Первый:

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

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

Ход Шеффера [ править ]

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

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

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

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

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

• Первый:

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

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

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

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

• Первый:

${\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)]}$^[8]

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

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

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

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

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

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

• Первый: ^[9]

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

• Второй: ^[9]

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

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

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

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

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

${\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)))}$^[12]

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

• Первый:

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

Johansson «s минимальная логика может быть аксиоматизирован любым из систем аксиом для положительного исчисления высказываний и расширяет язык с нульарной связкой , без каких - либо дополнительных схем аксиом. В качестве альтернативы, это также можно аксиоматизировать на языке , расширив положительное исчисление высказываний с помощью аксиомы${\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)}$

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

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

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

${\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 A,A\equiv B\vdash B}$

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

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

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

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

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

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

• Первый:

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

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

• Первый:

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

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

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

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

• Первый:

${\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: ^[16]

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

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

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

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