Секвенционное исчисление

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

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

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

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

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

Обзор

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

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

Основная статья: система Гильберта

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

$B$

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

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

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

Основная статья: Естественный вычет

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

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

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

Стандартная семантика суждения в естественной дедукции заключается в том, что оно утверждает, что всякий раз, когда $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},$

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

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

$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). Он писал, что интуиционистская система естественной дедукции штата Нью-Джерси несколько уродлива. Он говорил, что особая роль исключенного третьего в классической системе естественного вывода NK снимается в классической системе секвенциального исчисления LK. Он сказал, что секвенциальное исчисление LJ дает больше симметрии, чем естественная дедукция NJ в случае интуиционистской логики, а также в случае классической логики (LK против NK). Затем он сказал, что, помимо этих причин, секвенциальное исчисление с множественными последовательными формулами предназначено именно для его основной теоремы («Hauptsatz»).

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

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

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

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

Деревья сокращения

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

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

$((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)$

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

$(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$

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

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

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

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

Левый:	Верно:
$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 году. (Формальное) доказательство в этом исчислении представляет собой последовательность секвенций, где каждая из секвенций может быть получена из секвенций, появляющихся ранее в последовательности, с использованием одного из приведенных ниже правил .

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

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

• $\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$         $(\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)$

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

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

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

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

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

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

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

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

Свойства системы ЛК

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

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

Варианты

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

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

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

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

Правило ослабления становится допустимым, если аксиому (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

Удивительно, но некоторых небольших изменений в правилах ЛК оказывается достаточно, чтобы превратить ее в систему доказательств для интуиционистской логики . Для этого необходимо ограничиться секвенциями, имеющими не более одной формулы в правой части: и изменить правила, чтобы сохранить этот инвариант. Например, $({\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}}.$

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

См. также

• Цирковое исчисление
• Вложенное секвенционное исчисление
• Разрешение (логика)
• Теория доказательств

Ссылки

• Басс, Сэмюэл Р. (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 .

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

• Теория доказательств (секвенционные исчисления) в Стэнфордской энциклопедии философии
• «Секвенционное исчисление» , Математическая энциклопедия , EMS Press , 2001 [1994]
• Краткое отвлечение: секвентивное исчисление
• Интерактивное руководство по секвенционному исчислению