Естественный вычет

В логике и теории доказательств естественная дедукция — это своего рода исчисление доказательств , в котором логические рассуждения выражаются правилами вывода, тесно связанными с «естественным» способом рассуждения. ^{[ 1 ]} Это контрастирует с системами в стиле Гильберта , которые вместо этого используют аксиомы в максимально возможной степени для выражения логических законов дедуктивного рассуждения .

История

Естественная дедукция выросла из контекста неудовлетворенности аксиоматизациями дедуктивного рассуждения, общими для систем Гильберта , Фреге и Рассела (см., например, систему Гильберта ). Такие аксиоматизации наиболее широко использовались Расселом и Уайтхедом в их математическом трактате Principia Mathematica . Вдохновленный серией семинаров Лукасевича в Польше в 1926 году , которые выступали за более естественную трактовку логики, Ясковский предпринял первые попытки определить более естественную дедукцию, сначала в 1929 году, используя схематические обозначения, а затем обновив свое предложение в последовательности. статей 1934 и 1935 годов. ^{[ 2 ]} Его предложения привели к различным обозначениям. такие как исчисление в стиле Фитча (или диаграммы Фитча) или Суппеса метод , для которого Леммон предложил вариант, теперь известный как нотация Суппеса-Леммона .

Естественная дедукция в ее современной форме была независимо предложена немецким математиком Герхардом Генценом в 1933 году в диссертации, представленной на факультете математических наук Геттингенского университета . ^{[ 3 ]} Термин «естественная дедукция» (или, скорее, его немецкий эквивалент natürliches Schließen ) был придуман в этой статье:

Прежде всего, я хотел создать формализм, максимально приближенный к реальным рассуждениям. Это привело к «исчислению естественного рассуждения». ^{[ 4 ]}

Сначала я хотел построить формализм, максимально приближенный к реальным рассуждениям. Так возникло «исчисление естественной дедукции».

Генценом двигало желание установить непротиворечивость теории чисел . Ему не удалось доказать основной результат, необходимый для получения результата о непротиворечивости, — теорему об исключении разреза — Хауптзац — непосредственно для естественной дедукции. По этой причине он представил свою альтернативную систему, секвенциальное исчисление , для которого доказал хауптзац как для классической , так и для интуиционистской логики . В серии семинаров в 1961 и 1962 годах Правиц дал исчерпывающее изложение естественного дедуктивного исчисления и перенес большую часть работы Генцена с секвенционным исчислением в структуру естественной дедукции. Его монография 1965 года « Естественная дедукция: теоретико-доказательное исследование». ^{[ 5 ]} должен был стать справочником по естественной дедукции и включать приложения для модальной логики и логики второго порядка .

При естественной дедукции предложение выводится из набора посылок путем многократного применения правил вывода. Система, представленная в этой статье, представляет собой небольшую вариацию формулировки Генцена или Правица, но с более близким описанием Мартина-Лёфа . логических суждений и связок ^{[ 6 ]}

История стилей обозначений

Естественная дедукция имела большое разнообразие стилей записи. ^{[ 7 ]} что может затруднить распознавание доказательства, если вы не знакомы с одним из них. Чтобы помочь в этой ситуации, в этой статье есть раздел § «Обозначения», объясняющий, как читать все обозначения, которые в действительности будут использоваться. В этом разделе просто объясняется историческая эволюция стилей обозначений, большинство из которых не могут быть показаны, поскольку нет иллюстраций, доступных под публичной лицензией авторских прав – читателю указываются на SEP и IEP для изображений.

Генцен изобрел естественную дедукцию, используя доказательства в форме дерева - см. в § Обозначении дерева Генцена . подробности
Ясковский изменил это на обозначение, в котором использовались различные вложенные блоки. ^{[ 7 ]}
Fitch изменило метод Ясковского для построения ячеек, создав обозначение Fitch . ^{[ 7 ]}
1940: В учебнике Куайна ^{[ 8 ]} указал предшествующие зависимости номерами строк в квадратных скобках, предвосхищая обозначение номеров строк Суппеса 1957 года.
1950: В учебнике Куайн (1982 , стр. 241–255) продемонстрировал метод использования одной или нескольких звездочек слева от каждой строки доказательства для обозначения зависимостей. Это эквивалентно вертикальным полосам Клини. (Не совсем ясно, появилась ли звездочка Куайна в оригинальном издании 1950 года или была добавлена в более позднем издании.)
1957: Введение в практическое доказательство логических теорем в учебнике Суппеса (1999 , стр. 25–150). Это обозначало зависимости (т.е. предшествующие предложения) по номерам строк слева от каждой строки.
1963: Столл (1979 , стр. 183–190, 215–219) использует наборы номеров строк для обозначения предшествующих зависимостей строк последовательных логических аргументов, основанных на правилах естественного вывода.
1965: Весь учебник Леммона (1965) представляет собой введение в логические доказательства с использованием метода, основанного на методе Суппеса , который теперь известен как нотация Суппеса-Леммона .
1967: В учебнике Клини (2002 , стр. 50–58, 128–130) кратко продемонстрировала два вида практических логических доказательств: одна система использует явные кавычки предшествующих утверждений слева от каждой строки, другая система использует вертикальную черту. -линии слева для обозначения зависимостей. ^{[ а ]}

Обозначения

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

Нотационные варианты связок ^{[ 9 ]}^{[ 10 ]}
Соединительный	Символ
И	$A\land B$ , $A\cdot B$ , $AB$ , $A\&B$ , $A\&\&B$
эквивалент	$A\equiv B$ , $A\Leftrightarrow B$ , $A\leftrightharpoons B$
подразумевает	$A\Rightarrow B$ , $A\supset B$ , $A\rightarrow B$
NAND	$A{\overline {\land }}B$ , $A\mid B$ , ${\overline {A\cdot B}}$
неэквивалентный	$A\not \equiv B$ , $A\not \Leftrightarrow B$ , $A\nleftrightarrow B$
НИ	$A{\overline {\lor }}B$ , $A\downarrow B$ , ${\overline {A+B}}$
НЕТ	$\neg A$ , $-A$ , ${\overline {A}}$ , $\sim A$
ИЛИ	$A\lor B$ , $A+B$ , $A\mid B$ , $A\parallel B$
ИСНО-ИЛИ	$A$ ИСНО-ИЛИ $B$
БЕСПЛАТНО	$A{\underline {\lor }}B$ , $A\oplus B$

Обозначение дерева Генцена

Генцен , изобретший естественную дедукцию, имел свой собственный стиль записи аргументов. Это будет проиллюстрировано простым аргументом ниже. Допустим, у нас есть простой пример аргумента в логике высказываний , например: «если идет дождь, то облачно; идет дождь; следовательно, облачно». (Это in modus ponens .) Если представить это в виде списка предложений, как обычно, мы получим:

1)~P\to Q

2)~P

\therefore ~Q

В обозначениях Генцена ^{[ 7 ]} это будет написано так:

{\frac {P\to Q,P}{Q}}

Помещения показаны над линией, называемой линией вывода . ^{[ 11 ]}^{[ 12 ]} разделяются запятой , что указывает на совмещение помещений. ^{[ 13 ]} Заключение пишется под линией вывода. ^{[ 11 ]} Линия вывода представляет синтаксическое следствие , ^{[ 11 ]} иногда называют дедуктивным следствием , ^{[ 14 ]} который также обозначается знаком ⊢. ^{[ 15 ]}^{[ 14 ]} Таким образом, вышеизложенное также можно записать в одну строку как $P\to Q,P\vdash Q$ . (С точки зрения синтаксиса турникет имеет более низкий приоритет, чем запятая, которая представляет собой комбинацию посылок, которая, в свою очередь, имеет более низкий приоритет, чем стрелка, используемая для материальной импликации; поэтому для интерпретации этой формулы не нужны круглые скобки.) ^{[ 13 ]}

Синтаксическое последствие противопоставляется семантическому последствию . ^{[ 16 ]} который обозначается ⊧. ^{[ 15 ]}^{[ 14 ]} В этом случае вывод следует синтаксически, поскольку естественная дедукция представляет собой синтаксическую систему доказательства , которая предполагает правила вывода как примитивы .

Стиль Генцена будет использован в большей части этой статьи. Генценовских аннотаций, используемых для интернализации гипотетических суждений, можно избежать, представляя доказательства в виде дерева секвенций Γ ⊢A вместо дерева суждений о том, что A (истинно).

Обозначение Суппеса – Леммона

Во многих учебниках используются обозначения Суппеса-Леммона . ^{[ 7 ]} так что эта статья также даст это – хотя на данный момент это включено только для пропозициональной логики , а остальная часть освещения дается только в стиле Генцена. Доказательство , , оформленное в соответствии со стилем нотации Суппеса-Леммона , представляет собой последовательность строк, содержащих предложения ^{[ 17 ]} где каждое предложение является либо предположением, либо результатом применения правила доказательства к предыдущим предложениям в последовательности. ^{[ 17 ]} Каждая строка доказательства состоит из предложения доказательства вместе с его аннотацией , набором предположений и текущим номером строки . ^{[ 17 ]} В наборе предположений перечислены предположения, от которых зависит данное предложение доказательства, на которые ссылаются номера строк. ^{[ 17 ]} Аннотация указывает, какое правило доказательства было применено и к каким предыдущим строкам было получено текущее предложение. ^{[ 17 ]} Вот пример доказательства:

Доказательство в стиле Суппеса-Леммона (первый пример)
Успенский набор	Номер строки	Доказательное предложение	Аннотация
1	1	$P\to Q$	А
2	2	$-Q$	А
3	3	$P$	А
1 , 3	4	$Q$	1 , 3 →E
1 , 2	5	$-P$	2 , 4 РАА

Это доказательство станет яснее, когда будут указаны правила вывода и соответствующие аннотации к ним - см. § Правила пропозиционального вывода (стиль Суппеса-Леммона) .

Синтаксис пропозиционального языка

В этом разделе определяется формальный синтаксис языка пропозициональной логики , противопоставляя распространенные способы сделать это способу в стиле Генцена.

Общие стили определений

Формальный язык ${\mathcal {L}}$ исчисления высказываний обычно определяется рекурсивным определением , например, данным Бостоком : ^{[ 18 ]}

Каждое предложение-буква представляет собой формулу .
" $\top$ " и " $\bot$ " являются формулами.
Если $\varphi$ это формула, так что $\neg \varphi$ .
Если $\varphi$ и $\psi$ являются формулами, таковы $(\varphi \land \psi )$ , $(\varphi \lor \psi )$ , $(\varphi \to \psi )$ , $(\varphi \leftrightarrow \psi )$ .
Ничто иное не является формулой.

Есть и другие способы сделать это, например, грамматика BNF. $\phi ::=a_{1},a_{2},\ldots ~|~\neg \phi ~|~\phi ~\&~\psi ~|~\phi \vee \psi ~|~\phi \rightarrow \psi ~|~\phi \leftrightarrow \psi$ . ^{[ 19 ]}^{[ 20 ]}

Определение стиля Генцена

Определение синтаксиса также можно дать, используя § обозначение дерева Генцена , написав правильно построенные формулы под линией вывода и любые схематические переменные, используемые этими формулами над ней. ^{[ 20 ]} Например, эквивалент правил 3 и 4 из определения Бостока, приведенного выше, записывается следующим образом:

{\frac {\varphi }{(\neg \varphi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \lor \psi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \land \psi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \rightarrow \psi )}}\quad {\frac {\varphi \quad \psi }{(\varphi \leftrightarrow \psi )}}

.

Другая система обозначений рассматривает синтаксис языка как категориальную грамматику с единственной категорией «формула», обозначаемой символом ${\mathcal {F}}$ . Таким образом, любые элементы синтаксиса вводятся посредством категоризации, для которой используются обозначения $\varphi :{\mathcal {F}}$ , значение " $\varphi$ является выражением объекта в категории ${\mathcal {F}}$ ." ^{[ 21 ]} Таким образом, буквы-предложения вводятся посредством таких категорий, как $P:{\mathcal {F}}$ , $Q:{\mathcal {F}}$ , $R:{\mathcal {F}}$ , и так далее; ^{[ 21 ]} связки, в свою очередь, определяются утверждениями, аналогичными приведенным выше, но с использованием нотации категоризации, как показано ниже:

**Связки, определенные через категориальную грамматику ^{[ 21 ]}**
Соединение (&)	Дизъюнкция (∨)	Значение (→)	Отрицание (¬)
${\frac {A:{\mathcal {F}}\quad B:{\mathcal {F}}}{\&(A)(B):{\mathcal {F}}}}$	${\frac {A:{\mathcal {F}}\quad B:{\mathcal {F}}}{\vee (A)(B):{\mathcal {F}}}}$	${\frac {A:{\mathcal {F}}\quad B:{\mathcal {F}}}{\supset (A)(B):{\mathcal {F}}}}$	${\frac {A:{\mathcal {F}}}{\neg (A):{\mathcal {F}}}}$

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

Пропозициональная логика в стиле Генцена

Правила вывода в стиле Генцена

Ниже приводится полный список примитивных правил вывода для естественной дедукции в классической логике высказываний: ^{[ 20 ]}

Правила классической логики высказываний
Правила введения	Правила исключения
${\begin{array}{c}\varphi \qquad \psi \\\hline \varphi \wedge \psi \end{array}}(\wedge _{i})$	${\begin{array}{c}\varphi \wedge \psi \\\hline \varphi \end{array}}(\wedge _{e})$
${\begin{array}{c}\varphi \\\hline \varphi \vee \psi \end{array}}(\vee _{i})$	${\cfrac {\varphi \vee \psi \quad {\begin{matrix}[\varphi ]^{u}\\\vdots \\\chi \end{matrix}}\quad {\begin{matrix}[\psi ]^{v}\\\vdots \\\chi \end{matrix}}}{\chi }}\ \vee _{E^{u,v}}$
${\begin{array}{c}[\varphi ]^{u}\\\vdots \\\psi \\\hline \varphi \to \psi \end{array}}(\to _{i})\ u$	${\begin{array}{c}\varphi \qquad \varphi \to \psi \\\hline \psi \end{array}}(\to _{e})$
${\begin{array}{c}[\varphi ]^{u}\\\vdots \\\bot \\\hline \neg \varphi \end{array}}(\neg _{i})\ u$	${\begin{array}{c}\varphi \qquad \neg \varphi \\\hline \bot \end{array}}(\neg _{e})$
	${\begin{array}{c}[\neg \varphi ]^{u}\\\vdots \\\bot \\\hline \varphi \end{array}}({\text{PBC}})\ u$

Эта таблица соответствует обычаю использования греческих букв в качестве схем , которые могут охватывать любые формулы, а не только атомарные предложения. Имя правила указывается справа от его дерева формул. Например, первое правило введения называется $\wedge _{i}$ , что является сокращением от «введение союза».

Примеры доказательств в стиле Генцена

В качестве примера использования правил вывода рассмотрим коммутативность конъюнкции. Если А ∧ В , то В ∧ А ; этот вывод можно сделать, составив правила вывода таким образом, чтобы посылки более низкого вывода соответствовали заключению следующего более высокого вывода.

${\cfrac {{\cfrac {A\wedge B}{B{\hbox{ }}}}\ \wedge _{E2}\qquad {\cfrac {A\wedge B}{A}}\ \wedge _{E1}}{B\wedge A}}\ \wedge _{I}$

В качестве второго примера рассмотрим вывод « A ⊃ (B ⊃ (A ∧ B)) »:

${\cfrac {{\cfrac {{\cfrac {}{A}}\ u\quad {\cfrac {}{B}}\ w}{A\wedge B}}\ \wedge _{I}}{{\cfrac {B\supset \left(A\wedge B\right)}{A\supset \left(B\supset \left(A\wedge B\right)\right)}}\ \supset _{I^{u}}}}\ \supset _{I^{w}}$

Этот полный вывод не имеет неудовлетворенных посылок; однако дополнительные производные являются гипотетическими. Например, вывод « B ⊃ (A ∧ B) » является гипотетическим с антецедентом « A » (с именем u ).

Пропозициональная логика в стиле Суппеса – Леммона

Правила вывода Суппеса – Леммона

Правила естественного вывода, созданные, в конечном счете, Генценом , приведены ниже. ^{[ 22 ]} Существует десять примитивных правил доказательства, которые представляют собой правило предположения , плюс четыре пары правил введения и исключения для бинарных связок, а также правило reductio ad adbsurdum . ^{[ 17 ]} Дизъюнктивный силлогизм можно использовать как более простую альтернативу правильному ∨-исключению, ^{[ 17 ]} а MTT и DN — это обычно заданные правила, ^{[ 22 ]} хотя они не примитивны. ^{[ 17 ]}

Список правил вывода
Имя правила	Альтернативные названия	Аннотация	Успенский набор	Заявление
Правило предположений ^{[ 22 ]}	Предположение ^{[ 17 ]}	А ^{[ 22 ]}^{[ 17 ]}	Текущий номер строки. ^{[ 17 ]}	На любой стадии аргументации вводите предложение как предположение аргумента. ^{[ 22 ]}^{[ 17 ]}
Знакомство с союзом	Введение амперсанда, ^{[ 22 ]}^{[ 17 ]} союз (CONJ) ^{[ 17 ]}^{[ 23 ]}	м, н и я ^{[ 17 ]}^{[ 22 ]}	Объединение наборов допущений в строках m и n . ^{[ 17 ]}	От $\varphi$ и $\psi$ в строках m и n сделайте вывод $\varphi ~\&~\psi$ . ^{[ 22 ]}^{[ 17 ]}
Устранение союза	Упрощение (S), ^{[ 17 ]} устранение амперсанда ^{[ 22 ]}^{[ 17 ]}	мне ^{[ 17 ]}^{[ 22 ]}	То же, что и в строке m . ^{[ 17 ]}	От $\varphi ~\&~\psi$ в строке m сделайте вывод $\varphi$ и $\psi$ . ^{[ 17 ]}^{[ 22 ]}
Введение в дизъюнкцию ^{[ 22 ]}	Дополнение (ДОБАВИТЬ) ^{[ 17 ]}	м ∨I ^{[ 17 ]}^{[ 22 ]}	То же, что и в строке m . ^{[ 17 ]}	От $\varphi$ в строке m сделайте вывод $\varphi \lor \psi$ , что бы ни $\psi$ может быть. ^{[ 17 ]}^{[ 22 ]}
Устранение дизъюнкции	Устранение клина, ^{[ 22 ]} дилемма (DL) ^{[ 23 ]}	j,k,l,m,n ∨E ^{[ 22 ]}	Линии j,k,l,m,n . ^{[ 22 ]}	От $\varphi \lor \psi$ в строке j и предположение о $\varphi$ в строке k и вывод $\chi$ от $\varphi$ в строке l и предположение о $\psi$ в строке m и вывод $\chi$ от $\psi$ в строке n сделайте вывод $\chi$ . ^{[ 22 ]}
Дизъюнктивный силлогизм	Устранение клина (∨E), ^{[ 17 ]} метод удаления и размещения (MTP) ^{[ 17 ]}	м,н ДС ^{[ 17 ]}	Объединение наборов допущений в строках m и n . ^{[ 17 ]}	От $\varphi \lor \psi$ на линии м и $-\varphi$ в строке n сделайте вывод $\psi$ ; от $\varphi \lor \psi$ на линии м и $-\psi$ в строке n сделайте вывод $\varphi$ . ^{[ 17 ]}
Устранение стрелы ^{[ 17 ]}	настройка режима (МПП), ^{[ 22 ]}^{[ 17 ]} настройка режима (МП), ^{[ 23 ]}^{[ 17 ]} условное исключение	м, н →Е ^{[ 17 ]}^{[ 22 ]}	Объединение наборов допущений в строках m и n . ^{[ 17 ]}	От $\varphi \to \psi$ в строке m и $\varphi$ в строке n сделайте вывод $\psi$ . ^{[ 17 ]}
Знакомство со стрелкой ^{[ 17 ]}	Условное доказательство (CP), ^{[ 23 ]}^{[ 22 ]}^{[ 17 ]} условное введение	п, →I (м) ^{[ 17 ]}^{[ 22 ]}	Все в предположении, заданном в строке n , за исключением m , строки, где предполагался антецедент. ^{[ 17 ]}	От $\psi$ в строке n , что следует из предположения о $\varphi$ в строке m сделайте вывод $\varphi \to \psi$ . ^{[ 17 ]}
Доведение до абсурда ^{[ 22 ]}	Косвенное доказательство (IP), ^{[ 17 ]} введение отрицания (−I), ^{[ 17 ]} устранение отрицания (-E) ^{[ 17 ]}	м, н РАА (к) ^{[ 17 ]}	Объединение наборов предположений в строках m и n , исключая k (опровергнутое предположение). ^{[ 17 ]}	Из приговора и его отрицания ^{[ б ]} в строках m и n сделайте вывод об отрицании любого предположения, появляющегося в доказательстве (в строке k ). ^{[ 17 ]}
Знакомство с двойной стрелкой ^{[ 17 ]}	Двуусловное определение ( Df ↔), ^{[ 22 ]} двуусловное введение	м, н ↔ я ^{[ 17 ]}	Объединение наборов допущений в строках m и n . ^{[ 17 ]}	От $\varphi \to \psi$ и $\psi \to \varphi$ в строках m и n сделайте вывод $\varphi \leftrightarrow \psi$ . ^{[ 17 ]}
Устранение двойной стрелки ^{[ 17 ]}	Двуусловное определение ( Df ↔), ^{[ 22 ]} двуусловное исключение	м ↔ Е ^{[ 17 ]}	То же, что и в строке m . ^{[ 17 ]}	От $\varphi \leftrightarrow \psi$ в строке m сделайте вывод либо $\varphi \to \psi$ или $\psi \to \varphi$ . ^{[ 17 ]}
Двойное отрицание ^{[ 22 ]}^{[ 23 ]}	Устранение двойного отрицания	м Ду ^{[ 22 ]}	То же, что и в строке m . ^{[ 22 ]}	От $--\varphi$ в строке m сделайте вывод $\varphi$ . ^{[ 22 ]}
Способ снятия удаления ^{[ 22 ]}	Режим подъема (MT) ^{[ 23 ]}	м, н МТТ ^{[ 22 ]}	Объединение наборов допущений в строках m и n . ^{[ 22 ]}	От $\varphi \to \psi$ в строке m и $-\psi$ в строке n сделайте вывод $-\varphi$ . ^{[ 22 ]}

Пример доказательства в стиле Суппеса – Леммона

Напомним, что пример доказательства уже был приведен при введении § обозначения Суппеса–Леммона . Это второй пример.

Доказательство в стиле Суппеса-Леммона (второй пример)
Успенский набор	Номер строки	Доказательное предложение	Аннотация
1	1	$P\lor Q$	А
2	2	$\neg P$	А
3	3	$\neg P\to \neg Q$	А
2 , 3	4	$\neg Q$	2 , 3 →E
1 , 2 , 3	5	$P$	1 , 4 и Е
1 , 3	6	$P$	2 , 5 ДНЕЙ(2)
2 , 3	7	$\neg P$	2 , 3 РАА(1)

Согласованность, полнота и нормальные формы

Теория называется непротиворечивой , если ее ложность недоказуема (из-за отсутствия предположений), и полной, если каждая теорема или ее отрицание доказуемы с использованием правил логического вывода. Это утверждения обо всей логике и обычно привязаны к некоторому понятию модели . Однако существуют локальные понятия непротиворечивости и полноты, которые представляют собой чисто синтаксическую проверку правил вывода и не требуют обращения к моделям. Первый из них — это локальная непротиворечивость, также известная как локальная сводимость, которая гласит, что любой вывод, содержащий введение связки с последующим его устранением, может быть превращен в эквивалентный вывод без этого обходного пути. Это проверка силы правил исключения: они не должны быть настолько строгими, чтобы включать знания, еще не содержащиеся в их предпосылках. В качестве примера рассмотрим союзы.

{\begin{aligned}{\cfrac {{\cfrac {{\cfrac {}{A\ }}u\qquad {\cfrac {}{B\ }}w}{A\wedge B\ }}\wedge _{I}}{A\ }}\wedge _{E1}\end{aligned}}\quad \Rightarrow \quad {\cfrac {}{A\ }}u

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

{\cfrac {}{A\wedge B\ }}u\quad \Rightarrow \quad {\begin{aligned}{\cfrac {{\cfrac {{\cfrac {}{A\wedge B\ }}u}{A\ }}\wedge _{E1}\qquad {\cfrac {{\cfrac {}{A\wedge B\ }}u}{B\ }}\wedge _{E2}}{A\wedge B\ }}\wedge _{I}\end{aligned}}

Эти понятия в точности соответствуют β-редукции (бета-редукции) и η-конверсии (эта-конверсии) в лямбда-исчислении с использованием изоморфизма Карри – Говарда . По локальной полноте мы видим, что каждый вывод можно преобразовать в эквивалентный вывод, в котором введена главная связка. Фактически, если весь вывод подчиняется такому порядку исключений, за которыми следуют введения, то он считается нормальным . При обычном выводе все исключения происходят выше введений. В большинстве логик каждый вывод имеет эквивалентный нормальный вывод, называемый нормальной формой . Существование нормальных форм обычно трудно доказать, используя только естественную дедукцию, хотя такие описания существуют в литературе, особенно Дага Правица в 1961 году. ^{[ 24 ]} Гораздо легче показать это косвенно, с помощью без разрезов секвенциального исчисления .

Расширения первого и более высокого порядка

Логика предыдущего раздела является примером односортной логики , т. е . логики с единственным типом объекта: предложениями. Было предложено множество расширений этой простой структуры; в этом разделе мы расширим его за счет второго рода индивидов или терминов . Точнее, добавим новую категорию «термин», обозначаемую ${\mathcal {T}}$ . Зафиксируем счетное множество $V$ переменных , еще один счетный набор $F$ функциональных символов и строить термы со следующими правилами формирования:

{\frac {v\in V}{v:{\mathcal {T}}}}{\hbox{ var}}_{F}

и

{\frac {f\in F\qquad t_{1}:{\mathcal {T}}\qquad t_{2}:{\mathcal {T}}\qquad \cdots \qquad t_{n}:{\mathcal {T}}}{f(t_{1},t_{2},\cdots ,t_{n}):{\mathcal {T}}}}{\hbox{ app}}_{F}

предложений мы рассматриваем третий счетный набор P предикатов Для и определяем атомарные предикаты над терминами со следующим правилом образования:

{\frac {\phi \in P\qquad t_{1}:{\mathcal {T}}\qquad t_{2}:{\mathcal {T}}\qquad \cdots \qquad t_{n}:{\mathcal {T}}}{\phi (t_{1},t_{2},\cdots ,t_{n}):{\mathcal {F}}}}{\hbox{ pred}}_{F}

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

К ним добавляется пара правил формирования, определяющих обозначение количественных предложений; один для универсальной (∀) и экзистенциальной (∃) квантификации:

{\frac {x\in V\qquad A:{\mathcal {F}}}{\forall x.A:{\mathcal {F}}}}\;\forall _{F}\qquad \qquad {\frac {x\in V\qquad A:{\mathcal {F}}}{\exists x.A:{\mathcal {F}}}}\;\exists _{F}

Квантор всеобщности имеет правила введения и исключения:

{\cfrac {\begin{array}{c}{\cfrac {}{a:{\mathcal {T}}}}{\text{ u}}\\\vdots \\{}[a/x]A\end{array}}{\forall x.A}}\;\forall _{I^{u,a}}\qquad \qquad {\frac {\forall x.A\qquad t:{\mathcal {T}}}{[t/x]A}}\;\forall _{E}

Квантор существования имеет правила введения и исключения:

{\frac {[t/x]A}{\exists x.A}}\;\exists _{I}\qquad \qquad {\cfrac {\begin{array}{cc}&\underbrace {\,{\cfrac {}{a:{\mathcal {T}}}}{\hbox{ u}}\quad {\cfrac {}{[a/x]A}}{\hbox{ v}}\,} \\&\vdots \\\exists x.A\quad &C\\\end{array}}{C}}\exists _{E^{a,u,v}}

В этих правилах обозначение [ t / x ] A означает замену t для каждого (видимого) экземпляра x в A , избегая захвата. ^{[ с ]} Как и раньше, верхние индексы в имени обозначают высвобождаемые компоненты: член a не может входить в заключение ∀I (такие члены известны как собственные переменные или параметры ), а гипотезы с именами u и v в ∃E локализованы вторая посылка в гипотетическом выводе. Хотя логика высказываний предыдущих разделов была разрешима , добавление кванторов делает логику неразрешимой.

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

{\cfrac {\begin{matrix}{\cfrac {}{p:{\mathcal {F}}}}{\hbox{ u}}\\\vdots \\A:{\mathcal {F}}\\\end{matrix}}{\forall p.A:{\mathcal {F}}}}\;\forall _{F^{u}}\qquad \qquad {\cfrac {\begin{matrix}{\cfrac {}{p:{\mathcal {F}}}}{\hbox{ u}}\\\vdots \\A:{\mathcal {F}}\\\end{matrix}}{\exists p.A:{\mathcal {F}}}}\;\exists _{F^{u}}

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

Доказательства и теория типов

До сих пор изложение естественной дедукции концентрировалось на природе предложений, не давая формального определения доказательства . Чтобы формализовать понятие доказательства, мы немного изменим представление гипотетических выводов. Мы помечаем антецеденты переменными доказательства (из некоторого счетного множества переменных V ) и украшаем последующий факт фактическим доказательством. Антецеденты или гипотезы отделяются от последующих с помощью турникета (⊢). Эту модификацию иногда называют локализованными гипотезами . На следующей диаграмме суммированы изменения.

──── u₁ ──── u₂ ... ──── u_n
 J₁      J₂          J_n
              ⋮
              J

⇒

u₁:J₁, u₂:J₂, ..., u_n:J_n ⊢ J

Совокупность гипотез будет записываться как Γ, если их точный состав не важен. Чтобы сделать доказательства явными, мы перейдем от суждения без доказательств « А » к суждению: «π есть доказательство (А) », которое символически записывается как «π : A ». При стандартном подходе доказательства задаются собственными правилами формирования суждения «π- доказательство ». Самое простое возможное доказательство — это использование помеченной гипотезы; в этом случае доказательством является сама этикетка.

u ∈ V
─────── proof-F
u proof

───────────────────── hyp
u:A ⊢ u : A

Давайте еще раз рассмотрим некоторые связки с явными доказательствами. Что касается конъюнкции, мы смотрим на правило введения ∧I, чтобы определить форму доказательств конъюнкции: они должны быть парой доказательств двух конъюнктов. Таким образом:

π₁ proof    π₂ proof
──────────────────── pair-F
(π₁, π₂) proof

Γ ⊢ π₁ : A    Γ ⊢ π₂ : B
───────────────────────── ∧I
Γ ⊢ (π₁, π₂) : A ∧ B

Правила исключения ∧E ₁ и ∧E ₂ выбирают либо левый, либо правый конъюнктив; таким образом, доказательства представляют собой пару проекций — первую ( fst ) и вторую ( snd ).

π proof
─────────── fst-F
fst π proof

Γ ⊢ π : A ∧ B
───────────── ∧E₁
Γ ⊢ fst π : A

π proof
─────────── snd-F
snd π proof

Γ ⊢ π : A ∧ B
───────────── ∧E₂
Γ ⊢ snd π : B

Что касается импликации, вводная форма локализует или связывает гипотезу, записанную с использованием λ; это соответствует разряженной этикетке. В правиле «Γ, u : A » обозначает совокупность гипотез Γ вместе с дополнительной гипотезой u .

π proof
──────────── λ-F
λu. π proof

Γ, u:A ⊢ π : B
───────────────── ⊃I
Γ ⊢ λu. π : A ⊃ B

π₁ proof   π₂ proof
─────────────────── app-F
π₁ π₂ proof

Γ ⊢ π₁ : A ⊃ B    Γ ⊢ π₂ : A
──────────────────────────── ⊃E
Γ ⊢ π₁ π₂ : B

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

Теорема о замене

Если Γ ⊢ π ₁ : A и Γ, u : A ⊢ π ₂ : B , то Γ ⊢ [π ₁ / u ] π ₂ : B.

До сих пор суждение «Г ⊢ π : А » имело чисто логическую интерпретацию. В теории типов логическое представление заменяется более вычислительным представлением объектов. Предложения в логической интерпретации теперь рассматриваются как типы , а доказательства – как программы лямбда-исчисления . Таким образом, интерпретация «π : A » такова: « программа π имеет тип A ». Логические связки также получают другое прочтение: союз рассматривается как произведение (×), импликация как функциональная стрелка (→) и т. д. Однако различия носят лишь косметический характер. Теория типов имеет естественное дедуктивное представление в терминах правил образования, введения и исключения; на самом деле читатель может легко восстановить то, что известно как простая теория типов, из предыдущих разделов.

Разница между логикой и теорией типов заключается прежде всего в смещении акцента с типов (предложений) на программы (доказательства). Теория типов главным образом заинтересована в конвертируемости или сводимости программ. Для каждого типа существуют канонические программы этого типа, которые неприводимы; они известны как канонические формы или значения . Если любую программу можно привести к каноническому виду, то теорию типов называют нормализующей (или слабо нормализующей ). Если каноническая форма единственна, то теория называется сильно нормализующей . Нормализуемость — редкая особенность большинства нетривиальных теорий типов, что сильно отличается от логического мира. (Напомним, что почти каждый логический вывод имеет эквивалентный нормальный вывод.) Обрисуем причину: в теориях типов, допускающих рекурсивные определения, можно писать программы, которые никогда не сводятся к значению; таким циклическим программам обычно можно присвоить любой тип. В частности, программа цикла имеет тип ⊥, хотя логического доказательства «⊥» не существует. По этой причине предложения как типы; Парадигма доказательств как программ работает только в одном направлении, если вообще работает: интерпретация теории типов как логики обычно дает противоречивую логику.

Пример: теория зависимых типов

Как и логика, теория типов имеет множество расширений и вариантов, включая версии первого и высшего порядка. Одна ветвь, известная как теория зависимых типов , используется в ряде систем компьютерных доказательств . Теория зависимых типов позволяет квантификаторам варьироваться по самим программам. Эти количественные типы записываются как Π и Σ вместо ∀ и ∃ и имеют следующие правила формирования:

Γ ⊢ A type    Γ, x:A ⊢ B type
───────────────────────────── Π-F
Γ ⊢ Πx:A. B type

Γ ⊢ A type  Γ, x:A ⊢ B type
──────────────────────────── Σ-F
Γ ⊢ Σx:A. B type

Эти типы являются обобщениями типов стрелок и продуктов соответственно, о чем свидетельствуют правила их введения и исключения.

Γ, x:A ⊢ π : B
──────────────────── ΠI
Γ ⊢ λx. π : Πx:A. B

Γ ⊢ π₁ : Πx:A. B   Γ ⊢ π₂ : A
───────────────────────────── ΠE
Γ ⊢ π₁ π₂ : [π₂/x] B

Γ ⊢ π₁ : A    Γ, x:A ⊢ π₂ : B
───────────────────────────── ΣI
Γ ⊢ (π₁, π₂) : Σx:A. B

Γ ⊢ π : Σx:A. B
──────────────── ΣE₁
Γ ⊢ fst π : A

Γ ⊢ π : Σx:A. B
──────────────────────── ΣE₂
Γ ⊢ snd π : [fst π/x] B

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

Поскольку теории зависимых типов допускают, что типы зависят от программ, возникает естественный вопрос: могут ли программы зависеть от типов или любой другой комбинации. На подобные вопросы существует множество ответов. Популярный подход в теории типов заключается в том, чтобы позволить программам количественно оценивать типы, также известный как параметрический полиморфизм ; существует два основных вида: если типы и программы хранятся отдельно, то получается несколько более надежная система, называемая предикативным полиморфизмом ; если различие между программой и типом размыто, получается теоретико-типовый аналог логики высшего порядка, также известный как непредикативный полиморфизм . В литературе рассматривались различные комбинации зависимости и полиморфизма, наиболее известным из которых является лямбда-куб Хенка Барендрегта .

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

Классическая и модальная логика

Для простоты представленная до сих пор логика была интуиционистской . Классическая логика расширяет интуиционистскую логику дополнительной аксиомой или принципом исключенного третьего :

Для любого предложения p истинно предложение p ∨ ¬p.

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

────────────── XM₁
A ∨ ¬A

¬¬A
────────── XM₂
A

──────── u
¬A
⋮
p
────── XM₃^{u, p}
A

(ХМ ₃ — это просто ХМ ₂ , выраженный через Е.) Такая трактовка исключенного третьего, помимо того, что она нежелательна с точки зрения пуриста, вносит дополнительные сложности в определение нормальных форм.

Сравнительно более удовлетворительная трактовка классической естественной дедукции с точки зрения только правил введения и исключения была впервые предложена Париго в 1992 году в форме классического лямбда-исчисления, называемого λμ . Ключевой идеей его подхода была замена истинно-центричного суждения A более классическим понятием, напоминающим секвенциальное исчисление : в локализованной форме вместо Γ ⊢ A он использовал Γ ⊢ Δ, причем Δ — набор предложений, подобных к Г. Г рассматривалась как конъюнкция, а Δ как дизъюнкция. Эта структура, по сути, заимствована непосредственно из классических секвенциальных исчислений , но нововведение в λμ заключалось в том, чтобы придать вычислительный смысл классическим доказательствам естественной дедукции в терминах механизма callcc или броска/перехвата, наблюдаемого в LISP и его потомках. (См. также: первоклассный контроль .)

Другое важное расширение касалось модальных и других логик, которым нужно нечто большее, чем просто базовое суждение об истине. Впервые они были описаны для алетических модальных логик S4 и S5 в стиле естественной дедукции Правицем в 1965 году: ^{[ 5 ]} и с тех пор накопили большой объем сопутствующих работ. Приведем простой пример: модальная логика S4 требует одного нового суждения « Валидное », которое является категоричным по отношению к истине:

Если «А» (верно) без предположения, что «Б» (верно), то «А действительно».

Это категорическое суждение интериоризируется как унарная связка ◻ А (читай « обязательно А ») со следующими правилами введения и исключения:

A valid
──────── ◻I
◻ A

◻ A
──────── ◻E
A

Обратите внимание, что посылка « А действительно » не имеет определяющих правил; вместо этого вместо него используется категориальное определение действительности. Этот режим становится более ясным в локализованной форме, когда гипотезы явны. Мы пишем «Ω;Γ ⊢ A », где Γ, как и раньше, содержит истинные гипотезы, а Ω содержит действительные гипотезы. Справа только одно суждение « А »; валидность здесь не требуется, поскольку «Ω ⊢ A valid » по определению то же самое, что «Ω;⋅ ⊢ A ». Формы введения и исключения тогда следующие:

Ω;⋅ ⊢ π : A
──────────────────── ◻I
Ω;⋅ ⊢ box π : ◻ A

Ω;Γ ⊢ π : ◻ A
────────────────────── ◻E
Ω;Γ ⊢ unbox π : A

Модальные гипотезы имеют свою версию правила гипотезы и теоремы о замене.

─────────────────────────────── valid-hyp
Ω, u: (A valid) ; Γ ⊢ u : A

Теорема модальной замены

этом разделе не цитируются источники В . Пожалуйста, помогите улучшить этот раздел , добавив цитаты на надежные источники . Неиспользованный материал может быть оспорен и удален . ( Май 2024 г. ) ( Узнайте, как и когда удалить это сообщение ): Если Ω?⋅ ⊢ π ₁ : A и Ω, u : ( A допустимо ) ; Γ ⊢ π ₂ : C , то Ω Γ ⊢ [π ₁ / u ] π ₂ : C ;

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

Добавление меток к формулам позволяет гораздо точнее контролировать условия применения правил, позволяя применять более гибкие методы аналитических таблиц , как это было сделано в случае дедукции с метками . Метки также позволяют давать имена мирам в семантике Крипке; Симпсон (1993) представляет влиятельную технику преобразования условий фрейма модальных логик в семантике Крипке в правила вывода при естественной формализации вывода гибридной логики . Ступпа (2004) рассматривает применение многих теорий доказательства, таких как гиперсеквенции Белнапа, Аврона и Поттинджера и логика отображения к таким модальным логикам, как S5 и B.

Сравнение с секвенциальным исчислением

Секвенциальное исчисление является главной альтернативой естественной дедукции как основе математической логики . При естественной дедукции поток информации двунаправлен: правила исключения направляют информацию вниз путем деконструкции, а правила введения направляют информацию вверх путем сборки. Таким образом, доказательство естественной дедукции не предполагает чисто восходящего или нисходящего чтения, что делает его непригодным для автоматизации поиска доказательств. Чтобы обратить внимание на этот факт, Генцен в 1935 году предложил свое секвенционное исчисление , хотя первоначально он задумывал его как технический прием для выяснения непротиворечивости логики предикатов . Клини в своей плодотворной книге 1952 года «Введение в метаматематику » дал первую формулировку секвенциального исчисления в современном стиле. ^{[ 25 ]}

В секвенциальном исчислении все правила вывода имеют исключительно восходящий смысл. Правила вывода могут применяться к элементам с обеих сторон турникета . (Чтобы отличить естественную дедукцию, в этой статье используется двойная стрелка ⇒ вместо правой кнопки ⊢ для секвенций.) Вводные правила естественной дедукции рассматриваются как правильные правила в секвенциальном исчислении и структурно очень похожи. С другой стороны, правила исключения превращаются в левые правила в секвенциальном исчислении. В качестве примера рассмотрим дизъюнкцию; правильные правила известны:

Γ ⇒ A
───────── ∨R₁
Γ ⇒ A ∨ B

Γ ⇒ B
───────── ∨R₂
Γ ⇒ A ∨ B

Слева:

Γ, u:A ⇒ C       Γ, v:B ⇒ C
─────────────────────────── ∨L
Γ, w: (A ∨ B) ⇒ C

Напомним правило естественного вывода ∨E в локализованной форме:

Γ ⊢ A ∨ B    Γ, u:A ⊢ C    Γ, v:B ⊢ C
─────────────────────────────────────── ∨E
Γ ⊢ C

Предложение A ∨ B , являющееся потомком посылки из ∨E, превращается в гипотезу заключения в левом правиле ∨L. Таким образом, левые правила можно рассматривать как своего рода перевернутое правило исключения. Это наблюдение можно проиллюстрировать следующим образом:

естественный вычет

расчеты следуют

 ────── hyp
 |
 | elim. rules
 |
 ↓
 ────────────────────── ↑↓ meet
 ↑
 |
 | intro. rules
 |
 conclusion

⇒

 ─────────────────────────── init
 ↑            ↑
 |            |
 | left rules | right rules
 |            |
 conclusion

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

────────── init
Γ, u:A ⇒ A

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

Обоснованность ⇒ относительно. ⊢: Если Γ ⇒ A , то ⊢ A. Γ
Полнота ⇒ относительно. ⊢: Если Γ ⊢ A , то ⇒ A. Γ

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

расчеты следуют

естественный вычет

Γ ⇒ π₁ : A     Γ ⇒ π₂ : B
─────────────────────────── ∧R
Γ ⇒ (π₁, π₂) : A ∧ B

Γ ⊢ π₁ : A      Γ ⊢ π₂ : B
───────────────────────── ∧I
Γ ⊢ (π₁, π₂) : A ∧ B

Однако левое правило выполняет некоторые дополнительные замены, которые не выполняются в соответствующих правилах исключения.

расчеты следуют

естественный вычет

Γ, u:A ⇒ π : C
──────────────────────────────── ∧L₁
Γ, v: (A ∧ B) ⇒ [fst v/u] π : C

Γ ⊢ π : A ∧ B
───────────── ∧E₁
Γ ⊢ fst π : A

Γ, u:B ⇒ π : C
──────────────────────────────── ∧L₂
Γ, v: (A ∧ B) ⇒ [snd v/u] π : C

Γ ⊢ π : A ∧ B
───────────── ∧E₂
Γ ⊢ snd π : B

Поэтому виды доказательств, получаемые в секвенциальном исчислении, сильно отличаются от доказательств естественной дедукции. Секвенциальное исчисление дает доказательства в так называемой β-нормальной η-длинной форме, которая соответствует каноническому представлению нормальной формы доказательства естественной дедукции. Если попытаться описать эти доказательства, используя саму естественную дедукцию, получится так называемое интеркаляционное исчисление (впервые описанное Джоном Бирнсом), которое можно использовать для формального определения понятия нормальной формы естественной дедукции.

Теорема о замене естественной дедукции принимает форму структурного правила или структурной теоремы, известной как сокращение в секвенциальном исчислении.

Вырез (замена)

Если Γ ⇒ π ₁ : A и Γ, u : A ⇒ π ₂ : C , то Γ ⇒ [π ₁ /u] π ₂ : C .

В большинстве правильных логик сокращение не является необходимым в качестве правила вывода, хотя оно остается доказуемым как метатеорема ; избыточность правила отсечения обычно представляется как вычислительный процесс, известный как исключение отсечения . Это имеет интересное применение для естественной дедукции; обычно доказывать некоторые свойства непосредственно естественным выводом крайне утомительно из-за неограниченного числа случаев. Например, рассмотрите возможность показать, что данное утверждение недоказуемо с помощью естественной дедукции. Простой индуктивный аргумент терпит неудачу из-за таких правил, как ∨E или E, которые могут вводить произвольные предложения. Однако мы знаем, что секвенциальное исчисление является полным относительно естественной дедукции, поэтому достаточно показать эту недоказуемость в секвенциальном исчислении. Теперь, если сокращение недоступно в качестве правила вывода, то все секвенциальные правила либо вводят связку справа, либо слева, поэтому глубина секвенциального вывода полностью ограничивается связками в окончательном выводе. Таким образом, доказать недоказуемость гораздо проще, поскольку необходимо рассмотреть только конечное число случаев, и каждый случай полностью состоит из подпредложений заключения. Простым примером этого является Теорема о глобальной непротиворечивости : «⋅ ⊢ ⊥» недоказуема. В версии секвенциального исчисления это явно верно, поскольку не существует правила, вывод которого мог бы иметь «⋅ ⇒ ⊥»! Из-за таких свойств теоретики доказательства часто предпочитают работать над формулировками секвентивного исчисления без разрезов.

См. также

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

Примечания

^ Особое преимущество табличных естественных систем вывода Клини состоит в том, что он доказывает справедливость правил вывода как для исчисления высказываний, так и для исчисления предикатов. См . Клини, 2002 г. , стр. 44–45, 118–119.
^ Для упрощения изложения правила слово «отрицание» здесь использовано так: отрицание формулы $\varphi$ не отрицание это $-\varphi$ , тогда как отрицание , $-\varphi$ имеет два отрицания , а именно: $\varphi$ и $--\varphi$ . ^{[ 17 ]}
^ см. в статье о лямбда-исчислении . Более подробную информацию о концепции замены

Ссылки

Общие ссылки

Баркер-Пламмер, Дэйв; Барвайз, Джон ; Этчеменди, Джон (2011). Языковое доказательство и логика (2-е изд.). Публикации CSLI. ISBN 978-1575866321 .
Галье, Жан (2005). «Конструктивная логика. Часть I: Учебное пособие по системам доказательств и типизированным λ-исчислениям» . Проверено 12 июня 2014 г.
Генцен, Герхард Карл Эрих (1934). «Исследования по логическим рассуждениям. I» . Математический журнал . 39 (2): 176–210. дои : 10.1007/BF01201353 . S2CID 121546341 . (Английский перевод «Исследования по логической дедукции у М. Е. Сабо. Собрание сочинений Герхарда Генцена. Издательство Северной Голландии», 1969.)
Генцен, Герхард Карл Эрих (1935). «Исследования по логическим рассуждениям. II» . Математический журнал . 39 (3): 405–431. дои : 10.1007/bf01201363 . S2CID 186239837 .
Жирар, Жан-Ив (1990). Доказательства и типы . Кембриджские трактаты по теоретической информатике. Издательство Кембриджского университета, Кембридж, Англия. Архивировано из оригинала 4 июля 2016 г. Проверено 20 апреля 2006 г. Перевод и приложения Пола Тейлора и Ива Лафона.
Ясковский, Станислав (1934). О правилах предположений в формальной логике . Перепечатано в польской логике 1920–39 , изд. Сторрс Макколл.
Клини, Стивен Коул (1980) [1952]. Введение в метаматематику (Одиннадцатое изд.). Северная Голландия. ISBN 978-0-7204-2103-3 .
Клини, Стивен Коул (2009) [1952]. Введение в метаматематику . Иши Пресс Интернешнл. ISBN 978-0-923891-57-2 .
Клини, Стивен Коул (2002) [1967]. Математическая логика . Минеола, Нью-Йорк: Dover Publications. ISBN 978-0-486-42533-7 .
Леммон, Эдвард Джон (1965). Начало логики . Томас Нельсон. ISBN 978-0-17-712040-4 .
Мартин-Лёф, Пер (1996). «О значениях логических констант и обоснованиях логических законов» (PDF) . Северный журнал философской логики . 1 (1): 11–60. Конспект лекций к краткому курсу в Università degli Studi di Siena, апрель 1983 г.
Пфеннинг, Фрэнк; Дэвис, Роуэн (2001). «Оценочная реконструкция модальной логики» (PDF) . Математические структуры в информатике . 11 (4): 511–540. CiteSeerX 10.1.1.43.1611 . дои : 10.1017/S0960129501003322 . S2CID 16467268 .
Правиц, Даг (1965). Естественная дедукция: Теоретико-доказательное исследование . Acta Universitatis Stockholmiensis, Стокгольмские исследования в области философии 3. Стокгольм, Гетеборг, Уппсала: Almqvist & Wicksell.
Правиц, Даг (2006) [1965]. Естественный вывод: теоретико-доказательное исследование . Минеола, Нью-Йорк: Dover Publications. ISBN 978-0-486-44655-4 .
Куайн, Уиллард Ван Орман (1981) [1940]. Математическая логика (Переработанная ред.). Кембридж, Массачусетс: Издательство Гарвардского университета. ISBN 978-0-674-55451-1 .
Куайн, Уиллард Ван Орман (1982) [1950]. Методы логики (Четвертое изд.). Кембридж, Массачусетс: Издательство Гарвардского университета. ISBN 978-0-674-57176-1 .
Симпсон, Алекс (1993). Теория доказательств и семантика интуиционистской модальной логики (PDF) . Эдинбургский университет. Кандидатская диссертация.
Столл, Роберт Рот (1979) [1963]. Теория множеств и логика . Минеола, Нью-Йорк: Dover Publications. ISBN 978-0-486-63829-4 .
Ступпа, Финики (2004). Разработка модальных теорий доказательства: случай S5 . Дрезденский университет. CiteSeerX 10.1.1.140.1858 . Магистерская диссертация.
Суппес, Патрик Полковник (1999) [1957]. Введение в логику . Минеола, Нью-Йорк: Dover Publications. ISBN 978-0-486-40687-9 .
Ван Дален, Дирк (2013) [1980]. Логика и структура . Университетский текст (5-е изд.). Лондон, Гейдельберг, Нью-Йорк, Дордрехт: Springer . дои : 10.1007/978-1-4471-4558-5 . ISBN 978-1-4471-4558-5 .

Встроенные цитаты

^ «Естественная дедукция | Интернет-энциклопедия философии» . Проверено 1 мая 2024 г.
^ Ясковский 1934 .
^ Генцен 1934 , Генцен 1935 .
^ Генцен 1934 , с. 176.
^ Jump up to: ^а ^б Правиц 1965 , Правиц 2006 .
^ Мартин-Лёф 1996 .
^ Jump up to: ^а ^б ^с ^д ^и Пеллетье, Фрэнсис Джеффри; Хейзен, Аллен (2024), «Системы естественной дедукции в логике» , в Залте, Эдвард Н.; Нодельман, Ури (ред.), Стэнфордская энциклопедия философии (изд. весны 2024 г.), Лаборатория метафизических исследований, Стэнфордский университет , получено 22 марта 2024 г.
^ Куайн (1981) . См., в частности, страницы 91–93 для обозначения номеров строк Куайна для предшествующих зависимостей.
^ Платон, Ян фон (2013). Элементы логических рассуждений (1. изд.). Кембридж: Издательство Кембриджского университета. п. 9. ISBN 978-1-107-03659-8 .
^ Вайсштейн, Эрик В. «Соединительный» . mathworld.wolfram.com . Проверено 22 марта 2024 г.
^ Jump up to: ^а ^б ^с Платон, Ян фон (2013). Элементы логических рассуждений (1. изд.). Кембридж: Издательство Кембриджского университета. стр. 9, 32, 121. ISBN. 978-1-107-03659-8 .
^ «Пропозициональная логика» . www.cs.miami.edu . Проверено 22 марта 2024 г.
^ Jump up to: ^а ^б Рестолл, Грег (2018), «Субструктурная логика» , в Залте, Эдвард Н. (редактор), Стэнфордская энциклопедия философии (изд. весной 2018 г.), Лаборатория метафизических исследований, Стэнфордский университет , получено 22 марта 2024 г.
^ Jump up to: ^а ^б ^с «Компактность | Интернет-энциклопедия философии» . Проверено 22 марта 2024 г.
^ Jump up to: ^а ^б «Темы лекций для студентов, изучающих дискретную математику» . math.colorado.edu . Проверено 22 марта 2024 г.
^ Пасо, Александр; Прегель, Фабиан (2023), «Дедуктивизм в философии математики» , в Залте, Эдвард Н.; Нодельман, Ури (ред.), Стэнфордская энциклопедия философии (изд. осенью 2023 г.), Лаборатория метафизических исследований, Стэнфордский университет , получено 22 марта 2024 г.
^ Jump up to: ^а ^б ^с ^д ^и ^ж ^г ^час ^я ^дж ^к ^л ^м ^н ^тот ^п ^д ^р ^с ^т ^в ^v ^В ^х ^и ^С ^аа ^аб ^и ^{объявление} ^но ^из ^в ^ах ^есть ^также ^и ^аль ^{являюсь} ^а ^к ^ап ^ак ^с ^как ^в ^В ^из ^хорошо ^топор ^{является} ^тот ^нет ^бб ^{до нашей эры} ^др. ^быть Аллен, Колин; Хэнд, Майкл (2022). Букварь по логике (3-е изд.). Кембридж, Массачусетс: MIT Press. ISBN 978-0-262-54364-4 .
^ Босток, Дэвид (1997). Промежуточная логика . Оксфорд: Нью-Йорк: Clarendon Press; Издательство Оксфордского университета. п. 21. ISBN 978-0-19-875141-0 .
^ Ханссон, Свен Уве; Хендрикс, Винсент Ф. (2018). Введение в формальную философию . Тексты для студентов Спрингера по философии. Чам: Спрингер. п. 38. ISBN 978-3-030-08454-7 .
^ Jump up to: ^а ^б ^с Айала-Ринкон, Маурисио; де Моура, Флавио LC (2017). Прикладная логика для компьютерщиков . Темы бакалавриата по информатике. Спрингер. стр. 2, 20. doi : 10.1007/978-3-319-51653-0 . ISBN 978-3-319-51651-6 .
^ Jump up to: ^а ^б ^с Платон, Ян фон (2013). Элементы логического рассуждения . Издательство Кембриджского университета. стр. 12–13. ISBN 978-1-107-03659-8 .
^ Jump up to: ^а ^б ^с ^д ^и ^ж ^г ^час ^я ^дж ^к ^л ^м ^н ^тот ^п ^д ^р ^с ^т ^в ^v ^В ^х ^и ^С ^аа ^аб ^и ^{объявление} ^но ^из ^в Леммон, Эдвард Джон (1998). Начало логики . Бока-Ратон, Флорида: Chapman & Hall/CRC. стр. пассим, особенно 39-40. ISBN 978-0-412-38090-7 .
^ Jump up to: ^а ^б ^с ^д ^и ^ж Артур, Ричард Т.В. (2017). Введение в логику: использование естественной дедукции, реальных аргументов, немного истории и немного юмора (2-е изд.). Питерборо, Онтарио: Broadview Press. ISBN 978-1-55481-332-2 . OCLC 962129086 .
^ См. также его книги Prawitz 1965 , Prawitz 2006 .
^ Клини 2009 , стр. 440–516. См. также Клини, 1980 .

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

Лаборео, Даниэль Клементе (август 2004 г.). «Введение в естественную дедукцию» (PDF) .
«Домино на кислоте» . Проверено 10 декабря 2023 г. Естественная дедукция в виде игры в домино
Пеллетье, Фрэнсис Джеффри. «Учебники по истории естественной дедукции и элементарной логике» (PDF) .
«Системы естественной дедукции в логике» Статья Пеллетье, Фрэнсиса Джеффри ; Хейзен, Аллен в Стэнфордской энциклопедии философии , 29 октября 2021 г.
Леви, Мишель. «Пропозициональный доказывающий» .

[9] Особое преимущество табличных естественных систем вывода Клини состоит в том, что он доказывает справедливость правил вывода как для исчисления высказываний, так и для исчисления предикатов. См . Клини, 2002 г. , стр. 44–45, 118–119.

[25] Для упрощения изложения правила слово «отрицание» здесь использовано так: отрицание формулы $\varphi$ не отрицание это $-\varphi$ , тогда как отрицание , $-\varphi$ имеет два отрицания , а именно: $\varphi$ и $--\varphi$ . ^{[ 17 ]}

[27] см. в статье о лямбда-исчислении . Более подробную информацию о концепции замены

[1] «Естественная дедукция | Интернет-энциклопедия философии» . Проверено 1 мая 2024 г.

[2] Ясковский 1934 .

[3] Генцен 1934 , Генцен 1935 .

[4] Генцен 1934 , с. 176.

[prawitz1965-5] Jump up to: ^а ^б Правиц 1965 , Правиц 2006 .

[6] Мартин-Лёф 1996 .

[SEP_NaturalDeduction-7] Jump up to: ^а ^б ^с ^д ^и Пеллетье, Фрэнсис Джеффри; Хейзен, Аллен (2024), «Системы естественной дедукции в логике» , в Залте, Эдвард Н.; Нодельман, Ури (ред.), Стэнфордская энциклопедия философии (изд. весны 2024 г.), Лаборатория метафизических исследований, Стэнфордский университет , получено 22 марта 2024 г.

[8] Куайн (1981) . См., в частности, страницы 91–93 для обозначения номеров строк Куайна для предшествующих зависимостей.

[10] Платон, Ян фон (2013). Элементы логических рассуждений (1. изд.). Кембридж: Издательство Кембриджского университета. п. 9. ISBN 978-1-107-03659-8 .

[:23-11] Вайсштейн, Эрик В. «Соединительный» . mathworld.wolfram.com . Проверено 22 марта 2024 г.

[JanVonPlato_Reasoning-12] Jump up to: ^а ^б ^с Платон, Ян фон (2013). Элементы логических рассуждений (1. изд.). Кембридж: Издательство Кембриджского университета. стр. 9, 32, 121. ISBN. 978-1-107-03659-8 .

[MiamiLogic-13] «Пропозициональная логика» . www.cs.miami.edu . Проверено 22 марта 2024 г.

[SEP_Substructural-14] Jump up to: ^а ^б Рестолл, Грег (2018), «Субструктурная логика» , в Залте, Эдвард Н. (редактор), Стэнфордская энциклопедия философии (изд. весной 2018 г.), Лаборатория метафизических исследований, Стэнфордский университет , получено 22 марта 2024 г.

[IEP_Compactness-15] Jump up to: ^а ^б ^с «Компактность | Интернет-энциклопедия философии» . Проверено 22 марта 2024 г.

[ColoradoLogic-16] Jump up to: ^а ^б «Темы лекций для студентов, изучающих дискретную математику» . math.colorado.edu . Проверено 22 марта 2024 г.

[17] Пасо, Александр; Прегель, Фабиан (2023), «Дедуктивизм в философии математики» , в Залте, Эдвард Н.; Нодельман, Ури (ред.), Стэнфордская энциклопедия философии (изд. осенью 2023 г.), Лаборатория метафизических исследований, Стэнфордский университет , получено 22 марта 2024 г.

[AllenHand-18] Jump up to: ^а ^б ^с ^д ^и ^ж ^г ^час ^я ^дж ^к ^л ^м ^н ^тот ^п ^д ^р ^с ^т ^в ^v ^В ^х ^и ^С ^аа ^аб ^и ^{объявление} ^но ^из ^в ^ах ^есть ^также ^и ^аль ^{являюсь} ^а ^к ^ап ^ак ^с ^как ^в ^В ^из ^хорошо ^топор ^{является} ^тот ^нет ^бб ^{до нашей эры} ^др. ^быть Аллен, Колин; Хэнд, Майкл (2022). Букварь по логике (3-е изд.). Кембридж, Массачусетс: MIT Press. ISBN 978-0-262-54364-4 .

[:BostockLogic-19] Босток, Дэвид (1997). Промежуточная логика . Оксфорд: Нью-Йорк: Clarendon Press; Издательство Оксфордского университета. п. 21. ISBN 978-0-19-875141-0 .

[:42-20] Ханссон, Свен Уве; Хендрикс, Винсент Ф. (2018). Введение в формальную философию . Тексты для студентов Спрингера по философии. Чам: Спрингер. п. 38. ISBN 978-3-030-08454-7 .

[:0-21] Jump up to: ^а ^б ^с Айала-Ринкон, Маурисио; де Моура, Флавио LC (2017). Прикладная логика для компьютерщиков . Темы бакалавриата по информатике. Спрингер. стр. 2, 20. doi : 10.1007/978-3-319-51653-0 . ISBN 978-3-319-51651-6 .

[:1-22] Jump up to: ^а ^б ^с Платон, Ян фон (2013). Элементы логического рассуждения . Издательство Кембриджского университета. стр. 12–13. ISBN 978-1-107-03659-8 .

[LemmonLogic-23] Jump up to: ^а ^б ^с ^д ^и ^ж ^г ^час ^я ^дж ^к ^л ^м ^н ^тот ^п ^д ^р ^с ^т ^в ^v ^В ^х ^и ^С ^аа ^аб ^и ^{объявление} ^но ^из ^в Леммон, Эдвард Джон (1998). Начало логики . Бока-Ратон, Флорида: Chapman & Hall/CRC. стр. пассим, особенно 39-40. ISBN 978-0-412-38090-7 .

[TWArthurLogic-24] Jump up to: ^а ^б ^с ^д ^и ^ж Артур, Ричард Т.В. (2017). Введение в логику: использование естественной дедукции, реальных аргументов, немного истории и немного юмора (2-е изд.). Питерборо, Онтарио: Broadview Press. ISBN 978-1-55481-332-2 . OCLC 962129086 .

[26] См. также его книги Prawitz 1965 , Prawitz 2006 .

[28] Клини 2009 , стр. 440–516. См. также Клини, 1980 .

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[ а ]

[ 9 ]

[ 10 ]

[ 11 ]

[ 12 ]

[ 13 ]

[ 14 ]

[ 15 ]

[ 16 ]

[ 17 ]

[ 18 ]

[ 19 ]

[ 20 ]

[ 21 ]

[ 22 ]

[ 23 ]

[ б ]

[ 24 ]

[ с ]

[ 25 ]

v т и Основные темы Основ математики
Mathematical logic	Peano axioms Mathematical induction Formal system Axiomatic system Hilbert system Natural deduction Mathematical proof Model theory Mathematical constructivism Modal logic List of mathematical logic topics
Set theory	Set Naive set theory Axiomatic set theory Zermelo set theory Zermelo–Fraenkel set theory Constructive set theory Descriptive set theory Determinacy Russell's paradox List of set theory topics
Type theory	Axiom of reducibility Simple type theory Dependent type theory Intuitionistic type theory Homotopy type theory Univalent foundations Girard's paradox
Category theory	Category Topos theory Category of sets Higher category theory ∞-groupoid ∞-topos theory Mathematical structuralism Glossary of category theory List of category theory topics