Последовательное исчисление

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

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

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

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

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

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

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

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

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

{\ displaystyle B}

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

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

Системы естественной дедукции [ править ]

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

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

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

Стандартная семантика суждения в натуральной дедукции является то , что он утверждает , что всякий раз , когда ^[11] , и т.д., все это правда, тоже будет правда. Суждения ${\ displaystyle A_ {1}}$ ${\ displaystyle A_ {2}}$ ${\ displaystyle 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$

Стандартная семантика секвенции - это утверждение, что всякий раз , когда каждое истинно, по крайней мере одно также будет истинным. ^[13] Таким образом, пустая секвенция, в которой оба цедента пусты, ложна. ^[14] Один из способов выразить это - запятая слева от турникета должна рассматриваться как «и», а запятая справа от турникета должна рассматриваться как (включительно) «или». Секвенты $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}

(по крайней мере одно из As неверно, или одно из B верно) или как

\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})

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

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

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

Генцен проводил четкое различие между его системами естественного вывода с одним выходом (NK и NJ) и его системами последовательного исчисления с несколькими выходами (LK и LJ). Он писал, что интуиционистская система естественной дедукции NJ несколько уродлива. ^[15] Он сказал, что особая роль исключенного третьего в классической системе естественного вывода NK устранена в классической системе исчисления секвенций LK. ^[16] Он сказал, что исчисление секвенций LJ дает больше симметрии, чем естественный вывод NJ в случае интуиционистской логики, а также в случае классической логики (LK против NK). ^[17]Затем он сказал, что в дополнение к этим причинам, исчисление секвенций с несколькими последовательными формулами предназначено, в частности, для его основной теоремы («Хаупцац»). ^[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$ правило: $\quad {\cfrac {\Gamma ,A\land B\vdash \Delta }{\Gamma ,A,B\vdash \Delta }}$	$R\land$ правило: ${\cfrac {\Gamma \vdash \Delta ,A\land B}{\Gamma \vdash \Delta ,A\qquad \Gamma \vdash \Delta ,B}}$
$L\lor$ правило: ${\cfrac {\Gamma ,A\lor B\vdash \Delta }{\Gamma ,A\vdash \Delta \qquad \Gamma ,B\vdash \Delta }}$	$R\lor$ правило: $\quad {\cfrac {\Gamma \vdash \Delta ,A\lor B}{\Gamma \vdash \Delta ,A,B}}$
$L\rightarrow$ правило: ${\cfrac {\Gamma ,A\rightarrow B\vdash \Delta }{\Gamma \vdash \Delta ,A\qquad \Gamma ,B\vdash \Delta }}$	$R\rightarrow$ правило: $\quad {\cfrac {\Gamma \vdash \Delta ,A\rightarrow B}{\Gamma ,A\vdash \Delta ,B}}$
$L\lnot$ правило: $\quad {\cfrac {\Gamma ,\lnot A\vdash \Delta }{\Gamma \vdash \Delta ,A}}$	$R\lnot$ правило: $\quad {\cfrac {\Gamma \vdash \Delta ,\lnot A}{\Gamma ,A\vdash \Delta }}$
Аксиома:
$p,r\vdash q,r$

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

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

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

Отношение к стандартной аксиоматизации [ править ]

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

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

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

В этом разделе вводятся правила исчисления секвенций LK, введенные Гентценом в 1934 году. (LK, неинтуитивно, означает « k lassische Prädikaten l ogik».) ^[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$ , , , , , : Эти шесть стенда для двух версий каждого из трех структурных правил; один для использования слева ('L') от a , а другой - справа ('R'). Правила обозначаются сокращенно «W» для ослабления (влево / вправо) , «C» для сжатия и «P» для перестановки . $WR$ $CL$ $CR$ $PL$ $PR$ $\vdash$

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

Аксиома:	Резать:
${\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 \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\lor B\vdash \Delta ,\Pi }}\quad ({\lor }L)$	${\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma \vdash B,\Pi }{\Gamma ,\Sigma \vdash A\land B,\Delta ,\Pi }}\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$

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

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

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

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

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

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

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

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

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

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

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

Для чего-нибудь более интересного мы докажем . Легко найти вывод, который демонстрирует полезность LK в автоматическом доказательстве. ${\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)}$

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

			$(I)$
$B\vdash B$			$(I)$
$B\vdash B$

			$(I)$
$C\vdash C$			$(I)$
$C\vdash 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)

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

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

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

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

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

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

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

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

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

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

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

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

Приведенные выше правила можно изменить различными способами:

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

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

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

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

Независимо от этого, можно также изменить способ разделения контекстов внутри правил: в случаях и левый контекст каким-то образом разделяется на и при движении вверх. Поскольку сокращение позволяет дублировать их, можно предположить, что полный контекст используется в обеих ветвях деривации. Тем самым гарантируется, что ни одно важное помещение не потеряно в неправильном филиале. Используя ослабление, нерелевантные части контекста могут быть удалены позже. $({\land }R),({\lor }L)$ $({\rightarrow }L)$ $\Gamma$ $\Sigma$

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

Можно ввести , на константе нелепости , представляющую ЛОЖЬ , с аксиомой: $\bot$

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

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

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

При отрицании можно отнести к частному случаю импликации через определение . $\bot$ $\neg A\iff A\to \bot$

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

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

Интуиционистское секвенциальное исчисление: система LJ [ править ]

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

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

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

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

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

Это составляет пропозициональную формулу , классическую тавтологию, которая не имеет конструктивного значения. $(A\to (B\lor C))\to ((A\to B)\lor C)$

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

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

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

^ a b Gentzen 1934 , Gentzen 1935 .
^ a b Curry 1977 , стр. 208–213, дает 5-страничное доказательство теоремы исключения. См. Также страницы 188, 250.
^ a b Kleene 2009 , стр. 453, дает очень краткое доказательство теоремы об исключении сечения.
^ Curry 1977 , стр. 189–244, называет системы Gentzen LC системами. Карри уделяет больше внимания теории, чем доказательствам практической логики.
^ Клини 2009 , стр. 440-516. Эта книга гораздо больше посвящена теоретическим, метаматематическим последствиям секвенциального исчисления в стиле Генцена, чем приложениям к доказательствам практической логики.
^ Клини 2002 , стр. 283-312, 331-361, определяет систему Генцена и доказывает различные теоремырамках этих систем, включая теорему Гёделяполноте и теорему Генцена.
^ Smullyan 1995 , стр. 101-127, дает краткие теоретические представления систем Генценом. Он использует стиль макета табличного доказательства.
^ Карри 1977 , стр. 184–244, сравнивает системы естественного вывода, обозначенные LA, и системы Генцена, обозначенные LC. Карри делает акцент скорее на теоретическом, чем на практическом.
^ Suppes 1999 , стр. 25–150, представляет собой вводную презентацию практического естественного вывода такого рода. Это стало основой системы L .
^ Lemmon 1965 - это элементарное введение в практическую естественную дедукцию, основанную на удобном сокращенном стиле схемы доказательств Система L на основе Suppes 1999 , стр. 25–150.
^ Здесь «всякий раз» используется как неформальное сокращение «для каждого присвоения значений свободным переменным в решении».
↑ Шанкар, Натараджан ; Оуре, Сэм; Рашби, Джон М .; Стрингер-Калверт, Дэвид WJ (2001-11-01). «Руководство по PVS Prover» (PDF) . Руководство пользователя . SRI International . Проверено 29 мая 2015 .
^ Для объяснения дизъюнктивной семантики для правой части секвенций см. Curry 1977 , стр. 189–190, Kleene 2002 , стр. 290, 297, Kleene 2009 , p. 441, Hilbert & Bernays 1970 , стр. 385, Smullyan 1995 , pp. 104–105 и Gentzen 1934 , p. 180.
Перейти ↑ Buss 1998 , p. 10
^ Генценовского 1934 , стр. 188. "Der Kalkül NJ hat manche formale Unschönheiten".
^ Генценовского 1934 , стр. 191. «В дем klassischen Kalkül NK Нама дер Satz фом ausgeschlossenen Dritten Sonderstellung унтер сделайте ден Schlußweisen Эйн [...] ИНДЕМ эр Сечь дер Einführungs- унд Beseitigungssystematik Nicht einfügte. Bei дем им folgenden anzugebenden logistischen klassichen Kalkül LK вирда Diese Sonderstellung aufgehoben . "
^ Генценовского 1934 , стр. 191. «Die damit erreichte Symmetrie erweist sich als für die klassische Logik angemessener».
^ Генценовского 1934 , стр. 191. «Hiermit haben wir einige Gesichtspunkte zur Begründung der Aufstellung der folgenden Kalküle angegeben. Im wesentlichen ist ihre Form jedoch durch die Rücksicht auf den nachher zu beweisenden 'Hauptsatzülnachher zu beweisenden' Hauptsatzülnachher zu beweisenden 'Hauptsatzülnachherzu beweisenden' Hauptsatzülnahtherden da nbstimmtv».
Перейти ↑ Kleene 2002 , p. 441.
^ a b c Прикладная логика, Univ. Корнелла: Лекция 9 . Последнее обращение: 25.06.2016
^ «Помните,путькоторый вы доказать вывод является предположив гипотезу .» - Филип Вадлер , 2 ноября 2015 г., в своем основном докладе: «Утверждения как типы». Минута 14:36 / 55: 28 видеоклипа Code Mesh
^ Тэт WW (2010). "Оригинальное доказательство непротиворечивости Генцена и теорема Бар" (PDF) . В Kahle R, Rathjen M (ред.). Столетие Генцена: в поисках последовательности . Нью-Йорк: Спрингер. С. 213–228.
^ Ян фон Платон, Элементы логического рассуждения , Cambridge University Press, 2014, стр. 32.
^ Генценовского 1934 , стр. 190-193.
^ Smullyan 1995 , стр. 107
Перейти ↑ Kleene 2002 , p. 336, писал в 1967 году, что «это было главным логическим открытием Гентцена 1934–195: когда есть какое-либо (чисто логическое) доказательство предложения, существует прямое доказательство. Следствия этого открытия лежат в теоретико-логических исследованиях, а не в построении коллекций доказанных формул ».
^ Генценовского 1934 , стр. 194, писал: "Der Unterschied zwischen intuitionistischer und klassischer Logik ist bei den Kalkülen LJ und LK äußerlich ganz anderer Art als bei NJ und NK . Dort bestand er in Weglassung bzw. Hinzunahme des Satzesgedärünschrecht, aussendienschrechtungen, aussenschungen, aussellungen, aussendungen, вирд ". Английский перевод: «Разница между интуиционистской и классической логикой в случае исчислений LJ и LK совершенно иного рода, чем в случае NJ и NK.. В последнем случае оно заключалось в удалении или добавлении, соответственно, исключенного среднего правила, тогда как в первом случае оно выражается в последующих условиях ".
^ Теория структурного доказательства (CUP, 2001), Сара Негри и Ян ван Платон

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

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

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

«Последовательное исчисление» , Энциклопедия математики , EMS Press , 2001 [1994]
Краткое отступление: последовательное исчисление
Интерактивное руководство по последовательному исчислению

[gentzen19341935-1] Gentzen 1934 , Gentzen 1935 .

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

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

[4] Curry 1977 , стр. 189–244, называет системы Gentzen LC системами. Карри уделяет больше внимания теории, чем доказательствам практической логики.

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

[6] Клини 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 - это элементарное введение в практическую естественную дедукцию, основанную на удобном сокращенном стиле схемы доказательств Система L на основе Suppes 1999 , стр. 25–150.

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

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

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

[14] Перейти ↑ Buss 1998 , p. 10

[15] Генценовского 1934 , стр. 188. "Der Kalkül NJ hat manche formale Unschönheiten".

[16] Генценовского 1934 , стр. 191. «В дем klassischen Kalkül NK Нама дер Satz фом ausgeschlossenen Dritten Sonderstellung унтер сделайте ден Schlußweisen Эйн [...] ИНДЕМ эр Сечь дер Einführungs- унд Beseitigungssystematik Nicht einfügte. Bei дем им folgenden anzugebenden logistischen klassichen Kalkül LK вирда Diese Sonderstellung aufgehoben . "

[17] Генценовского 1934 , стр. 191. «Die damit erreichte Symmetrie erweist sich als für die klassische Logik angemessener».

[18] Генценовского 1934 , стр. 191. «Hiermit haben wir einige Gesichtspunkte zur Begründung der Aufstellung der folgenden Kalküle angegeben. Im wesentlichen ist ihre Form jedoch durch die Rücksicht auf den nachher zu beweisenden 'Hauptsatzülnachher zu beweisenden' Hauptsatzülnachher zu beweisenden 'Hauptsatzülnachherzu beweisenden' Hauptsatzülnahtherden da nbstimmtv».

[19] Перейти ↑ Kleene 2002 , p. 441.

[Cornell09-20] Прикладная логика, Univ. Корнелла: Лекция 9 . Последнее обращение: 25.06.2016

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

[Tait-22] Тэт WW (2010). "Оригинальное доказательство непротиворечивости Генцена и теорема Бар" (PDF) . В Kahle R, Rathjen M (ред.). Столетие Генцена: в поисках последовательности . Нью-Йорк: Спрингер. С. 213–228.

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

[FOOTNOTEGentzen1934190–193-24] Генценовского 1934 , стр. 190-193.

[25] Smullyan 1995 , стр. 107

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

[27] Генценовского 1934 , стр. 194, писал: "Der Unterschied zwischen intuitionistischer und klassischer Logik ist bei den Kalkülen LJ und LK äußerlich ganz anderer Art als bei NJ und NK . Dort bestand er in Weglassung bzw. Hinzunahme des Satzesgedärünschrecht, aussendienschrechtungen, aussenschungen, aussellungen, aussendungen, вирд ". Английский перевод: «Разница между интуиционистской и классической логикой в случае исчислений LJ и LK совершенно иного рода, чем в случае NJ и NK.. В последнем случае оно заключалось в удалении или добавлении, соответственно, исключенного среднего правила, тогда как в первом случае оно выражается в последующих условиях ".

[28] Теория структурного доказательства (CUP, 2001), Сара Негри и Ян ван Платон

[1]