Список систем Гильберта - List of Hilbert systems

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

• Первый:

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

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

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

• Второй:

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

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

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

• В третьих:

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

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

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

• Четвертый:

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

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

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

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

${\ Displaystyle [(А \ к (В \ к А)) \ к ([(\ отр С \ к (D \ к \ отр E)) \ к [(С \ к (D \ к F)) \ к ((E \ to D) \ to (E \ to F))]] \ to G)] \ to (H \ to G)}$

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

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

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

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

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

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

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

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

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

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

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

${\ Displaystyle (А \ к \ neg A) \ к \ neg A}$

${\ Displaystyle (А \ к \ Нег В) \ К (В \ к \ Нег А)}$

Sobociński «S системы аксиом:

• Первый:

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

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

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

• Второй:

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

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

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

Последствия и ложь

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

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

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

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

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

${\ displaystyle \ bot \ to A}$

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

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

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

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

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

• Первый:

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

• Второй:

  ${\ Displaystyle ((А \ к В) \ к ((\ бот \ к С) \ к D)) \ к ((D \ к А) \ к (Е \ к (F \ к А)))}$

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

Вместо импликации классическая логика также может быть сформулирована с использованием функционально полного набора связок. В этих формулировках используется следующее правило вывода; ${\ 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 (А \ лор В) \ лор (В \ лор А)}$

${\ Displaystyle \ Нег А \ лор (В \ лор А)}$

${\ Displaystyle \ neg (А \ лор А) \ лор А}$

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

• Первый:

  ${\ 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 \ Нег (\ Нег (\ Нег А \ лор В) \ лор (С \ лор (D \ лор Е))) \ лор (\ Нег (\ Нег С \ лор А) \ лор (Е \ лор ( Д \ лор А)))}$

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

Инсульт Шеффера

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

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

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

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

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

• Первый:

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

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

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

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

• Первый:

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

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

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

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

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

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

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

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

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

• Первый:

  ${\ Displaystyle [(A \ к (B \ к A)) \ к [([((C \ к D) \ к E) \ к F] \ к [(D \ к F) \ к (C \ к F)]) \ к G]] \ к G}$

• Второй:

  ${\ Displaystyle [(A \ к B) \ к ((C \ к D) \ к E)] \ к ([F \ к ((C \ к D) \ к E)] \ к [(A \ к F) \ to (D \ to E)])}$

• В третьих:

  ${\ Displaystyle ((А \ к В) \ к (С \ к D)) \ к (Е \ к ((D \ к А) \ к (С \ к А)))}$

• Четвертый:

  ${\ Displaystyle ((А \ к В) \ к (С \ к D)) \ к ((D \ к А) \ к (Е \ к (С \ к А)))}$

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

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

Интуиционистская и промежуточная логика

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

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

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

${\ Displaystyle (А \ земля В) \ к А}$

${\ Displaystyle (A \ земля B) \ к B}$

${\ Displaystyle А \ к (В \ к (А \ земля B))}$

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

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

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

${\ displaystyle \ bot \ to A}$

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

${\ Displaystyle (А \ к \ neg A) \ к \ neg A}$

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

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

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

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

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

${\ Displaystyle (от A \ до B) \ lor (от B \ до A).}$

Положительное импликационное исчисление

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

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

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

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

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

• Первый:

  ${\ Displaystyle Е \ к ((А \ к В) \ к (((D \ к А) \ к (В \ к С)) \ к (А \ к С)))}$

• Второй:

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

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

• В третьих:

  ${\ Displaystyle ((А \ к В) \ к С) \ к (D \ к ((В \ к (С \ к Е)) \ к (В \ к Е)))}$

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

• Первый:

  ${\ Displaystyle (А \ К (А \ К Б)) \ К (А \ К Б)}$

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

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

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

• Второй:

  ${\ Displaystyle (А \ К (А \ К Б)) \ К (А \ К Б)}$

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

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

• В третьих:

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

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

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

  ${\ Displaystyle (А \ К (А \ К Б)) \ К (А \ К Б)}$

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

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

${\ Displaystyle (А \ земля В) \ к А}$

${\ Displaystyle (A \ земля B) \ к B}$

${\ Displaystyle А \ к (В \ к (А \ земля B))}$

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

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

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

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

${\ Displaystyle (A \ leftrightarrow B) \ к (от A \ к B)}$

${\ Displaystyle (A \ leftrightarrow B) \ к (B \ к A)}$

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

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

${\ Displaystyle (А \ к \ Нег В) \ К (В \ к \ Нег А)}$

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

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

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

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

${\ Displaystyle (А \ к \ Нег В) \ К (В \ к \ Нег А)}$

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

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

${\ Displaystyle (А \ к \ neg A) \ к \ neg A}$

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

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

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

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

${\ Displaystyle (А \ к \ Нег В) \ К (В \ к \ Нег А)}$

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

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

${\ 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 \ земля B) \ leftrightarrow (\ neg A \ lor \ neg B)}$

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

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

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

${\ Displaystyle А, А \ эквив Б \ vdash B}$

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

${\ Displaystyle ((А \ эквив С) \ эквив (В \ эквив А)) \ эквив (С \ эквив В)}$

${\ Displaystyle (А \ эквив (В \ эквив С)) \ экв ((А \ эквив В) \ эквив С)}$

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

${\ Displaystyle А \ экв А}$

${\ Displaystyle (А \ эквив В) \ экв (В \ экв А)}$

${\ Displaystyle (А \ эквив В) \ эквив ((В \ эквив С) \ эквив (А \ эквив С))}$

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

• Первый:

  ${\ Displaystyle (А \ эквив (В \ эквив С)) \ экв ((А \ эквив В) \ эквив С)}$

  ${\ Displaystyle ((А \ эквив С) \ эквив (В \ эквив А)) \ эквив (С \ эквив В)}$

• Второй:

  ${\ Displaystyle (А \ эквив В) \ экв (В \ экв А)}$

  ${\ Displaystyle ((А \ эквив С) \ эквив (В \ эквив А)) \ эквив (С \ эквив В)}$

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

• Первый:

  ${\ Displaystyle (А \ эквив В) \ эквив ((С \ эквив В) \ эквив (А \ эквив С))}$

• Второй:

  ${\ Displaystyle (А \ эквив В) \ эквив ((А \ эквив С) \ эквив (С \ эквив В))}$

• В третьих:

  ${\ Displaystyle (А \ эквив В) \ эквив ((С \ эквив А) \ эквив (В \ эквив С))}$

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

• Первый:

  ${\ Displaystyle ((А \ эквив В) \ эквив С) \ эквив (В \ эквив (С \ эквив А))}$

• Второй:

  ${\ Displaystyle А \ эквив ((В \ эквив (А \ эквив С)) \ эквив (С \ эквив В))}$

• В третьих:

  ${\ Displaystyle (А \ эквив (В \ эквив С)) \ эквив (С \ эквив (А \ эквив В))}$

• Четвертый:

  ${\ Displaystyle (А \ эквив В) \ эквив (С \ эквив ((В \ эквив С) \ эквив А))}$

• Пятый:

  ${\ Displaystyle (А \ эквив В) \ эквив (С \ эквив ((С \ эквив В) \ эквив А))}$

• Шестое:

  ${\ Displaystyle ((А \ эквив (В \ эквив С)) \ эквив С) \ эквив (В \ эквив А)}$

• Седьмой:

  ${\ Displaystyle ((А \ эквив (В \ эквив С)) \ эквив В) \ эквив (С \ эквив А)}$

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

${\ Displaystyle А \ эквив ((В \ эквив (С \ эквив А)) \ эквив (С \ эквив В))}$

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

• Первый:

  ${\ Displaystyle А \ эквив ((В \ эквив С) \ экв ((А \ эквив С) \ эквив В))}$

• Второй:

  ${\ Displaystyle А \ эквив ((В \ эквив С) \ экв ((С \ эквив А) \ эквив В))}$

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

${\ Displaystyle А \ эквив (((А \ эквив В) \ эквив (С \ эквив В)) \ эквив С)}$

Смотрите также

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

Рекомендации