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

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

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

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

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

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

Обзор [ править ]

В теории доказательств и математической логике секвенциальное исчисление представляет собой семейство формальных систем, разделяющих определенный стиль вывода и определенные формальные свойства. Первые системы секвентивного исчисления, LK и LJ , были введены в 1934/1935 году Герхардом Генценом. ^[1]как инструмент изучения естественной дедукции в логике первого порядка (в классической и интуиционистской версиях соответственно). Так называемая «Основная теорема» Генцена ( Hauptsatz ) о LK и LJ была теоремой об исключении разреза , ^[2]^[3]результат с далеко идущими метатеоретическими последствиями, включая последовательность . Несколько лет спустя Генцен продемонстрировал мощь и гибкость этой техники, применив аргумент исключения разреза, чтобы дать (трансфинитное) доказательство непротиворечивости арифметики Пеано , что стало удивительным ответом на теоремы Гёделя о неполноте . Со времени этой ранней работы секвентивные исчисления, также называемые системами Генцена , ^[4]^[5]^[6]^[7] и общие концепции, связанные с ними, широко применяются в области теории доказательств, математической логики и автоматического вывода .

стиле Гильберта дедукции в Системы

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

B

где $B$ — это любая формула логики первого порядка (или любой другой логики, к которой применяется система вывода, например , исчисление высказываний, логика высшего порядка или модальная логика ). Теоремы — это те формулы, которые появляются как заключительное суждение в действительном доказательстве. Система в стиле Гильберта не требует различия между формулами и суждениями; мы приведем его здесь исключительно для сравнения с последующими случаями.

Цена, заплаченная за простой синтаксис системы в стиле Гильберта, заключается в том, что полные формальные доказательства имеют тенденцию становиться чрезвычайно длинными. Конкретные аргументы по поводу доказательств в такой системе почти всегда апеллируют к теореме о дедукции . Это приводит к идее включения теоремы о дедукции в качестве формального правила в систему, что и происходит при естественной дедукции .

естественного вычета Системы

При естественной дедукции суждения имеют форму

A_{1},A_{2},\ldots ,A_{n}\vdash B

где $A_{i}$ 'песок $B$ снова формулы и $n\geq 0$ . Перестановки $A_{i}$ не имеют значения. Другими словами, решение представляет собой список (возможно, пустой) формул слева от турникета ». символа $\vdash$ ", с одной формулой в правой части. ^[8]^[9]^[10] Теоремы – это формулы $B$ такой, что $\vdash B$ (с пустой левой частью) — это вывод действительного доказательства. (В некоторых представлениях о естественной дедукции $A_{i}$ s и турникет явно не прописаны; вместо этого используется двумерное обозначение, из которого их можно вывести.)

Стандартная семантика суждения в естественной дедукции заключается в том, что оно утверждает, что всякий раз, когда ^[11] $A_{1}$ , $A_{2}$ и т. д., все верно, $B$ тоже будет правдой. Суждения

A_{1},\ldots ,A_{n}\vdash B

и

\vdash (A_{1}\land \cdots \land A_{n})\rightarrow B

эквивалентны в том смысле, что доказательство одного может быть расширено до доказательства другого.

Системы секвенционного исчисления [ править ]

Наконец, секвенциальное исчисление обобщает форму естественного дедуктивного суждения на

A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k},

синтаксический объект, называемый секвенцией. Формулы на левой стороне турникета называются антецедентами , а формулы на правой стороне называются последующими или консеквенциями ; вместе они называются цедентами или секвенциями . ^[12] Снова, $A_{i}$ и $B_{i}$ являются формулами и $n$ и $k$ являются неотрицательными целыми числами, то есть левая или правая часть (или ни одна из них, или обе) могут быть пустыми. Как и в естественной дедукции, теоремы – это те, $B$ где $\vdash B$ является выводом действительного доказательства.

Стандартная семантика секвенции — это утверждение, что всякий раз, когда каждое $A_{i}$ правда, по крайней мере один $B_{i}$ тоже будет правдой. ^[13] Таким образом, пустая секвенция, в которой оба цедента пусты, является ложной. ^[14]Один из способов выразить это состоит в том, что запятую слева от турникета следует рассматривать как «и», а запятую справа от турникета следует рассматривать как (включающее) «или». Секвенции

A_{1},\ldots ,A_{n}\vdash B_{1},\ldots ,B_{k}

и

\vdash (A_{1}\land \cdots \land A_{n})\rightarrow (B_{1}\lor \cdots \lor B_{k})

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

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

\vdash \neg A_{1}\lor \neg A_{2}\lor \cdots \lor \neg A_{n}\lor B_{1}\lor B_{2}\lor \cdots \lor B_{k}

(по крайней мере одно из А ложно, или одно из Б верно)

или как

\vdash \neg (A_{1}\land A_{2}\land \cdots \land A_{n}\land \neg B_{1}\land \neg B_{2}\land \cdots \land \neg B_{k})

(не может быть так, чтобы все А были истинными, а все Б — ложными).

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

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

между естественной дедукцией и исчислением Различие последовательным

Генцен утверждал резкое различие между своими системами естественной дедукции с одним выходом (NK и NJ) и системами секвенциального исчисления с несколькими выходами (LK и LJ). Он писал, что интуиционистская система естественной дедукции штата Нью-Джерси несколько уродлива. ^[15] Он говорил, что особая роль исключенного третьего в классической системе естественного вывода NK снимается в классической системе секвенциального исчисления LK. ^[16] Он сказал, что секвенциальное исчисление LJ дает больше симметрии, чем естественная дедукция NJ в случае интуиционистской логики, а также в случае классической логики (LK против NK). ^[17] Затем он сказал, что, помимо этих причин, секвенциальное исчисление с множественными последовательными формулами предназначено именно для его основной теоремы («Hauptsatz»). ^[18]

Происхождение слова " последовательность "

Слово «секвенция» взято из слова «Sequenz» из статьи Генцена 1934 года. ^[1] Клини делает следующий комментарий по поводу перевода на английский язык: «Гентцен говорит «Sequenz», что мы переводим как «последовательность», потому что мы уже использовали слово «последовательность» для любой последовательности объектов, тогда как по-немецки это «Folge». ^[19]

Доказательство логических формул [ править ]

Деревья редукции [ править ]

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

Рассмотрим следующую формулу:

((p\rightarrow r)\lor (q\rightarrow r))\rightarrow ((p\land q)\rightarrow r)

Это записывается в следующем виде, где утверждение, которое необходимо доказать, находится справа от символа турникета $\vdash$ :

\vdash ((p\rightarrow r)\lor (q\rightarrow r))\rightarrow ((p\land q)\rightarrow r)

Теперь вместо того, чтобы доказывать это из аксиом, достаточно принять посылку импликации и затем попытаться доказать ее заключение. ^[21] Следовательно, мы переходим к следующей секвенции:

(p\rightarrow r)\lor (q\rightarrow r)\vdash (p\land q)\rightarrow r

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

(p\rightarrow r)\lor (q\rightarrow r),(p\land q)\vdash r

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

(p\rightarrow r)\lor (q\rightarrow r),p,q\vdash r

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

p\rightarrow r,p,q\vdash r

q\rightarrow r,p,q\vdash r

В случае первого решения перепишем $p\rightarrow r$ как $\lnot p\lor r$ и снова разделим секвенцию, чтобы получить:

\lnot p,p,q\vdash r

r,p,q\vdash r

Вторая секвенция готова; первую секвенцию можно упростить до:

p,q\vdash p,r

Этот процесс всегда можно продолжать до тех пор, пока в каждой стороне не останутся только атомарные формулы. Графически процесс можно описать графом корневого дерева , как показано справа. Корнем дерева является формула, которую мы хотим доказать; листья состоят только из атомарных формул. Дерево известно как дерево редукции . ^[20]^[22]

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

Ниже приведены правила движения по дереву. Всякий раз, когда одна секвенция разбивается на две, вершина дерева имеет две дочерние вершины, и дерево становится разветвленным. Кроме того, можно свободно менять порядок аргументов каждой стороны; Γ и Δ обозначают возможные дополнительные аргументы. ^[20]

Обычный термин для обозначения горизонтальной линии, используемый в раскладках в стиле Генцена для естественного вывода, — это линия вывода . ^[23]

Левый:	Верно:
$L\land {\text{rule: }}\quad {\cfrac {\Gamma ,A\land B\vdash \Delta }{\Gamma ,A,B\vdash \Delta }}$	$R\land {\text{rule: }}{\cfrac {\Gamma \vdash \Delta ,A\land B}{\Gamma \vdash \Delta ,A\qquad \Gamma \vdash \Delta ,B}}$
$L\lor {\text{rule: }}{\cfrac {\Gamma ,A\lor B\vdash \Delta }{\Gamma ,A\vdash \Delta \qquad \Gamma ,B\vdash \Delta }}$	$R\lor {\text{rule: }}\quad {\cfrac {\Gamma \vdash \Delta ,A\lor B}{\Gamma \vdash \Delta ,A,B}}$
$L\rightarrow {\text{rule: }}{\cfrac {\Gamma ,A\rightarrow B\vdash \Delta }{\Gamma \vdash \Delta ,A\qquad \Gamma ,B\vdash \Delta }}$	$R\rightarrow {\text{rule: }}\quad {\cfrac {\Gamma \vdash \Delta ,A\rightarrow B}{\Gamma ,A\vdash \Delta ,B}}$
$L\lnot {\text{rule: }}\quad {\cfrac {\Gamma ,\lnot A\vdash \Delta }{\Gamma \vdash \Delta ,A}}$	$R\lnot {\text{rule: }}\quad {\cfrac {\Gamma \vdash \Delta ,\lnot A}{\Gamma ,A\vdash \Delta }}$
Аксиома:
$\Gamma ,A\vdash \Delta ,A$

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

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

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

стандартным аксиоматизациям Отношение к

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

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

Система ЛК [ править ]

В этом разделе представлены правила секвенциального исчисления LK (расшифровывается как Logistische Kalkül), введенные Генценом в 1934 году. ^[24] (Формальное) доказательство в этом исчислении представляет собой последовательность секвенций, где каждая из секвенций может быть получена из секвенций, появляющихся ранее в последовательности, с использованием одного из приведенных ниже правил .

Правила вывода [ править ]

Будут использоваться следующие обозначения:

$\vdash$ известный как турникет , отделяет предположения слева от предложений справа.
$A$ и $B$ обозначают формулы логики предикатов первого порядка (можно также ограничить это логикой высказываний),
$\Gamma ,\Delta ,\Sigma$ $\Гамма,\Дельта,\Сигма$ , и $\Pi$ $\Пи$ представляют собой конечные (возможно, пустые) последовательности формул (на самом деле порядок формул не имеет значения; см. § Структурные правила ), называемые контекстами,
- когда слева от $\vdash$ , последовательность формул рассматривается конъюнктивно (предполагается, что все выполняются одновременно),
- находясь справа от $\vdash$ , последовательность формул рассматривается дизъюнктивно (при любом назначении переменных должна выполняться хотя бы одна из формул),
$t$ обозначает произвольный термин,
$x$ и $y$ обозначать переменные.
Говорят, что переменная встречается свободной , если она не связана кванторами. в формуле $\forall$ или $\exists$ .
$A[t/x]$ обозначает формулу, полученную заменой слагаемого $t$ для каждого свободного вхождения переменной $x$ в формуле $A$ с тем ограничением, что термин $t$ должно быть свободно для переменной $x$ в $A$ (т.е. отсутствие появления какой-либо переменной в $t$ становится связанным в $A[t/x]$ ).
$WL$ , $WR$ , $CL$ , $CR$ , $PL$ , $PR$ : Эти шесть означают две версии каждого из трех структурных правил; один для использования слева («L») $\vdash$ , а другой справа («R»). Правила обозначаются сокращенно «W» для ослабления (слева/вправо) , «C» для сокращения и «P» для перестановки .

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

Аксиома:	Резать:
${\cfrac {\qquad }{A\vdash A}}\quad (I)$	${\cfrac {\Gamma \vdash \Delta ,A\qquad A,\Sigma \vdash \Pi }{\Gamma ,\Sigma \vdash \Delta ,\Pi }}\quad ({\mathit {Cut}})$
Левые логические правила:	Правильные логические правила:
${\cfrac {\Gamma ,A\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{1})$	${\cfrac {\Gamma \vdash A,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{1})$
${\cfrac {\Gamma ,B\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{2})$	${\cfrac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{2})$
${\cfrac {\Gamma ,A\vdash \Delta \qquad \Gamma ,B\vdash \Delta }{\Gamma ,A\lor B\vdash \Delta }}\quad ({\lor }L)$	${\cfrac {\Gamma \vdash A,\Delta \qquad \Gamma \vdash B,\Delta }{\Gamma \vdash A\land B,\Delta }}\quad ({\land }R)$
${\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\rightarrow B\vdash \Delta ,\Pi }}\quad ({\rightarrow }L)$	${\cfrac {\Gamma ,A\vdash B,\Delta }{\Gamma \vdash A\rightarrow B,\Delta }}\quad ({\rightarrow }R)$
${\cfrac {\Gamma \vdash A,\Delta }{\Gamma ,\lnot A\vdash \Delta }}\quad ({\lnot }L)$	${\cfrac {\Gamma ,A\vdash \Delta }{\Gamma \vdash \lnot A,\Delta }}\quad ({\lnot }R)$
${\cfrac {\Gamma ,A[t/x]\vdash \Delta }{\Gamma ,\forall xA\vdash \Delta }}\quad ({\forall }L)$	${\cfrac {\Gamma \vdash A[y/x],\Delta }{\Gamma \vdash \forall xA,\Delta }}\quad ({\forall }R)$
${\cfrac {\Gamma ,A[y/x]\vdash \Delta }{\Gamma ,\exists xA\vdash \Delta }}\quad ({\exists }L)$	${\cfrac {\Gamma \vdash A[t/x],\Delta }{\Gamma \vdash \exists xA,\Delta }}\quad ({\exists }R)$
Левые структурные правила:	Правильные структурные правила:
${\cfrac {\Gamma \vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {WL}})$	${\cfrac {\Gamma \vdash \Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {WR}})$
${\cfrac {\Gamma ,A,A\vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {CL}})$	${\cfrac {\Gamma \vdash A,A,\Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {CR}})$
${\cfrac {\Gamma _{1},A,B,\Gamma _{2}\vdash \Delta }{\Gamma _{1},B,A,\Gamma _{2}\vdash \Delta }}\quad ({\mathit {PL}})$	${\cfrac {\Gamma \vdash \Delta _{1},A,B,\Delta _{2}}{\Gamma \vdash \Delta _{1},B,A,\Delta _{2}}}\quad ({\mathit {PR}})$

Ограничения: В правилах $({\forall }R)$ и $({\exists }L)$ , переменная $y$ не должно встречаться свободно где-либо в соответствующих нижних секвенциях.

Интуитивное объяснение [ править ]

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

Несмотря на формальную формулировку, приведенные выше правила допускают очень интуитивное прочтение с точки зрения классической логики. Рассмотрим, например, правило $({\land }L_{1})$ . Там говорится, что всякий раз, когда можно доказать, что $\Delta$ можно сделать вывод из некоторой последовательности формул, содержащих $A$ , то также можно сделать вывод $\Delta$ из (более сильного) предположения, что $A\land B$ держит. Аналогично, правило $({\neg }R)$ утверждает, что если $\Gamma$ и $A$ достаточно, чтобы сделать вывод $\Delta$ , затем из $\Gamma$ в одиночку можно либо еще заключить $\Delta$ или $A$ должно быть ложным, т.е. ${\neg }A$ держит. Все правила можно интерпретировать именно так.

Чтобы получить представление о правилах кванторов, рассмотрим правило $({\forall }R)$ . Конечно, сделав такой вывод $\forall {x}A$ справедливо только потому, что $A[y/x]$ правда, вообще-то это невозможно. Если же переменная у нигде не упоминается (т.е. ее все равно можно выбирать свободно, не влияя на другие формулы), то можно предположить, что $A[y/x]$ выполняется для любого значения y. Остальные правила должны быть довольно простыми.

Вместо того, чтобы рассматривать правила как описания юридических выводов в логике предикатов, их можно также рассматривать как инструкции по построению доказательства для данного утверждения. В этом случае правила можно читать снизу вверх; например, $({\land }R)$ говорит это, чтобы доказать это $A\land B$ следует из предположений $\Gamma$ и $\Sigma$ , достаточно доказать, что $A$ можно сделать вывод из $\Gamma$ и $B$ можно сделать вывод из $\Sigma$ , соответственно. Обратите внимание, что, учитывая некоторую предысторию, неясно, как это разделить на $\Gamma$ и $\Sigma$ . Однако существует лишь конечное число возможностей, подлежащих проверке, поскольку антецедент по предположению конечен. Это также иллюстрирует, как теорию доказательств можно рассматривать как комбинаторную обработку доказательств: при наличии доказательств для обоих $A$ и $B$ , можно построить доказательство $A\land B$ .

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

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

Обратите внимание, что у всех правил есть зеркальные компаньоны, за исключением подразумеваемых. Это отражает тот факт, что обычный язык логики первого порядка не включает связку «не подразумевается». $\not \leftarrow$ это было бы двойственное значение Де Моргана. Добавление такой связки с ее естественными правилами сделало бы исчисление полностью лево-правосимметричным.

Пример вывода [ править ]

Вот вывод " $\vdash A\lor \lnot A$ ", известный как Закон исключенного третьего ( tertium non datur по-латыни).

		$(I)$
$A\vdash A$
		$(\lnot R)$
$\vdash \lnot A,A$
		$(\lor R_{2})$
$\vdash A\lor \lnot A,A$
		$(PR)$
$\vdash A,A\lor \lnot A$
		$(\lor R_{1})$
$\vdash A\lor \lnot A,A\lor \lnot A$
		$(CR)$
$\vdash A\lor \lnot A$

Далее следует доказательство простого факта, касающегося кванторов. Обратите внимание, что обратное неверно, и его ложность можно увидеть при попытке вывести его снизу вверх, поскольку существующую свободную переменную нельзя использовать для замены в правилах. $(\forall R)$ и $(\exists L)$ .

		$(I)$
$p(x,y)\vdash p(x,y)$
		$(\forall L)$
$\forall x\left(p(x,y)\right)\vdash p(x,y)$
		$(\exists R)$
$\forall x\left(p(x,y)\right)\vdash \exists y\left(p(x,y)\right)$
		$(\exists L)$
$\exists y\left(\forall x\left(p(x,y)\right)\right)\vdash \exists y\left(p(x,y)\right)$
		$(\forall R)$
$\exists y\left(\forall x\left(p(x,y)\right)\right)\vdash \forall x\left(\exists y\left(p(x,y)\right)\right)$

Для более интересного докажем ${\left(\left(A\rightarrow \left(B\lor C\right)\right)\rightarrow \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)\right)}$ . Вывод найти несложно, что иллюстрирует полезность LK в автоматизированном доказательстве.

		$(I)$
$A\vdash A$
		$(\lnot R)$
$\vdash \lnot A,A$
		$(PR)$
$\vdash A,\lnot A$

		$(I)$
$B\vdash B$
		$(WR)$
$B\vdash B,C$

		$(I)$
$C\vdash C$
		$(WR)$
$C\vdash B,C$

(\lor L)

B\lor C\vdash B,C

(PR)

B\lor C\vdash C,B

(\lnot L)

B\lor C,\lnot C\vdash B

		$(I)$
$\lnot A\vdash \lnot A$		$(I)$
$\lnot A\vdash \lnot A$

(\rightarrow L)

\left(B\lor C\right),\lnot C,\left(B\rightarrow \lnot A\right)\vdash \lnot A

(\land L_{1})

\left(B\lor C\right),\lnot C,\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A

(PL)

\left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\lnot C\vdash \lnot A

(\land L_{2})

\left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A

(CL)

\left(B\lor C\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A

(PL)

\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(B\lor C\right)\vdash \lnot A

(\rightarrow L)

\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(A\rightarrow \left(B\lor C\right)\right)\vdash \lnot A,\lnot A

(CR)

\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right),\left(A\rightarrow \left(B\lor C\right)\right)\vdash \lnot A

(PL)

\left(A\rightarrow \left(B\lor C\right)\right),\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\vdash \lnot A

(\rightarrow R)

\left(A\rightarrow \left(B\lor C\right)\right)\vdash \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)

(\rightarrow R)

\vdash \left(\left(A\rightarrow \left(B\lor C\right)\right)\rightarrow \left(\left(\left(B\rightarrow \lnot A\right)\land \lnot C\right)\rightarrow \lnot A\right)\right)

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

Связь с аналитическими таблицами [ править ]

Для некоторых формулировок (т.е. вариантов) секвенциального исчисления доказательство в таком исчислении изоморфно перевернутой замкнутой аналитической таблице . ^[25]

Структурные правила [ править ]

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

Ослабление (W) позволяет добавлять в последовательность произвольные элементы. Интуитивно это допускается в антецеденте, поскольку мы всегда можем ограничить объем нашего доказательства (если у всех машин есть колеса, то можно с уверенностью сказать, что у всех черных машин есть колеса); и в последующем, потому что мы всегда можем допустить альтернативные выводы (если у всех машин есть колеса, то можно с уверенностью сказать, что у всех машин есть либо колеса, либо крылья).

Сжатие (C) и перестановка (P) гарантируют, что ни порядок (P), ни кратность вхождений (C) элементов последовательностей не имеют значения. Таким образом, вместо последовательностей можно было бы рассматривать и множества .

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

Свойства системы ЛК [ править ]

Можно показать, что эта система правил одновременно надежна и полна по отношению к логике первого порядка, т. е. к утверждению $A$ следует семантически из набора посылок $\Gamma$ $(\Gamma \vDash A)$ тогда и только тогда, когда последовательность $\Gamma \vdash A$ можно получить по вышеуказанным правилам. ^[26]

В секвенциальном исчислении допустимо правило отсечения . Этот результат также известен как Hauptsatz Генцена («Основная теорема»). ^[2]^[3]

Варианты [ править ]

Вышеупомянутые правила могут быть изменены различными способами:

структурные альтернативы Незначительные

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

Прежде всего, как упоминалось выше, секвенции можно рассматривать как состоящие из множеств или мультимножеств . В этом случае правила перестановки и (при использовании множеств) формул сжатия излишни.

Правило ослабления становится допустимым, если аксиому (I) изменить для вывода любой секвенции вида $\Gamma ,A\vdash A,\Delta$ . Любое ослабление, возникающее при выводе, можно тогда перенести в начало доказательства. Это может быть удобным изменением при построении доказательств снизу вверх.

Можно также изменить, будут ли правила с более чем одной посылкой использовать один и тот же контекст для каждой из этих посылок или разделить свои контексты между ними: например, $({\lor }L)$ вместо этого может быть сформулировано как

{\cfrac {\Gamma ,A\vdash \Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\lor B\vdash \Delta ,\Pi }}.

Сокращение и ослабление делают эту версию правила взаимовыводимой с версией выше, хотя при их отсутствии, как и в линейной логике , эти правила определяют разные связки.

Абсурд [ править ]

Можно представить $\bot$ , константа абсурда, представляющая false , с аксиомой:

{\cfrac {}{\bot \vdash \quad }}

Или если, как описано выше, ослабление должно быть допустимым правилом, то с аксиомой:

{\cfrac {}{\Gamma ,\bot \vdash \Delta }}

С $\bot$ , отрицание можно отнести к частному случаю импликации посредством определения $(\neg A)\iff (A\to \bot )$ .

Субструктурная логика [ править ]

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

: System LJ секвенциальное исчисление Интуиционистское

Удивительно, но некоторых небольших изменений в правилах ЛК оказывается достаточно, чтобы превратить ее в систему доказательств для интуиционистской логики . ^[27] Для этого необходимо ограничиться секвенциями, имеющими не более одной формулы в правой части: ^[28]и изменить правила, чтобы сохранить этот инвариант. Например, $({\lor }L)$ переформулируется следующим образом (где C – произвольная формула):

{\cfrac {\Gamma ,A\vdash C\qquad \Gamma ,B\vdash C}{\Gamma ,A\lor B\vdash C}}\quad ({\lor }L)

Получившаяся система называется LJ. Оно корректно и полно по отношению к интуиционистской логике и допускает аналогичное доказательство исключения разреза. Это можно использовать при доказательстве свойств дизъюнкции и существования .

Фактически, единственные правила в LK, которые необходимо ограничить консеквентами, состоящими из одной формулы, — это $({\to }R)$ , $(\neg R)$ (что можно рассматривать как частный случай ${\to }R$ , как описано выше) и $({\forall }R)$ . Когда многоформульные консеквенции интерпретируются как дизъюнкции, все остальные правила вывода LK выводятся в LJ, а правила $({\to }R)$ и $({\forall }R)$ становиться

{\cfrac {\Gamma ,A\vdash B\lor C}{\Gamma \vdash (A\to B)\lor C}}

и когда $y$ не встречается свободно в нижней секвенции)

{\cfrac {\Gamma \vdash A[y/x]\lor C}{\Gamma \vdash (\forall xA)\lor C}}.

Эти правила не являются интуиционистски обоснованными.

См. также [ править ]

Примечания [ править ]

^ Перейти обратно: ^а ^б Генцен 1934 , Генцен 1935 .
^ Перейти обратно: ^а ^б Curry 1977 , стр. 208–213, дает 5-страничное доказательство теоремы исключения. См. также стр. 188, 250.
^ Перейти обратно: ^а ^б Клини 2009 , стр. 453, дает очень краткое доказательство теоремы об исключении разреза.
^ Карри 1977 , стр. 189–244, называет системы Генцена LC-системами. Акцент Карри делается больше на теории, чем на практических логических доказательствах.
^ Клини 2009 , стр. 440–516. Эта книга гораздо больше посвящена теоретическим, метаматематическим последствиям секвентивного исчисления в стиле Генцена, чем приложениям к практическим логическим доказательствам.
^ Kleene 2002 , стр. 283–312, 331–361, определяет системы Генцена и доказывает различные теоремы в рамках этих систем, включая теорему Гёделя о полноте и теорему Генцена.
^ Smullyan 1995 , стр. 101–127, дает краткое теоретическое представление систем Генцена. Он использует стиль макета табличного доказательства.
^ Карри 1977 , стр. 184–244, сравнивает естественные системы дедукции, обозначенные LA, и системы Генцена, обозначенные LC. Акцент Карри носит скорее теоретический, чем практический характер.
^ Suppes 1999 , стр. 25–150, представляет собой вводное изложение практических естественных выводов такого рода. Это стало основой L. Системы
^ Lemmon 1965 — это элементарное введение в практический естественный вывод, основанное на удобном стиле сокращенного доказательства System L , основанном на Suppes 1999 , стр. 25–150.
^ Здесь «всякий раз» используется как неформальное сокращение «для каждого присвоения значений свободным переменным в решении»
^ Шанкар, Натараджан ; Оуре, Сэм; Рашби, Джон М .; Стрингер-Калверт, Дэвид У.Дж. (1 ноября 2001 г.). «Руководство по проверке PVS» (PDF) . Гид пользователя . НИИ Интернешнл . Проверено 29 мая 2015 г.
^ Объяснения дизъюнктивной семантики правой части секвенций см. в Curry 1977 , стр. 189–190, Kleene 2002 , стр. 290, 297, Kleene 2009 , p. 441, Гильберт и Бернейс 1970 , с. 385, Smullyan 1995 , стр. 104–105 и Genzen 1934 , p. 180.
^ Басс 1998 , стр. 10.
^ Генцен 1934 , с. 188. « Исчисление штата Нью-Джерси имеет некоторые формальные недостатки».
^ Генцен 1934 , с. 191. «В классическом исчислении НК теорема об исключенном третьем лице занимала особое положение среди методов рассуждения [...] тем, что не вписывалась в систему введения и исключения. В логистическом классическом исчислении ЛК к как будет указано ниже , это особое положение упраздняется».
^ Генцен 1934 , с. 191. «Достигаемая таким образом симметрия оказывается более подходящей для классической логики».
^ Генцен 1934 , с. 191. «Настоящим мы дали некоторые аспекты, чтобы оправдать установление следующих вычислений. Однако по существу их форма определяется рассмотрением «основной теоремы», которая будет доказана позже, и поэтому не может быть обоснована более подробно в настоящее время. ."
^ Клини 2002 , с. 441.
^ Перейти обратно: ^а ^б ^с Прикладная логика, унив. Корнелла: Лекция 9 . Последнее получение: 25 июня 2016 г.
^ «Помните, что вы можете доказать импликацию гипотезу , приняв » . - Филип Уодлер , 2 ноября 2015 г., в своем основном докладе: «Предложения как типы». Минута 14:36/55:28 видеоклипа Code Mesh
^ Тейт В.В. (2010). «Оригинальное доказательство непротиворечивости Генцена и теорема Бара» (PDF) . Кале Р., Ратьен М. (ред.). Столетие Генцена: В поисках последовательности . Нью-Йорк: Спрингер. стр. 213–228.
^ Ян фон Платон, Элементы логического рассуждения , Cambridge University Press, 2014, стр. 32.
^ Анджей-Инджейчак, Введение в теорию и приложения пропозициональных секвентивных исчислений (2021, глава «Секвенционное исчисление Генцена LK»). По состоянию на 3 августа 2022 г.
^ Смуллян 1995 , с. 107
^ Клини 2002 , с. 336, писал в 1967 году, что «важным логическим открытием Генцена (1934–1935 гг.) было то, что, когда есть какое-либо (чисто логическое) доказательство предложения, существует и прямое доказательство. Смысл этого открытия лежит в теоретических логических исследованиях, а не создавать коллекции доказанных формул».
^ Генцен 1934 , с. 194, писал: «Различие между интуиционистской и классической логикой имеет внешне совершенно иной характер в расчетах LJ и LK , чем в NJ и NK . Там оно заключалось в опущении или добавлении предложения об исключенном третьем, тогда как здесь оно было выражено условием правопреемства». Английский перевод: «Разница между интуиционистской и классической логикой в случае исчислений LJ и LK совершенно иного рода, чем в случае NJ и NK . В последнем случае она заключалась в удалении или добавлении соответственно правило исключенного среднего, тогда как в первом случае оно выражается через последовательные условия».
^ М. Темкин, "Доказательство недоказуемости", стр.22--26. В материалах третьего ежегодного симпозиума по логике в информатике, 5–8 июля 1988 г. (1988), IEEE. ISBN 0-8186-0853-6.

Ссылки [ править ]

Басс, Сэмюэл Р. (1998). «Введение в теорию доказательств». У Сэмюэля Р. Басса (ред.). Справочник по теории доказательств . Эльзевир. стр. 1–78. ISBN 0-444-89840-9 .
Карри, Хаскелл Брукс (1977) [1963]. Основы математической логики . Dover Publications Inc. Нью-Йорк: ISBN 978-0-486-63462-3 .
Генцен, Герхард Карл Эрих (1934). «Исследования по логическим рассуждениям. I» . Математический журнал . 39 (2): 176–210. дои : 10.1007/BF01201353 . S2CID 121546341 .
Генцен, Герхард Карл Эрих (1935). «Исследования по логическим рассуждениям. II» . Математический журнал . 39 (3): 405–431. дои : 10.1007/bf01201363 . S2CID 186239837 .
Жирар, Жан-Ив ; Пол Тейлор; Ив Лафон (1990) [1989]. Доказательства и типы . Издательство Кембриджского университета (Кембриджские трактаты по теоретической информатике, 7). ISBN 0-521-37181-3 .
Гильберт, Дэвид ; Бернейс, Пол (1970) [1939]. Основы математики II (Второе изд.). Берлин, Нью-Йорк: Springer Verlag. ISBN 978-3-642-86897-9 .
Клини, Стивен Коул (2009) [1952]. Введение в метаматематику . Иши Пресс Интернешнл. ISBN 978-0-923891-57-2 .
Клини, Стивен Коул (2002) [1967]. Математическая логика . Минеола, Нью-Йорк: Dover Publications. ISBN 978-0-486-42533-7 .
Леммон, Эдвард Джон (1965). Начало логики . Томас Нельсон. ISBN 0-17-712040-1 .
Манкосу, Паоло; Гальван, Серджио; Зак, Ричард (2021). Введение в теорию доказательств — нормализация, исключение разрезов и доказательства непротиворечивости . Издательство Оксфордского университета . п. 431. ИСБН 978-0-19-289593-6 .
Смуллян, Раймонд Меррилл (1995) [1968]. Логика первого порядка . Нью-Йорк: Dover Publications. ISBN 978-0-486-68370-6 .
Суппес, Патрик Полковник (1999) [1957]. Введение в логику . Минеола, Нью-Йорк: Dover Publications. ISBN 978-0-486-40687-9 .

Внешние ссылки [ править ]

[gentzen19341935-1] Перейти обратно: ^а ^б Генцен 1934 , Генцен 1935 .

[curry_cut_elimination-2] Перейти обратно: ^а ^б Curry 1977 , стр. 208–213, дает 5-страничное доказательство теоремы исключения. См. также стр. 188, 250.

[kleene_cut_elimination-3] Перейти обратно: ^а ^б Клини 2009 , стр. 453, дает очень краткое доказательство теоремы об исключении разреза.

[4] Карри 1977 , стр. 189–244, называет системы Генцена LC-системами. Акцент Карри делается больше на теории, чем на практических логических доказательствах.

[5] Клини 2009 , стр. 440–516. Эта книга гораздо больше посвящена теоретическим, метаматематическим последствиям секвентивного исчисления в стиле Генцена, чем приложениям к практическим логическим доказательствам.

[6] Kleene 2002 , стр. 283–312, 331–361, определяет системы Генцена и доказывает различные теоремы в рамках этих систем, включая теорему Гёделя о полноте и теорему Генцена.

[7] Smullyan 1995 , стр. 101–127, дает краткое теоретическое представление систем Генцена. Он использует стиль макета табличного доказательства.

[8] Карри 1977 , стр. 184–244, сравнивает естественные системы дедукции, обозначенные LA, и системы Генцена, обозначенные LC. Акцент Карри носит скорее теоретический, чем практический характер.

[9] Suppes 1999 , стр. 25–150, представляет собой вводное изложение практических естественных выводов такого рода. Это стало основой L. Системы

[10] Lemmon 1965 — это элементарное введение в практический естественный вывод, основанное на удобном стиле сокращенного доказательства System L , основанном на Suppes 1999 , стр. 25–150.

[11] Здесь «всякий раз» используется как неформальное сокращение «для каждого присвоения значений свободным переменным в решении»

[pvs-prover-12] Шанкар, Натараджан ; Оуре, Сэм; Рашби, Джон М .; Стрингер-Калверт, Дэвид У.Дж. (1 ноября 2001 г.). «Руководство по проверке PVS» (PDF) . Гид пользователя . НИИ Интернешнл . Проверено 29 мая 2015 г.

[13] Объяснения дизъюнктивной семантики правой части секвенций см. в Curry 1977 , стр. 189–190, Kleene 2002 , стр. 290, 297, Kleene 2009 , p. 441, Гильберт и Бернейс 1970 , с. 385, Smullyan 1995 , стр. 104–105 и Genzen 1934 , p. 180.

[14] Басс 1998 , стр. 10.

[15] Генцен 1934 , с. 188. « Исчисление штата Нью-Джерси имеет некоторые формальные недостатки».

[16] Генцен 1934 , с. 191. «В классическом исчислении НК теорема об исключенном третьем лице занимала особое положение среди методов рассуждения [...] тем, что не вписывалась в систему введения и исключения. В логистическом классическом исчислении ЛК к как будет указано ниже , это особое положение упраздняется».

[17] Генцен 1934 , с. 191. «Достигаемая таким образом симметрия оказывается более подходящей для классической логики».

[18] Генцен 1934 , с. 191. «Настоящим мы дали некоторые аспекты, чтобы оправдать установление следующих вычислений. Однако по существу их форма определяется рассмотрением «основной теоремы», которая будет доказана позже, и поэтому не может быть обоснована более подробно в настоящее время. ."

[19] Клини 2002 , с. 441.

[Cornell09-20] Перейти обратно: ^а ^б ^с Прикладная логика, унив. Корнелла: Лекция 9 . Последнее получение: 25 июня 2016 г.

[Wadler-21] «Помните, что вы можете доказать импликацию гипотезу , приняв » . - Филип Уодлер , 2 ноября 2015 г., в своем основном докладе: «Предложения как типы». Минута 14:36/55:28 видеоклипа Code Mesh

[Tait-22] Тейт В.В. (2010). «Оригинальное доказательство непротиворечивости Генцена и теорема Бара» (PDF) . Кале Р., Ратьен М. (ред.). Столетие Генцена: В поисках последовательности . Нью-Йорк: Спрингер. стр. 213–228.

[23] Ян фон Платон, Элементы логического рассуждения , Cambridge University Press, 2014, стр. 32.

[24] Анджей-Инджейчак, Введение в теорию и приложения пропозициональных секвентивных исчислений (2021, глава «Секвенционное исчисление Генцена LK»). По состоянию на 3 августа 2022 г.

[25] Смуллян 1995 , с. 107

[26] Клини 2002 , с. 336, писал в 1967 году, что «важным логическим открытием Генцена (1934–1935 гг.) было то, что, когда есть какое-либо (чисто логическое) доказательство предложения, существует и прямое доказательство. Смысл этого открытия лежит в теоретических логических исследованиях, а не создавать коллекции доказанных формул».

[27] Генцен 1934 , с. 194, писал: «Различие между интуиционистской и классической логикой имеет внешне совершенно иной характер в расчетах LJ и LK , чем в NJ и NK . Там оно заключалось в опущении или добавлении предложения об исключенном третьем, тогда как здесь оно было выражено условием правопреемства». Английский перевод: «Разница между интуиционистской и классической логикой в случае исчислений LJ и LK совершенно иного рода, чем в случае NJ и NK . В последнем случае она заключалась в удалении или добавлении соответственно правило исключенного среднего, тогда как в первом случае оно выражается через последовательные условия».

[28] М. Темкин, "Доказательство недоказуемости", стр.22--26. В материалах третьего ежегодного симпозиума по логике в информатике, 5–8 июля 1988 г. (1988), IEEE. ISBN 0-8186-0853-6.

[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]

[26]

[27]

[28]