В логике и теории доказательств естественная дедукция — это разновидность исчисления доказательств , в которой логические рассуждения выражаются правилами вывода, тесно связанными с «естественным» способом рассуждения. [1] Это контрастирует с системами в стиле Гильберта , которые вместо этого используют аксиомы в максимально возможной степени для выражения логических законов дедуктивного рассуждения .
Естественная дедукция возникла из контекста неудовлетворенности аксиоматизациями дедуктивного рассуждения, общими для систем Гильберта , Фреге и Рассела (см., например, система Гильберта ). Такие аксиоматизации были наиболее известны в математическом трактате Рассела и Уайтхеда Principia Mathematica . Под влиянием серии семинаров, проведенных Лукасевичем в Польше в 1926 году , на которых отстаивалась более естественная трактовка логики, Яськовский предпринял самые ранние попытки определить более естественную дедукцию, сначала в 1929 году, используя диаграммную нотацию, а затем обновил свое предложение в серии статей в 1934 и 1935 годах. [2] Его предложения привели к появлению различных нотаций, таких как исчисление в стиле Фитча (или диаграммы Фитча) или метод Суппеса , для которого Леммон предложил вариант, теперь известный как нотация Суппеса–Леммона .
Естественная дедукция в ее современной форме была независимо предложена немецким математиком Герхардом Генценом в 1933 году в диссертации, представленной на факультете математических наук Геттингенского университета . [3] Термин естественная дедукция (или, скорее, его немецкий эквивалент natürliches Schließen ) был введен в употребление в этой статье:
Генцен был мотивирован желанием установить непротиворечивость теории чисел . Он не смог доказать основной результат, требуемый для результата непротиворечивости, теорему об устранении разрезов — Hauptsatz — непосредственно для естественной дедукции. По этой причине он представил свою альтернативную систему, секвенциальное исчисление , для которого он доказал Hauptsatz как для классической , так и для интуиционистской логики . На серии семинаров в 1961 и 1962 годах Правитц дал всеобъемлющее резюме исчислений естественной дедукции и перенес большую часть работы Генцена с секвенциальными исчислениями в рамки естественной дедукции. Его монография 1965 года Natural deduction: a proof-theoretic study [5] должна была стать справочной работой по естественной дедукции и включала приложения для модальной и второпорядковой логики .
В естественной дедукции предложение выводится из набора предпосылок путем многократного применения правил вывода. Система, представленная в этой статье, представляет собой незначительное изменение формулировки Генцена или Правица, но с более тесным соответствием описанию Мартином-Лёфом логических суждений и связок. [6]
У естественной дедукции было большое разнообразие стилей обозначений, [7] что может затруднить распознавание доказательства, если вы не знакомы с одним из них. Чтобы помочь в этой ситуации, в этой статье есть раздел § Обозначения, объясняющий, как читать все обозначения, которые она фактически будет использовать. В этом разделе просто объясняется историческая эволюция стилей обозначений, большинство из которых не могут быть показаны, поскольку нет иллюстраций, доступных по лицензии открытого авторского права — читателю следует обратиться к SEP и IEP за картинками.
Ниже представлена таблица с наиболее распространенными вариантами записи логических связок .
Генцен , который изобрел естественную дедукцию, имел свой собственный стиль записи аргументов. Это будет проиллюстрировано простым аргументом ниже. Допустим, у нас есть простой пример аргумента в пропозициональной логике , например, «если идет дождь, то облачно; идет дождь; следовательно, облачно». (Это в modus ponens .) Представляя это в виде списка предложений, как это обычно бывает, мы бы имели:
В обозначениях Генцена [7] это можно записать так:
Посылки показаны над линией, называемой линией вывода , [11] [12] разделенной запятой , которая указывает на комбинацию посылок. [13] Заключение написано под линией вывода. [11] Линия вывода представляет собой синтаксическое следствие , [11] иногда называемое дедуктивным следствием , [14] которое также обозначается знаком ⊢. [15] [14] Таким образом, вышесказанное можно также записать в одну строку как . (Турникет, обозначающий синтаксическое следствие, имеет меньший приоритет, чем запятая, обозначающая комбинацию посылок, которая, в свою очередь, имеет меньший приоритет, чем стрелка, используемая для материальной импликации; поэтому для интерпретации этой формулы скобки не нужны.) [13]
Синтаксическое следствие противопоставляется семантическому следствию , [16] которое обозначается знаком ⊧. [15] [14] В этом случае вывод следует синтаксически, поскольку естественная дедукция является системой синтаксического доказательства , которая предполагает правила вывода как примитивы .
Стиль Генцена будет использоваться в большей части этой статьи. Разряжающих аннотаций Генцена, используемых для интернализации гипотетических суждений, можно избежать, представляя доказательства в виде дерева последовательностей Γ ⊢A вместо дерева суждений о том, что A (истинно).
Во многих учебниках используется нотация Суппса–Леммона [7] , поэтому в этой статье она также будет приведена — хотя на данный момент она включена только для пропозициональной логики , а остальная часть охвата дается только в стиле Генцена. Доказательство , изложенное в соответствии со стилем нотации Суппса–Леммона , представляет собой последовательность строк, содержащих предложения [17] , где каждое предложение является либо предположением, либо результатом применения правила доказательства к более ранним предложениям в последовательности. [17] Каждая строка доказательства состоит из предложения доказательства вместе с его аннотацией , его набором предположений и текущим номером строки . [17] Набор предположений перечисляет предположения, от которых зависит данное предложение доказательства, на которые ссылаются номера строк. [17] Аннотация указывает, какое правило доказательства было применено и к каким более ранним строкам, чтобы получить текущее предложение. [17] Вот пример доказательства:
Это доказательство станет более понятным, когда будут указаны правила вывода и соответствующие им аннотации – см. § Правила пропозиционального вывода (стиль Суппеса–Леммона).
В этом разделе определяется формальный синтаксис языка пропозициональной логики , в котором обычные способы его реализации противопоставляются способу, разработанному в стиле Генцена.
Формальный язык исчисления высказываний обычно определяется рекурсивным определением , например, таким, как это, из Бостока : [18]
Существуют и другие способы сделать это, например, грамматика BNF . [19] [20]
Определение синтаксиса также может быть дано с использованием древовидной нотации Генцена, путем записи правильно сформированных формул под линией вывода и любых схематических переменных, используемых этими формулами, над ней. [20] Например, эквивалент правил 3 и 4 из определения Бостока выше записывается следующим образом:
Другая нотационная конвенция рассматривает синтаксис языка как категориальную грамматику с единственной категорией «формула», обозначенной символом . Таким образом, любые элементы синтаксиса вводятся категоризациями, для которых нотация есть , что означает « является выражением для объекта в категории ». [21] Буквы предложения, затем, вводятся категоризациями, такими как , , , и так далее; [21] связки, в свою очередь, определяются утверждениями, аналогичными приведенным выше, но с использованием нотации категоризации, как показано ниже:
В оставшейся части статьи нотация категоризации будет использоваться для любых утверждений нотации Генцена, определяющих грамматику языка; любые другие утверждения в нотации Генцена будут выводами, утверждающими, что следует секвенция, а не то, что выражение является правильно сформированной формулой.
Ниже приведен полный список примитивных правил вывода для естественной дедукции в классической пропозициональной логике: [20]
Эта таблица следует традиции использования греческих букв в качестве схем , которые могут охватывать любые формулы, а не только атомарные предложения. Имя правила дается справа от его дерева формул. Например, первое правило введения называется , что является сокращением от "conjunction introduction".
В качестве примера использования правил вывода рассмотрим коммутативность конъюнкции. Если A ∧ B , то B ∧ A ; этот вывод можно сделать, составив правила вывода таким образом, чтобы предпосылки более низкого вывода соответствовали заключению следующего более высокого вывода.
В качестве второго примера рассмотрим вывод формулы « A ⊃ (B ⊃ (A ∧ B)) »:
Этот полный вывод не имеет неудовлетворенных посылок; однако, подвыводы являются гипотетическими. Например, вывод " B ⊃ (A ∧ B) " является гипотетическим с антецедентом " A " (названным u ).
Правила вывода естественной дедукции, в конечном счете, принадлежащие Генцену , приведены ниже. [22] Существует десять примитивных правил доказательства, которые представляют собой правило предположения , плюс четыре пары правил введения и исключения для бинарных связок, а также правило reductio ad adbsurdum . [17] Дизъюнктивный силлогизм может использоваться как более простая альтернатива правильному ∨-исключению, [17] а MTT и DN являются обычно заданными правилами, [22] хотя они не являются примитивными. [17]
Напомним, что пример доказательства уже был приведен при введении нотации § Суппеса–Леммона. Это второй пример.
Теория считается последовательной, если ложность недоказуема (без предположений) и полной, если каждая теорема или ее отрицание доказуемы с использованием правил вывода логики. Это утверждения о всей логике, и обычно они привязаны к некоторому понятию модели . Однако существуют локальные понятия последовательности и полноты, которые являются чисто синтаксическими проверками правил вывода и не требуют обращения к моделям. Первое из них — локальная последовательность, также известная как локальная сводимость, которая гласит, что любой вывод, содержащий введение связки, за которым немедленно следует ее исключение, может быть превращен в эквивалентный вывод без этого обходного пути. Это проверка силы правил исключения: они не должны быть настолько сильными, чтобы включать знания, которые еще не содержатся в их предпосылках. В качестве примера рассмотрим конъюнкции.
Двойственно, локальная полнота говорит, что правила исключения достаточно сильны, чтобы разложить связку на формы, подходящие для ее правила введения. Опять же для союзов:
Эти понятия в точности соответствуют β-редукции (бета-редукции) и η-преобразованию (эта-преобразованию) в лямбда-исчислении , использующем изоморфизм Карри–Ховарда . По локальной полноте мы видим, что каждый вывод может быть преобразован в эквивалентный вывод, где вводится главная связка. Фактически, если весь вывод подчиняется этому порядку исключений, за которыми следуют введения, то он называется нормальным . В нормальном выводе все исключения происходят выше введений. В большинстве логик каждый вывод имеет эквивалентный нормальный вывод, называемый нормальной формой . Существование нормальных форм, как правило, трудно доказать, используя только естественную дедукцию, хотя такие описания существуют в литературе, в частности, Дагом Правицем в 1961 году. [24] Гораздо проще показать это косвенно с помощью представления секвенциального исчисления без сечений .
Логика предыдущего раздела является примером односортной логики, т. е . логики с одним видом объекта: предложениями. Было предложено много расширений этой простой структуры; в этом разделе мы расширим ее вторым видом индивидов или терминов . Точнее, мы добавим новую категорию, «термин», обозначенную . Мы зафиксируем счетный набор переменных , другой счетный набор символов функций и построим термины со следующими правилами формирования:
и
Для предложений мы рассматриваем третье счетное множество P предикатов и определяем атомарные предикаты над терминами с помощью следующего правила формирования:
Первые два правила формирования дают определение термина, которое фактически совпадает с определением в терминологической алгебре и теории моделей , хотя фокус этих областей изучения весьма отличается от естественной дедукции. Третье правило формирования фактически определяет атомарную формулу , как в логике первого порядка , и снова в теории моделей.
К ним добавляется пара правил формирования, определяющих обозначения для квантифицированных предложений; одно для универсальной (∀) и экзистенциальной (∃) квантификации:
Квантификатор всеобщности имеет правила введения и исключения:
Квантор существования имеет правила введения и исключения:
В этих правилах обозначение [ t / x ] A обозначает замену t для каждого (видимого) экземпляра x в A , избегая захвата. [c] Как и прежде, верхние индексы в имени обозначают компоненты, которые выгружаются: термин a не может встречаться в заключении ∀I (такие термины известны как собственные переменные или параметры ), а гипотезы, названные u и v в ∃E, локализуются во второй посылке в гипотетическом выводе. Хотя пропозициональная логика предыдущих разделов была разрешимой , добавление квантификаторов делает логику неразрешимой.
До сих пор квантифицированные расширения являются первопорядковыми : они отличают предложения от видов объектов, над которыми квантифицированы. Логика более высокого порядка использует другой подход и имеет только один вид предложений. Квантификаторы имеют в качестве области квантификации тот же самый вид предложений, что отражено в правилах формирования:
Обсуждение форм введения и исключения для логики высшего порядка выходит за рамки этой статьи. Можно находиться между логикой первого порядка и логикой высшего порядка. Например, логика второго порядка имеет два вида предложений, один вид квантифицирует по терминам, а второй вид квантифицирует по предложениям первого вида.
Представление естественной дедукции до сих пор было сосредоточено на природе предложений без предоставления формального определения доказательства . Чтобы формализовать понятие доказательства, мы немного изменяем представление гипотетических выводов. Мы помечаем антецеденты переменными доказательства (из некоторого счетного множества V переменных) и украшаем сукцедент фактическим доказательством. Антецеденты или гипотезы отделяются от сукцедента с помощью турникета (⊢). Эта модификация иногда проходит под названием локализованных гипотез . Следующая диаграмма суммирует изменение.
Совокупность гипотез будет записана как Γ, когда их точный состав не имеет значения. Чтобы сделать доказательства явными, мы переходим от суждения без доказательств " A " к суждению: "π является доказательством (A) ", которое символически записывается как "π : A ". Следуя стандартному подходу, доказательства указываются с их собственными правилами формирования для суждения "π proof ". Простейшим возможным доказательством является использование маркированной гипотезы; в этом случае доказательством является сама метка.
Давайте перепроверим некоторые из конъюнктов с явными доказательствами. Для конъюнкции мы смотрим на правило введения ∧I, чтобы обнаружить форму доказательств конъюнкции: они должны быть парой доказательств двух конъюнктов. Таким образом:
Правила исключения ∧E 1 и ∧E 2 выбирают либо левый, либо правый конъюнкт; таким образом, доказательства представляют собой пару проекций — первую ( fst ) и вторую ( snd ).
Для импликации форма введения локализует или связывает гипотезу, записанную с использованием λ; это соответствует разряженной метке. В правиле "Γ, u : A " обозначает совокупность гипотез Γ вместе с дополнительной гипотезой u .
Имея доказательства, доступные явно, можно манипулировать доказательствами и рассуждать о них. Ключевая операция с доказательствами — это замена одного доказательства на предположение, используемое в другом доказательстве. Это обычно известно как теорема о замене и может быть доказано индукцией по глубине (или структуре) второго суждения.
До сих пор суждение "Γ ⊢ π : A " имело чисто логическую интерпретацию. В теории типов логическое представление заменяется на более вычислительное представление объектов. Предложения в логической интерпретации теперь рассматриваются как типы , а доказательства как программы в лямбда-исчислении . Таким образом, интерпретация "π : A " - " программа π имеет тип A ". Логическим связкам также дается разное прочтение: конъюнкция рассматривается как произведение (×), импликация как функциональная стрелка (→) и т. д. Однако различия носят лишь косметический характер. Теория типов имеет естественное представление вывода в терминах правил формирования, введения и исключения; на самом деле, читатель может легко восстановить то, что известно как простая теория типов из предыдущих разделов.
Разница между логикой и теорией типов заключается в первую очередь в смещении фокуса с типов (предложений) на программы (доказательства). Теория типов в основном интересуется преобразуемостью или сводимостью программ. Для каждого типа существуют канонические программы этого типа, которые неприводимы; они известны как канонические формы или значения . Если каждая программа может быть приведена к канонической форме, то говорят, что теория типов является нормализующей (или слабо нормализующей ). Если каноническая форма уникальна, то говорят, что теория является сильно нормализующей . Нормализуемость является редкой чертой большинства нетривиальных теорий типов, что является большим отходом от логического мира. (Напомним, что почти каждый логический вывод имеет эквивалентный нормальный вывод.) Чтобы обрисовать причину: в теориях типов, которые допускают рекурсивные определения, можно писать программы, которые никогда не сводятся к значению; таким циклическим программам, как правило, можно задать любой тип. В частности, циклическая программа имеет тип ⊥, хотя нет логического доказательства "⊥". По этой причине парадигма предложений как типов; доказательств как программ работает только в одном направлении, если вообще работает: интерпретация теории типов как логики обычно дает противоречивую логику.
Как и логика, теория типов имеет множество расширений и вариантов, включая версии первого и более высокого порядка. Одна ветвь, известная как теория зависимых типов , используется в ряде систем компьютерных доказательств . Теория зависимых типов позволяет квантификаторам ранжироваться по самим программам. Эти квантифицированные типы записываются как Π и Σ вместо ∀ и ∃ и имеют следующие правила формирования:
Эти типы являются обобщениями типов стрелок и продуктов соответственно, о чем свидетельствуют их правила введения и исключения.
Теория зависимых типов в полной общности очень мощна: она способна выразить почти любое мыслимое свойство программ непосредственно в типах программы. Эта общность имеет высокую цену — либо проверка типов неразрешима ( теория экстенсиональных типов ), либо экстенсиональные рассуждения более сложны ( теория интенсиональных типов ). По этой причине некоторые теории зависимых типов не допускают квантификации произвольных программ, а ограничиваются программами заданной разрешимой индексной области , например, целыми числами, строками или линейными программами.
Поскольку зависимые теории типов позволяют типам зависеть от программ, возникает естественный вопрос: возможно ли, чтобы программы зависели от типов или любой другой комбинации? На такие вопросы существует множество ответов. Популярный подход в теории типов заключается в том, чтобы разрешить программам квантифицироваться по типам, что также известно как параметрический полиморфизм ; существует два основных вида этого подхода: если типы и программы сохраняются отдельно, то получается несколько более хорошо себя ведущая система, называемая предикативным полиморфизмом ; если различие между программой и типом размыто, то получается теоретико-типовой аналог логики высшего порядка, также известный как непредикативный полиморфизм . В литературе рассматривались различные комбинации зависимости и полиморфизма, наиболее известной из которых является лямбда-куб Хенка Барендрегта .
Пересечение логики и теории типов является обширной и активной областью исследований. Новые логики обычно формализуются в общей теоретической установке типов, известной как логический каркас . Популярные современные логические каркасы, такие как исчисление конструкций и LF, основаны на теории зависимых типов более высокого порядка с различными компромиссами в терминах разрешимости и выразительной силы. Эти логические каркасы сами по себе всегда определяются как системы естественной дедукции, что является свидетельством универсальности подхода естественной дедукции.
Для простоты, логика, представленная до сих пор, была интуиционистской . Классическая логика расширяет интуиционистскую логику дополнительной аксиомой или принципом исключенного третьего :
Это утверждение не является, очевидно, ни введением, ни исключением; на самом деле, оно включает в себя два различных коннектора. Первоначальная трактовка Генценом исключенного третьего предписывала одну из следующих трех (эквивалентных) формулировок, которые уже присутствовали в аналогичных формах в системах Гильберта и Гейтинга :
(XM 3 — это просто XM 2 , выраженный в терминах E.) Такая трактовка исключенного третьего, помимо того, что она неприемлема с точки зрения пуриста, вносит дополнительные сложности в определение нормальных форм.
Сравнительно более удовлетворительная трактовка классической естественной дедукции в терминах только правил введения и исключения была впервые предложена Париго в 1992 году в форме классического лямбда-исчисления под названием λμ . Ключевым моментом его подхода была замена истинностно-центрического суждения A более классическим понятием, напоминающим секвенциальное исчисление : в локализованной форме вместо Γ ⊢ A он использовал Γ ⊢ Δ, где Δ — набор предложений, аналогичных Γ. Γ трактовалась как конъюнкция, а Δ — как дизъюнкция. Эта структура по сути взята непосредственно из классических секвенциальных исчислений , но нововведение в λμ заключалось в том, чтобы придать вычислительный смысл классическим доказательствам естественной дедукции в терминах callcc или механизма throw/catch, наблюдаемого в LISP и его потомках. (См. также: first class control .)
Другое важное расширение было сделано для модальных и других логик, которым нужно больше, чем просто базовое суждение об истине. Они были впервые описаны для алетических модальных логик S4 и S5 в стиле естественной дедукции Правитцем в 1965 году [5] и с тех пор накопили большой объем связанной работы. Чтобы привести простой пример, модальная логика S4 требует одного нового суждения, « A valid », которое является категоричным по отношению к истине:
Это категорическое суждение интернализуется как одноместная связка ◻ A (читается как « обязательно A ») со следующими правилами введения и исключения:
Обратите внимание, что посылка « A valid » не имеет определяющих правил; вместо этого вместо нее используется категориальное определение валидности. Этот режим становится более понятным в локализованной форме, когда гипотезы явные. Мы пишем «Ω;Γ ⊢ A », где Γ содержит истинные гипотезы, как и прежде, а Ω содержит валидные гипотезы. Справа есть только одно суждение « A »; валидность здесь не нужна, поскольку «Ω ⊢ A valid » по определению то же самое, что и «Ω;⋅ ⊢ A ». Формы введения и исключения тогда следующие:
Модальные гипотезы имеют свою собственную версию правила гипотезы и теоремы о подстановке.
Эта структура разделения суждений на отдельные наборы гипотез, также известная как многозонные или полиадические контексты, является очень мощной и расширяемой; она применялась для многих различных модальных логик, а также для линейных и других субструктурных логик , чтобы дать несколько примеров. Однако относительно немногие системы модальной логики могут быть формализованы непосредственно в естественной дедукции. Чтобы дать доказательно-теоретические характеристики этих систем, расширения, такие как маркировка или системы глубокого вывода.
Добавление меток к формулам позволяет гораздо более тонко контролировать условия, при которых применяются правила, позволяя применять более гибкие методы аналитических таблиц , как это было сделано в случае маркированной дедукции. Метки также позволяют именовать миры в семантике Крипке; Симпсон (1993) представляет влиятельную технику для преобразования условий фрейма модальной логики в семантике Крипке в правила вывода в естественной дедуктивной формализации гибридной логики . Стоуппа (2004) рассматривает применение многих теорий доказательств, таких как гиперсеквенции Аврона и Поттингера и логика отображения Белнапа, к таким модальным логикам, как S5 и B.
Последовательное исчисление является главной альтернативой естественной дедукции как основе математической логики . В естественной дедукции поток информации является двунаправленным: правила исключения переносят информацию вниз путем деконструкции, а правила введения переносят информацию вверх путем сборки. Таким образом, доказательство естественной дедукции не имеет чистого чтения снизу вверх или сверху вниз, что делает его непригодным для автоматизации поиска доказательств. Чтобы решить эту проблему, Генцен в 1935 году предложил свое последовательное исчисление , хотя изначально он намеревался использовать его как техническое устройство для прояснения согласованности логики предикатов . Клини в своей основополагающей книге 1952 года «Введение в метаматематику» дал первую формулировку последовательного исчисления в современном стиле. [25]
В исчислении последовательностей все правила вывода имеют чистое чтение снизу вверх. Правила вывода могут применяться к элементам по обе стороны турникета . (Чтобы отличить от естественной дедукции, в этой статье используется двойная стрелка ⇒ вместо правой кнопки ⊢ для секвенций.) Правила введения естественной дедукции рассматриваются как правые правила в исчислении последовательностей и структурно очень похожи. С другой стороны, правила исключения превращаются в левые правила в исчислении последовательностей. Чтобы привести пример, рассмотрим дизъюнкцию; правые правила знакомы:
Слева:
Вспомним правило ∨E естественного вывода в локализованной форме:
Предложение A ∨ B , которое является преемником посылки в ∨E, превращается в гипотезу заключения в левом правиле ∨L. Таким образом, левые правила можно рассматривать как своего рода инвертированное правило исключения. Это наблюдение можно проиллюстрировать следующим образом:
В исчислении последовательностей левые и правые правила выполняются в синхронном порядке до тех пор, пока не будет достигнута начальная секвенция , которая соответствует точке встречи правил исключения и введения в естественной дедукции. Эти начальные правила внешне похожи на правило гипотезы естественной дедукции, но в исчислении последовательностей они описывают транспозицию или рукопожатие левого и правого предложений:
Соответствие между секвенциальным исчислением и естественной дедукцией представляет собой пару теорем о корректности и полноте, обе из которых доказуемы с помощью индуктивного аргумента.
Из этих теорем ясно, что секвенциальное исчисление не изменяет понятия истины, поскольку тот же набор предложений остается истинным. Таким образом, можно использовать те же объекты доказательства, что и раньше в выводах секвенциального исчисления. В качестве примера рассмотрим конъюнкции. Правильное правило практически идентично правилу введения
Однако левое правило выполняет некоторые дополнительные замены, которые не выполняются в соответствующих правилах исключения.
Виды доказательств, генерируемых в секвенциальном исчислении, поэтому довольно сильно отличаются от доказательств естественной дедукции. Секвенциальное исчисление производит доказательства в так называемой β-нормальной η-длинной форме, которая соответствует каноническому представлению нормальной формы доказательства естественной дедукции. Если попытаться описать эти доказательства, используя саму естественную дедукцию, то получится то, что называется интеркаляционным исчислением (впервые описанным Джоном Бирнсом), которое можно использовать для формального определения понятия нормальной формы для естественной дедукции.
Теорема подстановки естественного вывода принимает форму структурного правила или структурной теоремы, известной как разрез в секвенциальном исчислении.
В большинстве хорошо себя ведущих логик разрезание не является необходимым как правило вывода, хотя оно остается доказуемым как метатеорема ; избыточность правила разрезания обычно представляется как вычислительный процесс, известный как устранение разрезания . Это имеет интересное применение для естественной дедукции; обычно чрезвычайно утомительно доказывать определенные свойства непосредственно в естественной дедукции из-за неограниченного числа случаев. Например, рассмотрим показ того, что данное предложение не доказуемо в естественной дедукции. Простой индуктивный аргумент терпит неудачу из-за правил вроде ∨E или E, которые могут вводить произвольные предложения. Однако мы знаем, что исчисление последовательностей является полным относительно естественной дедукции, поэтому достаточно показать эту недоказуемость в исчислении последовательностей. Теперь, если разрезание недоступно как правило вывода, то все правила последовательностей либо вводят связку справа, либо слева, поэтому глубина вывода последовательностей полностью ограничена связками в окончательном заключении. Таким образом, показать недоказуемость гораздо проще, потому что есть только конечное число случаев для рассмотрения, и каждый случай полностью состоит из подпредложений заключения. Простым примером этого является теорема о глобальной согласованности : "⋅ ⊢ ⊥" недоказуемо. В версии секвенциального исчисления это явно верно, потому что нет правила, которое может иметь "⋅ ⇒ ⊥" в качестве заключения! Теоретики доказательств часто предпочитают работать над формулировками секвенциального исчисления без сечений из-за таких свойств.
Натуральная дедукция, визуализированная как игра в домино