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

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

История

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

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

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

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

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

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

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

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

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

Обозначения

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

Нотационные варианты связок

Соединительный	Символ
И	$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$

В обозначениях Генцена это будет написано так:

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

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

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

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

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

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

Доказательство в стиле Суппеса-Леммона (первый пример)

Успенский набор	Номер строки	Доказательное предложение	Аннотация
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}}$ исчисления высказываний обычно определяется рекурсивным определением , например, данным Бостоком :

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

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

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

Интересно, что § нотацию дерева Генцена можно использовать для определения синтаксиса: путем введения обозначения «prop» для обозначения «предложение » (в данном контексте это означает правильно составленную формулу ). Правила синтаксиса можно назвать « правилами образования » связок , в отличие от « правил вывода » доказательства . Вот правило образования союза :

${\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{(A\wedge B){\hbox{ prop}}}}\ \wedge _{F}$

или, для простоты, опуская круглые скобки:

${\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{A\wedge B{\hbox{ prop}}}}\ \wedge _{F}$

А вот и другие правила формирования:

${\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{A\vee B{\hbox{ prop}}}}\ \vee _{F}\qquad {\frac {A{\hbox{ prop}}\qquad B{\hbox{ prop}}}{A\supset B{\hbox{ prop}}}}\ \supset _{F}$

${\frac {\hbox{ }}{\top {\hbox{ prop}}}}\ \top _{F}\qquad {\frac {\hbox{ }}{\bot {\hbox{ prop}}}}\ \bot _{F}\qquad {\frac {A{\hbox{ prop}}}{\neg A{\hbox{ prop}}}}\ \neg _{F}$

Остальная часть этой статьи будет посвящена самой системе доказательства естественной дедукции, используя слово «истина» (или ничего) вместо «подпорка», чтобы показать, что она дает правила вывода, а не правила формирования.

Генцена

стиле Генцена

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

Правила классической логики высказываний

Правила введения	Правила исключения
${\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}$, что является сокращением от «введение союза».

стиле Генцена

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

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

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

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

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

-Леммона

-

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

Список правил вывода

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

-Леммона

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

Доказательство в стиле Суппеса-Леммона (второй пример)

Успенский набор	Номер строки	Доказательное предложение	Аннотация
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\ {\text{true}}}}u\qquad {\cfrac {}{B\ {\text{true}}}}w}{A\wedge B\ {\text{true}}}}\wedge _{I}}{A\ {\text{true}}}}\wedge _{E1}\end{aligned}}\quad \Rightarrow \quad {\cfrac {}{A\ {\text{true}}}}u$

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

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

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

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

Краткое описание системы первого порядка

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

${\frac {v\in V}{v{\hbox{ term}}}}{\hbox{ var}}_{F}$

и

${\frac {f\in F\qquad t_{1}{\hbox{ term}}\qquad t_{2}{\hbox{ term}}\qquad \cdots \qquad t_{n}{\hbox{ term}}}{f(t_{1},t_{2},\cdots ,t_{n}){\hbox{ term}}}}{\hbox{ app}}_{F}$

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

${\frac {\phi \in P\qquad t_{1}{\hbox{ term}}\qquad t_{2}{\hbox{ term}}\qquad \cdots \qquad t_{n}{\hbox{ term}}}{\phi (t_{1},t_{2},\cdots ,t_{n}){\hbox{ prop}}}}{\hbox{ pred}}_{F}$

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

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

${\frac {x\in V\qquad A{\hbox{ prop}}}{\forall x.A{\hbox{ prop}}}}\;\forall _{F}\qquad \qquad {\frac {x\in V\qquad A{\hbox{ prop}}}{\exists x.A{\hbox{ prop}}}}\;\exists _{F}$

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

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

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

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

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

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

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

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

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

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

──── u 1 ──── u 2 ... ──── u n Д 1 Д 2 Д н ⋮ Дж

⇒

ты 1 :J 1 , ты 2 :J 2 , ..., ты п :J n ⊢ J

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

ты € V ─────── доказательство-F ты доказательство

───────────────────── хайп u: Истина ⊢ u : Истина

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

π 1 доказательство π 2 доказательство ──────────────────── пара-F (π 1 , π 2 ) доказательство

Г ⊢ π 1 : А Г ⊢ π 2 : B ─────────────────────────── ∧I Г ⊢ (π 1 , π 2 ) : А ∧ B

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

π доказательство ─────────── fst -F первое π доказательство		Г ⊢ π : А ∧ B ───────────── ∧E 1 Γ ⊢ fst π : A
π доказательство ─────────── snd -F snd π доказательство		Г ⊢ π : А ∧ B ─────────────∧E 2 Γ ⊢ snd π : B

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

р доказательство ───────────── λ-F лу. р доказательство		C, и:А ⊢ π : B ────────────────── ⊃I C ⊢ λu. π : А ⊃ Б
π 1 доказательство π 2 доказательство ───────────────────app-F π 1 π 2 доказательство		Г ⊢ π 1 : А ⊃ B Γ ⊢ π 2 : А ──────────────────────────────── ⊃E C ⊢ π 1 π 2 : B

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

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

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

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

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

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

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

Γ ⊢ A тип Γ, x:A ⊢ B тип ──────────────────────────────── П-Ф C ⊢ Πx:A. Тип Б

Γ ⊢ A тип Γ, x:A ⊢ B тип ───────────────────────────────── Σ-F C ⊢ Σx:A. Тип Б

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

C, x:A ⊢ π: B Я С ⊢ λx. π : Πx:A. Б

Г ⊢ π 1 : Πx:A. B C ⊢ π 2 : А ────────────────────────────┄ C ⊢ π 1 π 2 : [π 2 /x] B

Γ ⊢ π 1 : A Γ, x:A ⊢ π 2 : B - Г ⊢ (π 1 , π 2 ) : Σx:A. Б

C ⊢ π : Σx:A. Б ────────────────── ИН 1 Γ ⊢ fst π : A

C ⊢ π : Σx:A. Б ──────────────────────────── Φ 2 Γ ⊢ snd π : [ fst π/x] B

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

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

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

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

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

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

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

────────────── XM 1 А ∨ ¬А правда

¬¬Правда ────────── ХМ 2 Правда

──────── ты ¬Правда ⋮ п правда ────── ХМ 3 вверх Правда

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

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

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

Если «А истинно» при отсутствии предположений вида «Б истинно», то «А достоверно».

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

Действительный ──────── ◻Я ◻ Правда

◻ Правда ──────── ◻E Правда

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

Ω;⋅ ⊢ π: истинное ───────────────────── ◻Я Ω;⋅ ⊢ ящик π : ◻ Истина

Oh?C ⊢ π : ◻ Правда ───────────────────────── ◻E О, C ⊢ распаковать π: правда ?

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

───────────────────────────────── valid-hyp Ω, u: (А допустимо) ; Γ ⊢ u : истинное

замены

Если Ω;⋅ ⊢ π ₁ : A true и Ω, u : ( A valid ) ; Γ ⊢ π ₂ : C true , то Ω;Γ ⊢ [π ₁ / u ] π ₂ : C true .

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

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

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

Основная статья: Секвенционное исчисление

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

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

С ⇒ А ───────── ∨R 1 С ⇒ А ∨ Б

В ⇒ Б ─────────∨R 2 С ⇒ А ∨ Б

Слева:

С, и:А ⇒ С С, v:B ⇒ С ────────────────────────────── ∨L C, w: (A ∨ B) ⇒ C

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

Γ ⊢ A ∨ B Γ, u:A ⊢ C Γ, v:B ⊢ C - Э С ⊢ С

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

естественный вычет		расчеты следуют
────── хайп | | элим. правила | ↓ ─────────────────────── ↑↓ встреча ↑ | | вступление. правила | заключение	⇒	──────────────────────────── init ↑ ↑ | | | левые правила | правильные правила | | заключение

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

─────────── инициализация С, и: А ⇒ А

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

Обоснованность ⇒ относительно. ⊢

Если Γ ⇒ A , то ⊢ A. Γ

Полнота ⇒ относительно. ⊢

Если Γ ⊢ A , то Γ A. ⇒

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

расчеты следуют		естественный вычет
С ⇒ π 1 : А С ⇒ π 2 : В ───────────────────────────── ∧R C ⇒ (π 1 , π 2 ) : А ∧ B		Г ⊢ π 1 : А Г ⊢ π 2 : B ─────────────────────────── ∧I Г ⊢ (π 1 , π 2 ) : А ∧ B

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

расчеты следуют		естественный вычет
Γ, и:А ⇒ π:C - Γ, v: (A ∧ B) ⇒ [ fst v/u] π : C		Г ⊢ π : А ∧ B ───────────── ∧E 1 Γ ⊢ fst π : A
C, и: B ⇒ π : C ─────────────────────────────────── ∧L 2 C, v: (A ∧ B) ⇒ [ snd v/u] π : C		Г ⊢ π : А ∧ B ─────────────∧E 2 Γ ⊢ snd π : B

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

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

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

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

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

См. также

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

Ссылки

Общие ссылки

• Баркер-Пламмер, Дэйв; Барвайз, Джон ; Этчеменди, Джон (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. Конспект лекций к краткому курсу в Университете Студи ди Сиены, апрель 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 .

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

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