Аксиоматическая система (логика)

В логике , особенно в математической логике , аксиоматическая система , иногда называемая дедуктивной системой «гильбертовского стиля», представляет собой тип системы формальной дедукции, разработанной Готтлобом Фреге . Ян Лукасевич , Рассел и Уайтхед, и Дэвид Гилберт . Эти дедуктивные системы чаще всего изучаются для логики первого порядка , но представляют интерес и для других логик.

Большинство вариантов аксиоматических систем придерживаются характерного подхода, балансируя между логическими аксиомами и правилами вывода . Аксиоматические системы могут характеризоваться выбором большого числа схем логических аксиом и небольшого набора правил вывода . Системы естественной дедукции придерживаются противоположного подхода, включая множество правил дедукции, но очень мало схем аксиом или вообще их отсутствие. Наиболее часто изучаемые аксиоматические системы имеют либо только одно правило вывода – modus ponens для логики высказываний – либо два – с обобщением , а также для обработки логики предикатов – и несколько бесконечных схем аксиом. Аксиоматические системы для алетических модальных логик , иногда называемые системами Гильберта-Льюиса , дополнительно требуют правила необходимости . Некоторые системы используют в качестве аксиом конечный список конкретных формул вместо бесконечного набора формул через схемы аксиом, и в этом случае равномерное правило замены требуется .

Характерной особенностью многих вариантов аксиоматических систем является то, что контекст не изменяется ни в одном из их правил вывода, в то время как как естественная дедукция , так и секвенциальное исчисление содержат некоторые правила изменения контекста. Таким образом, если интересовать только выводимость тавтологий , а не гипотетических суждений, то можно формализовать аксиоматическую систему так, чтобы ее правила вывода содержали лишь суждения достаточно простой формы. То же самое нельзя сделать и с двумя другими системами вычетов: поскольку в некоторых из их правил вывода изменяется контекст, их нельзя формализовать, чтобы можно было избежать гипотетических суждений – даже если мы хотим использовать их только для доказательства выводимости тавтологий.

Пропозициональная логика

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

Фреге Концептуальное письмо

Хотя аксиоматическое доказательство использовалось со времен знаменитого древнегреческого учебника « , Евклида Элементы геометрии» в логике высказываний оно восходит к Готтлоба Фреге года 1879 «Begriffsschrift» . Система Фреге использовала в качестве связок только импликацию и отрицание . и у него было шесть аксиом, какие это были:

• Предложение 1: $a\supset (b\supset a)$
• Предложение 2: $(c\supset (b\supset a))\supset ((c\supset b)\supset (c\supset a))$
• Предложение 8: $(d\supset (b\supset a))\supset (b\supset (d\supset a))$
• Предложение 28: $(b\supset a)\supset (\neg a\supset \neg b)$
• Предложение 31: $\neg \neg a\supset a$
• Предложение 41: $a\supset \neg \neg a$

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

Лукасевича _{П 2}

Ян Лукасевич показал, что в системе Фреге «третья аксиома является лишней, поскольку ее можно вывести из двух предыдущих аксиом, и что последние три аксиомы можно заменить одним предложением $CCNpNqCpq$". Лукасевича Что, переведя из польской записи в современную систему обозначений, означает: $(\neg p\rightarrow \neg q)\rightarrow (p\rightarrow q)$. Следовательно, Лукасевичу приписывают с этой системой трех аксиом:

• $p\to (q\to p)$
• $(p\to (q\to r))\to ((p\to q)\to (p\to r))$
• $(\neg p\to \neg q)\to (q\to p)$

Как и система Фреге, эта система использует правило замены и использует modus ponens в качестве правила вывода. Точно такую ​​же систему предложил (с явным правилом замены) Алонсо Чёрч , который назвал ее системой P _2, и способствовал его популяризации.

Схематическая форма Р ₂

A graphic representation of the deduction system

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

• $\varphi \to (\psi \to \varphi )$
• $(\varphi \to (\psi \to \chi ))\to ((\varphi \to \psi )\to (\varphi \to \chi ))$
• $(\neg \varphi \to \neg \psi )\to (\psi \to \varphi )$

Схематическая версия P ₂ приписывается Джону фон Нейману , и используется в базе данных формальных доказательств Metamath «set.mm». Его также приписывают Гильберту . и назван ${\mathcal {H}}$ в этом контексте.

Пример доказательства в P ₂

В качестве примера доказательство $A\to A$ в P ₂ приведен ниже. Во-первых, аксиомам даны имена:

(А1) $(p\to (q\to p))$

(А2) $((p\to (q\to r))\to ((p\to q)\to (p\to r)))$

(А3) $((\neg p\to \neg q)\to (q\to p))$

И доказательство следующее:

1. $A\to ((B\to A)\to A)$ (пример (A1))
2. $(A\to ((B\to A)\to A))\to ((A\to (B\to A))\to (A\to A))$ (пример (A2))
3. $(A\to (B\to A))\to (A\to A)$ (из (1) и (2) по modus ponens )
4. $A\to (B\to A)$ (пример (A1))
5. $A\to A$ (из (4) и (3) по modus ponens)

Согласованность и полнота P ₂

Важнейшими свойствами этого набора правил является то, что они надежны и полны . Неформально это означает, что правила верны и никаких других правил не требуется. Эти утверждения можно сделать более формальными следующим образом. Доказательства правильности и полноты логики высказываний сами по себе не являются доказательствами в логике высказываний; это теоремы в ZFC, используемые в качестве метатеории для доказательства свойств логики высказываний.

Мы определяем истинностное присвоение как функцию , которая отображает пропозициональные переменные в истинное или ложное . Неформально такое присвоение истинности можно понимать как описание возможного положения дел (или возможного мира ), в котором одни утверждения истинны, а другие — нет. Семантику формул затем можно формализовать, определив, для какого «положения дел» они считаются истинными, что и делается с помощью следующего определения.

Мы определяем, когда такое истинностное присвоение A удовлетворяет некоторой корректной формуле со следующими правилами:

• A удовлетворяет пропозициональной переменной P тогда и только тогда, когда A ( P ) = true
• A удовлетворяет ¬ φ тогда и только тогда, когда A не удовлетворяет φ
• A удовлетворяет ( φ ∧ ψ ) тогда и только тогда, когда A удовлетворяет как φ, так и ψ.
• A удовлетворяет ( φ ∨ ψ ) тогда и только тогда, когда A удовлетворяет хотя бы одному из φ или ψ
• A удовлетворяет ( φ → ψ ) тогда и только тогда, когда это не тот случай, когда A удовлетворяет φ , но не ψ
• A удовлетворяет ( φ ↔ ψ ) тогда и только тогда, когда A удовлетворяет обоим φ и ψ или не удовлетворяет ни одному из них.

С помощью этого определения мы теперь можем формализовать, что означает, что формула φ следует из определенного набора S формул. Неформально это верно, если во всех возможных мирах с учетом набора формул S также выполняется формула φ . Это приводит к следующему формальному определению: мы говорим, что набор S корректных формул семантически влечет за собой (или подразумевает ) определенную корректную формулу φ, если все назначения истинности, которые удовлетворяют всем формулам в S, также удовлетворяют φ .

Наконец, мы определяем синтаксическое следствие так, что φ синтаксически влечет за собой S тогда и только тогда, когда мы можем получить его с помощью правил вывода, которые были представлены выше, за конечное число шагов. Это позволяет нам точно сформулировать, что означает, что набор правил вывода является надежным и полным:

Правильность: если набор правильно составленных формул S синтаксически влечет за собой правильно составленную формулу φ, то S семантически влечет за собой φ .

Полнота: если набор правильно сформированных формул S семантически влечет за собой правильно сформированную формулу φ, то S синтаксически влечет за собой φ .

Для приведенного выше набора правил это действительно так.

Эскиз доказательства надежности

(Для большинства логических систем это сравнительно «простое» направление доказательства)

Соглашения об обозначениях: пусть G — переменная, охватывающая наборы предложений. Пусть A, B и C варьируются по предложениям. Поскольку « G синтаксически влечет за собой А », мы пишем « G доказывает А ». Поскольку « G семантически влечет за собой А », мы пишем « G подразумевает А ».

Мы хотим показать: ( A )( G ) (если G доказывает A , то G подразумевает A ).

Заметим, что « G доказывает А » имеет индуктивное определение, и это дает нам непосредственные ресурсы для демонстрации утверждений вида «Если G доказывает А , то...». Итак, наше доказательство проводится по индукции.

1. Основа. Докажите: Если является членом G , то G подразумевает A. A
2. Основа. Докажите: Если А аксиома, то из G следует А. —
3. Индуктивный шаг (индукция по n , длине доказательства):
   1. Предположим для произвольных G и A что если G доказывает A за n или меньше шагов, то G подразумевает A. ,
   2. Для каждого возможного применения правила вывода на шаге n +1 приводящего к новой теореме B , покажите, что из G следует B. ,

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

Базис» показывают, что простейшие доказуемые предложения из G также подразумеваются из G для любого G. Шаги « (Доказательство простое, поскольку семантический факт, что множество подразумевает любой из своих членов, также тривиален.) Индуктивный шаг будет систематически охватывать все дальнейшие предложения, которые могут быть доказуемы, - рассматривая каждый случай, в котором мы можем прийти к логическому выводу. используя правило вывода, и показывает, что если новое предложение доказуемо, оно также логически подразумевается. (Например, у нас может быть правило, говорящее нам, что из « А » мы можем вывести « А» или «В ». В III.a мы предполагаем, что если А доказуемо, то оно подразумевается. Мы также знаем, что если А доказуемо, то « A или B » доказуемо. Мы должны показать, что тогда « A или B также подразумевается ». Мы делаем это, апеллируя к семантическому определению и предположению, которое мы только что сделали. Мы предполагаем, что A доказуемо из G. Итак, это так. также подразумевается G. Таким образом, любая семантическая оценка, делающая все G истинным, делает A истинным, но любая оценка, делающая A истинным, делает « A» или «B » истинными в соответствии с определенной семантикой для «или». G true делает « A или B » истинным. Таким образом, подразумевается « А или Б ».) Как правило, индуктивный этап состоит из длительного, но простого каждом конкретном случае анализа всех правил вывода в , показывающего, что каждое из них «сохраняет» семантическую импликацию.

По определению доказуемости, не существует никаких предложений, которые можно было бы доказать, кроме как будучи членом G , аксиомой или следуя правилу; поэтому, если все это семантически подразумевается, дедуктивный расчет верен.

Эскиз доказательства полноты

(Обычно это гораздо более сложное направление доказательства.)

Мы принимаем те же обозначения, что и выше.

показать: если G подразумевает A , то G доказывает A. Мы хотим Мы действуем методом противопоставления : вместо этого мы показываем, что G не , доказывает A то G не следует из A. если Если мы покажем, что существует модель , в которой A не выполняется, несмотря на G истинность из G не следует A. , то, очевидно , Идея состоит в том, чтобы построить такую ​​модель, исходя из самого нашего предположения, что не доказывает A. G

1. G не A. доказывает (Предположение)
2. Если G не доказывает A , то мы можем построить (бесконечное) максимальное множество , G ^∗ , которое является надмножеством G и которое также не доказывает A .
   1. Упорядочите (с типом порядка ω) все предложения на языке (например, сначала самые короткие и одинаково длинные в расширенном алфавитном порядке) и пронумеруйте их ( E ₁ , E ₂ , ...)
   2. Определим серию G _n множеств ( G ₀ , G ₁ , ...) индуктивно:
      1. $G_{0}=G$
      2. Если $G_{k}\cup \{E_{k+1}\}$ доказывает A , тогда $G_{k+1}=G_{k}$
      3. Если $G_{k}\cup \{E_{k+1}\}$ не доказывает то A , $G_{k+1}=G_{k}\cup \{E_{k+1}\}$
   3. Определить G ^∗ как объединение всех G _n . (то есть Г. ^∗ — множество всех предложений, входящих в любой . _Gn )
   4. Можно легко показать, что
      1. Г ^∗ содержит (является надмножеством) G (по (bi));
      2. Г ^∗ не доказывает A (поскольку доказательство будет содержать только конечное число предложений, и когда последнее из них будет введено в некотором то _, Gn A _{докажет} вопреки определению Gn ) _Gn ; и
      3. Г ^∗ является максимальным набором относительно A было добавлено еще какое-либо предложение : если к G ^∗ докажет А. , это что, если бы можно было добавить еще предложения, их следовало бы добавлять тогда, когда они встречались при построении Gn _{( Потому} , опять же по определению)
3. Если Г ^∗ является максимальным множеством относительно A , то оно истинноподобно . Это означает, что он содержит C тогда и только тогда, когда он не содержит ¬C ; Если он содержит C и содержит «Если C, то B », то он также содержит B ; и так далее. Чтобы показать это, нужно показать, что аксиоматическая система достаточно сильна для следующего:
   • Для любых формул C и D , если доказываются и , и ¬C , то доказывается D. C Отсюда следует, что максимальное множество относительно A не может доказать одновременно C и ¬C доказывало бы A. , так как в противном случае оно
   • Для любых формул C и D , если доказано C → D и ¬C → D доказано D. , то Это используется вместе с теоремой о дедукции , чтобы показать, что для любой формулы либо она, либо ее отрицание находится в G ^∗ : Пусть B — формула, не принадлежащая G ^∗ ; тогда Г ^∗ добавлением B доказывает A. с Таким образом, из теоремы дедукции следует, что G ^∗ доказывает B → A. ​Но предположим, что ¬B также не было в G ^∗ , то по той же логике G ^∗ также доказывает ¬B → A ; но тогда Г ^∗ доказывает A , ложность которого мы уже показали.
   • Для любых формул C и D , если доказано C и D то доказано C → D. ,
   • Для любых формул C и D , если доказано C и ¬D , то доказывается ¬( C → D ).
   • Для любых формул C и D , если доказывается ¬C то доказывается C → D. ,
   Если дополнительные логические операции (такие как конъюнкция и/или дизъюнкция) также являются частью словаря, то к аксиоматической системе предъявляются дополнительные требования (например, если она доказывает C и D , она также доказывает и их конъюнкцию).
4. Если Г ^∗ похоже на правду, есть G ^∗ -Каноническая оценка языка: такая, которая превращает каждое предложение в G ^∗ правда и все за пределами G ^∗ ложно, но при этом подчиняется законам семантической композиции в языке. Требование истинности необходимо для того, чтобы гарантировать, что это присвоение истинности будет удовлетворять законам семантической композиции в языке.
5. А Г ^∗ -каноническая оценка сделает наш исходный набор G истинным, а A — ложным.
6. Если существует оценка, при которой G истинны, а ложны , то G не (семантически) подразумевает A. A

Таким образом, каждая система, которая имеет modus ponens в качестве правила вывода и доказывает следующие теоремы (включая их замены), является полной:

• $p\to (\neg p\to q)$
• $(p\to q)\to ((\neg p\to q)\to q)$
• $p\to (q\to (p\to q))$
• $p\to (\neg q\to \neg (p\to q))$
• $\neg p\to (p\to q)$
• $p\to p$
• $p\to (q\to p)$
• $(p\to (q\to r))\to ((p\to q)\to (p\to r))$

Первые пять используются для удовлетворения пяти условий этапа III выше, а последние три — для доказательства теоремы дедукции.

Пример

В качестве примера можно показать, что, как и любая другая тавтология, три аксиомы классической системы исчисления высказываний, описанной ранее, могут быть доказаны в любой системе, которая удовлетворяет вышесказанному, а именно, которая имеет modus ponens в качестве правила вывода и доказывает вышеизложенное. восемь теорем (включая их замены). Из восьми теорем последние две являются двумя из трех аксиом; третья аксиома, $(\neg q\to \neg p)\to (p\to q)$, также может быть доказано, как мы сейчас покажем.

Для доказательства мы можем использовать гипотетическую теорему о силлогизме (в форме, актуальной для этой аксиоматической системы), поскольку она опирается только на две аксиомы, которые уже входят в приведенный выше набор из восьми теорем. Доказательство тогда следующее:

1. $q\to (p\to q)$ (пример 7-й теоремы)
2. $(q\to (p\to q))\to ((\neg q\to \neg p)\to (q\to (p\to q)))$ (пример 7-й теоремы)
3. $(\neg q\to \neg p)\to (q\to (p\to q))$ (из (1) и (2) по modus ponens)
4. $(\neg p\to (p\to q))\to ((\neg q\to \neg p)\to (\neg q\to (p\to q)))$ (пример теоремы о гипотетическом силлогизме)
5. $(\neg p\to (p\to q))$ (пример 5-й теоремы)
6. $(\neg q\to \neg p)\to (\neg q\to (p\to q))$ (из (5) и (4) по modus ponens)
7. $(q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q))$ (пример 2-й теоремы)
8. $((q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q)))\to ((\neg q\to \neg p)\to ((q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q))))$ (пример 7-й теоремы)
9. $(\neg q\to \neg p)\to ((q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q)))$ (из (7) и (8) по modus ponens)
10. $((\neg q\to \neg p)\to ((q\to (p\to q))\to ((\neg q\to (p\to q))\to (p\to q))))\to$

    $(((\neg q\to \neg p)\to (q\to (p\to q)))\to ((\neg q\to \neg p)\to ((\neg q\to (p\to q))\to (p\to q))))$ (пример 8-й теоремы)

11. $((\neg q\to \neg p)\to (q\to (p\to q)))\to ((\neg q\to \neg p)\to ((\neg q\to (p\to q))\to (p\to q)))$ (из (9) и (10) по modus ponens)
12. $(\neg q\to \neg p)\to ((\neg q\to (p\to q))\to (p\to q))$ (из (3) и (11) по modus ponens)
13. $((\neg q\to \neg p)\to ((\neg q\to (p\to q))\to (p\to q)))\to (((\neg q\to \neg p)\to (\neg q\to (p\to q)))\to ((\neg q\to \neg p)\to (p\to q)))$ (пример 8-й теоремы)
14. $((\neg q\to \neg p)\to (\neg q\to (p\to q)))\to ((\neg q\to \neg p)\to (p\to q))$ (из (12) и (13) по modus ponens)
15. $(\neg q\to \neg p)\to (p\to q)$ (из (6) и (14) по modus ponens)

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

Теперь мы проверим, что классическая система исчисления высказываний, описанная ранее, действительно может доказать необходимые восемь упомянутых выше теорем. Мы используем несколько доказанных здесь лемм :

(ДН1) $\neg \neg p\to p$ - Двойное отрицание (в одном направлении)

(ДН2) $p\to \neg \neg p$ - Двойное отрицание (другое направление)

(HS1) $(q\to r)\to ((p\to q)\to (p\to r))$ - одна из форм гипотетического силлогизма

(HS2) $(p\to q)\to ((q\to r)\to (p\to r))$ - другая форма гипотетического силлогизма.

(ТР1) $(p\to q)\to (\neg q\to \neg p)$ - Транспонирование

(ТР2) $(\neg p\to q)\to (\neg q\to p)$ - другая форма транспозиции.

(Л1) $p\to ((p\to q)\to q)$

(Л3) $(\neg p\to p)\to p$

Мы также используем метод метатеоремы гипотетического силлогизма как сокращение для нескольких шагов доказательства.

• $p\to (\neg p\to q)$ - доказательство:
  1. $p\to (\neg q\to p)$ (пример (A1))
  2. $(\neg q\to p)\to (\neg p\to \neg \neg q)$ (экземпляр (TR1))
  3. $p\to (\neg p\to \neg \neg q)$ (из (1) и (2) с использованием метатеоремы гипотетического силлогизма)
  4. $\neg \neg q\to q$ (экземпляр (DN1))
  5. $(\neg \neg q\to q)\to ((\neg p\to \neg \neg q)\to (\neg p\to q))$ (пример (HS1))
  6. $(\neg p\to \neg \neg q)\to (\neg p\to q)$ (из (4) и (5) с использованием modus ponens)
  7. $p\to (\neg p\to q)$ (из (3) и (6) с использованием метатеоремы гипотетического силлогизма)
• $(p\to q)\to ((\neg p\to q)\to q)$ - доказательство:
  1. $(p\to q)\to ((\neg q\to p)\to (\neg q\to q))$ (пример (HS1))
  2. $(\neg q\to q)\to q$ (пример (L3))
  3. $((\neg q\to q)\to q)\to (((\neg q\to p)\to (\neg q\to q))\to ((\neg q\to p)\to q))$ (пример (HS1))
  4. $((\neg q\to p)\to (\neg q\to q))\to ((\neg q\to p)\to q)$ (из (2) и (3) по modus ponens)
  5. $(p\to q)\to ((\neg q\to p)\to q)$ (из (1) и (4) с использованием метатеоремы гипотетического силлогизма)
  6. $(\neg p\to q)\to (\neg q\to p)$ (пример (TR2))
  7. $((\neg p\to q)\to (\neg q\to p))\to (((\neg q\to p)\to q)\to ((\neg p\to q)\to q))$ (пример (HS2))
  8. $((\neg q\to p)\to q)\to ((\neg p\to q)\to q)$ (из (6) и (7) с использованием modus ponens)
  9. $(p\to q)\to ((\neg p\to q)\to q)$ (из (5) и (8) с использованием метатеоремы гипотетического силлогизма)
• $p\to (q\to (p\to q))$ - доказательство:
  1. $q\to (p\to q)$ (пример (A1))
  2. $(q\to (p\to q))\to (p\to (q\to (p\to q)))$ (пример (A1))
  3. $p\to (q\to (p\to q))$ (из (1) и (2) с использованием modus ponens)
• $p\to (\neg q\to \neg (p\to q))$ - доказательство:
  1. $p\to ((p\to q)\to q)$ (пример (L1))
  2. $((p\to q)\to q)\to (\neg q\to \neg (p\to q))$ (экземпляр (TR1))
  3. $p\to (\neg q\to \neg (p\to q))$ (из (1) и (2) с использованием метатеоремы гипотетического силлогизма)
• $\neg p\to (p\to q)$ - доказательство:
  1. $\neg p\to (\neg q\to \neg p)$ (пример (A1))
  2. $(\neg q\to \neg p)\to (p\to q)$ (пример (A3))
  3. $\neg p\to (p\to q)$ (из (1) и (2) с использованием метатеоремы гипотетического силлогизма)
• $p\to p$ - доказательство, приведенное в примере доказательства выше
• $p\to (q\to p)$ - аксиома (А1)
• $(p\to (q\to r))\to ((p\to q)\to (p\to r))$ - аксиома (А2)

Еще один план доказательства полноты

Если формула является тавтологией , то для нее существует таблица истинности , которая показывает, что каждая оценка дает истинное значение для формулы. Рассмотрим такую ​​оценку. С помощью математической индукции по длине подформул покажите, что истинность или ложность подформулы следует из истинности или ложности (в зависимости от оценки) каждой пропозициональной переменной в подформуле. Затем объедините строки таблицы истинности вместе по две, используя «( P истинно, подразумевает S ) подразумевает (( P ложно, подразумевает S ) подразумевает S )». Продолжайте повторять это до тех пор, пока не будут устранены все зависимости от пропозициональных переменных. В результате мы доказали данную тавтологию. Поскольку любая тавтология доказуема, логика полна.

Другая система аксиоматических доказательств

Можно определить другую версию исчисления высказываний, которая определяет большую часть синтаксиса логических операторов посредством аксиом и использует только одно правило вывода.

Аксиомы

Пусть φ , χ и ψ обозначают корректные формулы. (Сами правильно построенные формулы не будут содержать греческих букв, а только заглавные латинские буквы, соединительные операторы и круглые скобки.) Тогда аксиомы будут следующими:

Аксиомы

Имя	Схема аксиом	Описание
ТОГДА-1	$\phi \to (\chi \to \phi )$	Добавить гипотезу χ , введение импликации
ТОГДА-2	$(\phi \to (\chi \to \psi ))\to ((\phi \to \chi )\to (\phi \to \psi ))$	Распределить гипотезу $\phi$ чрезмерная импликация
И-1	$\phi \land \chi \to \phi$	Устранить союз
И-2	$\phi \land \chi \to \chi$
И-3	$\phi \to (\chi \to (\phi \land \chi ))$	Ввести союз
ОР-1	$\phi \to \phi \lor \chi$	Ввести дизъюнкцию
ОР-2	$\chi \to \phi \lor \chi$
ОР-3	$(\phi \to \psi )\to ((\chi \to \psi )\to (\phi \lor \chi \to \psi ))$	Устранить дизъюнкцию
НЕ-1	$(\phi \to \chi )\to ((\phi \to \neg \chi )\to \neg \phi )$	Ввести отрицание
НЕ-2	$\phi \to (\neg \phi \to \chi )$	Устранить отрицание
НЕ-3	$\phi \lor \neg \phi$	Исключена середина, классическая логика
МКФ-1	$(\phi \leftrightarrow \chi )\to (\phi \to \chi )$	Устранить эквивалентность
МКФ-2	$(\phi \leftrightarrow \chi )\to (\chi \to \phi )$
МКФ-3	$(\phi \to \chi )\to ((\chi \to \phi )\to (\phi \leftrightarrow \chi ))$	Ввести эквивалентность

• Аксиому THEN-2 можно рассматривать как «распределительное свойство импликации относительно импликации».
• Аксиомы И-1 и И-2 соответствуют «устранению соединения». Отношение между AND-1 и AND-2 отражает коммутативность оператора конъюнкции.
• Аксиома AND-3 соответствует «введению союза».
• Аксиомы ОР-1 и ОР-2 соответствуют «введению дизъюнкции». Связь между OR-1 и OR-2 отражает коммутативность оператора дизъюнкции.
• Аксиома НЕ-1 соответствует «доведению до абсурда».
• Аксиома НЕ-2 гласит, что «из противоречия можно вывести все».
• Аксиома НЕ-3 называется « tertium non datur » ( лат . «третьего не дано») и отражает семантическую оценку пропозициональных формул: формула может иметь истинностное значение либо истинное, либо ложное. Третьего истинностного значения не существует, по крайней мере, в классической логике. Логики-интуиционисты не принимают аксиому НЕ-3 .

Правило вывода

Правило вывода – это способ выразить :

${\frac {\phi ,\ \phi \to \chi }{\chi }}$.

Пример доказательства в другой аксиоматической системе

Ниже приведен пример (синтаксической) демонстрации, включающий только аксиомы THEN-1 и THEN-2 :

Доказывать: $A\to A$ (Рефлексивность импликации).

Доказательство:

1. $(A\to ((B\to A)\to A))\to ((A\to (B\to A))\to (A\to A))$

   Аксиома ТОГДА-2 с $\phi =A,\chi =B\to A,\psi =A$

2. $A\to ((B\to A)\to A)$

   Аксиома ТОГДА-1 с $\phi =A,\chi =B\to A$

3. $(A\to (B\to A))\to (A\to A)$

   Из (1) и (2) по modus ponens.

4. $A\to (B\to A)$

   Аксиома ТОГДА-1 с $\phi =A,\chi =B$

5. $A\to A$

   Из (3) и (4) по modus ponens.

Металогика

Пусть демонстрация представлена ​​последовательностью, в которой гипотезы располагаются слева от турникета , а выводы — справа от турникета. Тогда теорему о дедукции можно сформулировать следующим образом:

Если последовательность

$\phi _{1},\ \phi _{2},\ ...,\ \phi _{n},\ \chi \vdash \psi$

было продемонстрировано, то можно также продемонстрировать последовательность

$\phi _{1},\ \phi _{2},\ ...,\ \phi _{n}\vdash \chi \to \psi$.

Эта теорема о выводе (DT) сама по себе не сформулирована с помощью исчисления высказываний: это не теорема об исчислении высказываний, а теорема об исчислении высказываний. В этом смысле это метатеорема , сравнимая с теоремами о правильности или полноте исчисления высказываний.

С другой стороны, DT настолько полезен для упрощения процесса синтаксического доказательства, что его можно рассматривать и использовать как еще одно правило вывода, сопровождающее modus ponens. В этом смысле DT соответствует естественному правилу вывода условного доказательства , которое является частью первой версии исчисления высказываний, представленной в этой статье.

Обратное DT также справедливо:

Если последовательность

$\phi _{1},\ \phi _{2},\ ...,\ \phi _{n}\vdash \chi \to \psi$

было продемонстрировано, то можно также продемонстрировать последовательность

$\phi _{1},\ \phi _{2},\ ...,\ \phi _{n},\ \chi \vdash \psi$

на самом деле, справедливость обратного DT почти тривиальна по сравнению с DT:

Если

$\phi _{1},\ ...,\ \phi _{n}\vdash \chi \to \psi$

затем

1: $\phi _{1},\ ...,\ \phi _{n},\ \chi \vdash \chi \to \psi$

2: $\phi _{1},\ ...,\ \phi _{n},\ \chi \vdash \chi$

и из (1) и (2) можно вывести

3: $\phi _{1},\ ...,\ \phi _{n},\ \chi \vdash \psi$

посредством модус-полагания, QED

Обратное DT имеет важные последствия: его можно использовать для преобразования аксиомы в правило вывода. Например, по аксиоме И-1 имеем:

$\vdash \phi \wedge \chi \to \phi ,$

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

$\phi \wedge \chi \vdash \phi ,$

что говорит нам о том, что правило вывода

${\frac {\phi \wedge \chi }{\phi }}$

допустимо ​ . Это правило вывода — исключение конъюнктуры , одно из правил вывода, используемых в естественной дедукции .

Консервативные расширения

В систему аксиом логики принято включать только аксиомы импликации и отрицания. Учитывая эти аксиомы, можно сформировать консервативные расширения теоремы о дедукции , допускающие использование дополнительных связок. Эти расширения называются консервативными, потому что если формула φ, включающая новые связки, переписана как логически эквивалентная формула θ, включающая только отрицание, импликацию и универсальную квантификацию, то φ выводима в расширенной системе тогда и только тогда, когда θ выводима в исходной системе. . В полном расширении аксиоматическая система будет больше напоминать систему естественной дедукции .

Экзистенциальная количественная оценка

• Введение

$\forall x(\phi \to \exists y(\phi [x:=y]))$

• Устранение

$\forall x(\phi \to \psi )\to \exists x(\phi )\to \psi$ где $x$ не является свободной переменной $\psi$.

Соединение и дизъюнкция

• Введение и устранение союза

введение: $\alpha \to (\beta \to \alpha \land \beta )$

удаление осталось: $\alpha \wedge \beta \to \alpha$

право на удаление: $\alpha \wedge \beta \to \beta$

• Введение и устранение дизъюнкции

вступление осталось: $\alpha \to \alpha \vee \beta$

введение справа: $\beta \to \alpha \vee \beta$

устранение: $(\alpha \to \gamma )\to ((\beta \to \gamma )\to \alpha \vee \beta \to \gamma )$

Метатеоремы

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

Некоторые распространенные метатеоремы этой формы:

• Теорема о дедукции : $\Gamma ;\phi \vdash \psi$ тогда и только тогда, когда $\Gamma \vdash \phi \to \psi$.
• $\Gamma \vdash \phi \leftrightarrow \psi$ тогда и только тогда, когда $\Gamma \vdash \phi \to \psi$ и $\Gamma \vdash \psi \to \phi$.
• Противопоставление: Если $\Gamma ;\phi \vdash \psi$ затем $\Gamma ;\lnot \psi \vdash \lnot \phi$.
• Обобщение : если $\Gamma \vdash \phi$ и x не встречается в свободном виде ни в одной формуле $\Gamma$ затем $\Gamma \vdash \forall x\phi$.

Некоторые полезные теоремы и их доказательства

Ниже приведены несколько теорем логики высказываний , а также их доказательства (или ссылки на эти доказательства в других статьях). Обратите внимание: поскольку (P1) само по себе можно доказать, используя другие аксиомы, фактически (P2), (P3) и (P4) достаточно для доказательства всех этих теорем.

(HS1) $(q\to r)\to ((p\to q)\to (p\to r))$ - Гипотетический силлогизм , см . доказательство .

(Л1) $p\to ((p\to q)\to q)$ - доказательство:

(1) $((p\to q)\to (p\to q))\to (((p\to q)\to p)\to ((p\to q)\to q))$ (пример (P3))

(2) $(p\to q)\to (p\to q)$ (пример (P1))

(3) $((p\to q)\to p)\to ((p\to q)\to q)$ (из (2) и (1) по modus ponens )

(4) $(((p\to q)\to p)\to ((p\to q)\to q))\to ((p\to ((p\to q)\to p))\to (p\to ((p\to q)\to q)))$ (пример (HS1))

(5) $(p\to ((p\to q)\to p))\to (p\to ((p\to q)\to q))$ (из (3) и (4) по modus ponens)

(6) $p\to ((p\to q)\to p)$ (пример (P2))

(7) $p\to ((p\to q)\to q)$ (из (6) и (5) по modus ponens)

Следующие две теоремы вместе известны как двойное отрицание :

(ДН1) $\neg \neg p\to p$

(ДН2) $p\to \neg \neg p$

Смотрите доказательства .

(Л2) $(p\to (q\to r))\to (q\to (p\to r))$ - для этого доказательства мы используем метод метатеоремы гипотетического силлогизма как сокращение для нескольких шагов доказательства:

(1) $(p\to (q\to r))\to ((p\to q)\to (p\to r))$ (пример (P3))

(2) $((p\to q)\to (p\to r))\to ((q\to (p\to q))\to (q\to (p\to r)))$ (пример (HS1))

(3) $(p\to (q\to r))\to ((q\to (p\to q))\to (q\to (p\to r)))$ (из (1) и (2) с использованием метатеоремы гипотетического силлогизма)

(4) $((p\to (q\to r))\to ((q\to (p\to q))\to (q\to (p\to r))))\to (((p\to (q\to r))\to (q\to (p\to q)))\to ((p\to (q\to r))\to (q\to (p\to r))))$ (пример (P3))

(5) $((p\to (q\to r))\to (q\to (p\to q)))\to ((p\to (q\to r))\to (q\to (p\to r)))$ (из (3) и (4) с использованием modus ponens)

(6) $q\to (p\to q)$ (пример (P2))

(7) $(q\to (p\to q))\to ((p\to (q\to r))\to (q\to (p\to q)))$ (пример (P2))

(8) $(p\to (q\to r))\to (q\to (p\to q))$ (из (6) и (7) с использованием modus ponens)

(9) $(p\to (q\to r))\to (q\to (p\to r))$ (из (8) и (5) с использованием modus ponens)

(HS2) $(p\to q)\to ((q\to r)\to (p\to r))$ — альтернативная форма гипотетического силлогизма . доказательство:

(1) $(q\to r)\to ((p\to q)\to (p\to r))$ (пример (HS1))

(2) $((q\to r)\to ((p\to q)\to (p\to r)))\to ((p\to q)\to ((q\to r)\to (p\to r)))$ (пример (L2))

(3) $(p\to q)\to ((q\to r)\to (p\to r))$ (из (1) и (2) по modus ponens)

(ТР1) $(p\to q)\to (\neg q\to \neg p)$ - Транспонирование, см. доказательство (другое направление транспонирования — (P4)).

(ТР2) $(\neg p\to q)\to (\neg q\to p)$ - другая форма транспозиции; доказательство:

(1) $(\neg p\to q)\to (\neg q\to \neg \neg p)$ (экземпляр (TR1))

(2) $\neg \neg p\to p$ (экземпляр (DN1))

(3) $(\neg \neg p\to p)\to ((\neg q\to \neg \neg p)\to (\neg q\to p))$ (пример (HS1))

(4) $(\neg q\to \neg \neg p)\to (\neg q\to p)$ (из (2) и (3) по modus ponens)

(5) $(\neg p\to q)\to (\neg q\to p)$ (из (1) и (4) с использованием метатеоремы гипотетического силлогизма)

(Л3) $(\neg p\to p)\to p$ - доказательство:

(1) $\neg p\to (\neg \neg (q\to q)\to \neg p)$ (пример (P2))

(2) $(\neg \neg (q\to q)\to \neg p)\to (p\to \neg (q\to q))$ (пример (P4))

(3) $\neg p\to (p\to \neg (q\to q))$ (из (1) и (2) с использованием метатеоремы гипотетического силлогизма)

(4) $(\neg p\to (p\to \neg (q\to q)))\to ((\neg p\to p)\to (\neg p\to \neg (q\to q)))$ (пример (P3))

(5) $(\neg p\to p)\to (\neg p\to \neg (q\to q))$ (из (3) и (4) с использованием мод ponens)

(6) $(\neg p\to \neg (q\to q))\to ((q\to q)\to p)$ (пример (P4))

(7) $(\neg p\to p)\to ((q\to q)\to p)$ (из (5) и (6) с использованием метатеоремы гипотетического силлогизма)

(8) $q\to q$ (пример (P1))

(9) $(q\to q)\to (((q\to q)\to p)\to p)$ (пример (L1))

(10) $((q\to q)\to p)\to p$ (из (8) и (9) с использованием мод ponens)

(11) $(\neg p\to p)\to p$ (из (7) и (10) с использованием метатеоремы гипотетического силлогизма)

См. также

• Список аксиоматических систем логики
• Естественный вычет
• Переписка Карри-Ховарда
• Комбинаторная логика

Ссылки

• Карри, Хаскелл Б.; Роберт Фейс (1958). Комбинаторная логика Vol. Я. ​Том. 1. Амстердам: Северная Голландия.
• Монк, Дж. Дональд (1976). Математическая логика . Тексты для аспирантов по математике. Берлин, Нью-Йорк: Springer-Verlag . ISBN  978-0-387-90170-1 .
• Ружа, Имре; Мате, Андраш (1997). Введение в современную логику (на венгерском языке). Будапешт: Издательство Осирис.
• Тарский, Альфред (1990). Доказательство и правда (на венгерском языке). Будапешт: Мысль. Это венгерский перевод избранных статей Альфреда Тарского по семантической теории истины .
• Дэвид Гильберт (1927) «Основы математики», перевод Стефана Бауэра-Менглерберга и Дагфинна Фёллесдала (стр. 464–479). в:
  • ван Хейеноорт, Жан (1967). От Фреге до Гёделя: Справочник по математической логике, 1879–1931 (3-е издание, 1976 г., изд.). Кембридж, Массачусетс: Издательство Гарвардского университета. ISBN  0-674-32449-8 .
  • В книге Гильберта 1927 года, основанной на более ранней лекции «Основы» 1925 года (стр. 367–392), представлены его 17 аксиом - аксиомы импликации № 1–4, аксиомы о & и V № 5–10, аксиомы отрицания № 11- 12, его логическая ε-аксиома № 13, аксиомы равенства № 14–15 и аксиомы № 16–17, а также другие необходимые элементы его формалистической «теории доказательства» – например, аксиомы индукции, аксиомы рекурсии, и т. д; он также предлагает энергичную защиту против интуиционизма Л. Дж. Брауэра. См. также комментарии и опровержения Германа Вейля (1927) (стр. 480–484), приложение Пола Бернея (1927) к лекции Гильберта (стр. 485–489) и ответ Луицена Эгбертуса Яна Брауэра (1927) (стр. 490–495).
• Клини, Стивен Коул (1952). Введение в метаматематику (10-е издание с исправлениями 1971 г., изд.). Амстердам, штат Нью-Йорк: Издательская компания Северной Голландии. ISBN  0-7204-2103-9 .
  • См., в частности, главу IV «Формальная система» (стр. 69–85), в которой Клини представляет подразделы §16 Формальные символы, §17 Правила формирования, §18 Свободные и связанные переменные (включая замену), §19 Правила преобразования (например, modus ponens) — и из них он представляет 21 «постулат» — 18 аксиом и 3 отношения «непосредственных последствий», разделенных следующим образом: Постулаты для исчисления высказываний № 1–8, Дополнительные постулаты для исчисления предикатов № 9–12 и Дополнительные постулаты для исчисления предикатов № 9–12 и Дополнительные постулаты для исчисления высказываний № 9–12. теория чисел № 13-21.

Внешние ссылки

• Гейфман, Хаим. «Дедуктивная система типа Гильберта для логики предложений, полноты и компактности» (PDF) .
• Фармер, В.М. «Пропозициональная логика» (PDF) . Он описывает (среди прочего) часть системы дедукции в стиле Гильберта (ограниченной исчислением высказываний ).