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

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

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

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

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

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

Обзор

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

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

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

${\ displaystyle B}$

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

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

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

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

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

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

Стандартная семантика суждения при естественной дедукции состоит в том, что оно утверждает, что всякий раз , когда все и т. Д. Верны, также будет истинным. Суждения ${\ displaystyle A_ {1}}$${\ displaystyle A_ {2}}$${\ displaystyle B}$

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

а также

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

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

Системы последовательного исчисления

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

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

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

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

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

а также

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

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

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

${\ Displaystyle \ 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 верно)

или как

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

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

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

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

Редукционные деревья

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

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

${\ displaystyle ((п \ rightarrow r) \ lor (q \ rightarrow r)) \ rightarrow ((p \ land q) \ rightarrow r)}$

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

${\ displaystyle \ vdash ((p \ rightarrow r) \ lor (q \ rightarrow r)) \ rightarrow ((p \ land q) \ rightarrow r)}$

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

${\ displaystyle (п \ rightarrow r) \ lor (q \ rightarrow r) \ vdash (p \ land q) \ rightarrow r}$

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

${\ Displaystyle (п \ rightarrow г) \ лор (д \ rightarrow г), (р \ земля д) \ vdash г}$

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

${\ Displaystyle (п \ rightarrow г) \ лор (д \ rightarrow г), р, д \ vdash г}$

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

${\ displaystyle p \ rightarrow r, p, q \ vdash r}$

${\ displaystyle q \ rightarrow r, p, q \ vdash r}$

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

${\ displaystyle \ lnot p, p, q \ vdash r}$

${\ displaystyle r, p, q \ vdash r}$

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

${\ displaystyle p, q \ vdash p, r}$

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

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

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

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

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

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

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

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

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

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

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

Система LK

В этом разделе вводятся правила исчисления секвенций LK, введенные Гентценом в 1934 году. (LK, неинтуитивно, означает « k lassische Prädikaten l ogik».) (Формальное) доказательство в этом исчислении представляет собой последовательность секвенций, где каждая из секвенции получаются из секвенций, появляющихся раньше в последовательности, с использованием одного из правил, приведенных ниже.

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

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

• ${\ displaystyle \ vdash}$известный как турникет , отделяет предположения слева от предложений справа
• ${\ displaystyle A}$и обозначают формулы логики предикатов первого порядка (можно также ограничить это логикой высказываний),${\ displaystyle B}$
• ${\ Displaystyle \ Gamma, \ Delta, \ Sigma}$, и являются конечными (возможно, пустыми) последовательностями формул (на самом деле порядок формул не имеет значения; см. подраздел Структурные правила ), называемые контекстами, ${\ displaystyle \ Pi}$
  • когда слева от , последовательность формул рассматривается
  совместно (предполагается, что все они выполняются одновременно),${\ displaystyle \ vdash}$
• в то время как справа от , последовательность формул считается дизъюнктивно (по крайней мере, одна из формул должна выполняться для любого присвоения переменных),${\ displaystyle \ vdash}$

${\ displaystyle t}$ обозначает произвольный термин,

${\ displaystyle x}$и обозначают переменные.${\ displaystyle y}$

переменная считается свободной в формуле, если она встречается за пределами квантификаторов или .${\ displaystyle \ forall}$${\ Displaystyle \ существует}$

${\ Displaystyle А [т / х]}$обозначает формулу, которая получается заменой члена для каждого свободного вхождения переменной в формуле с ограничением, что термин должен быть свободным для переменной в (т. е. никакое вхождение какой-либо переменной в не становится связанным ).${\ displaystyle t}$${\ displaystyle x}$${\ displaystyle A}$${\ displaystyle t}$${\ displaystyle x}$${\ displaystyle A}$${\ displaystyle t}$${\ Displaystyle А [т / х]}$

${\ displaystyle WL}$, , , , , : Эти шесть стенда для двух версий каждого из трех структурных правил; один для использования слева ('L') от a , а другой справа ('R'). Правила обозначаются сокращенно «W» для ослабления (влево / вправо) , «C» для сокращения и «P» для перестановки .${\ displaystyle WR}$${\ displaystyle CL}$${\ displaystyle CR}$${\ displaystyle PL}$${\ displaystyle PR}$${\ displaystyle \ vdash}$

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

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

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

Интуитивное объяснение

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

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

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

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

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

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

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

Примеры выводов

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

		${\ displaystyle (I)}$
${\ Displaystyle A \ vdash A}$
		${\ Displaystyle (\ lnot R)}$
${\ Displaystyle \ vdash \ lnot А, А}$
		${\ Displaystyle (\ лор R_ {2})}$
${\ displaystyle \ vdash A \ lor \ lnot A, A}$
		${\ displaystyle (PR)}$
${\ displaystyle \ vdash A, A \ lor \ lnot A}$
		${\ Displaystyle (\ лор R_ {1})}$
${\ Displaystyle \ vdash А \ лор \ lnot А, А \ лор \ lnot А}$
		${\ displaystyle (CR)}$
${\ displaystyle \ vdash A \ lor \ lnot A}$

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

		${\ displaystyle (I)}$
${\ Displaystyle р (х, у) \ vdash р (х, у)}$
		${\ Displaystyle (\ forall L)}$
${\ displaystyle \ forall x \ left (p (x, y) \ right) \ vdash p (x, y)}$
		${\ Displaystyle (\ существует R)}$
${\ displaystyle \ forall x \ left (p (x, y) \ right) \ vdash \ существует y \ left (p (x, y) \ right)}$
		${\ Displaystyle (\ существует L)}$
${\ Displaystyle \ существует у \ влево (\ forall х \ влево (р (х, у) \ вправо) \ вправо) \ vdash \ существует у \ влево (р (х, у) \ вправо)}$
		${\ Displaystyle (\ forall R)}$
${\ Displaystyle \ существует y \ влево (\ forall x \ left (p (x, y) \ right) \ right) \ vdash \ forall x \ left (\ существует y \ left (p (x, y) \ right) \Правильно)}$

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

${\ displaystyle (I)}$ ${\ Displaystyle A \ vdash A}$     ${\ Displaystyle (\ lnot R)}$ ${\ Displaystyle \ vdash \ lnot А, А}$     ${\ displaystyle (PR)}$ ${\ displaystyle \ vdash A, \ lnot A}$              ${\ displaystyle (I)}$ ${\ displaystyle B \ vdash B}$              ${\ displaystyle (I)}$ ${\ Displaystyle C \ vdash C}$         ${\ Displaystyle (\ лор L)}$ ${\ Displaystyle B \ lor C \ vdash B, C}$     ${\ displaystyle (PR)}$ ${\ Displaystyle B \ lor C \ vdash C, B}$     ${\ Displaystyle (\ lnot L)}$ ${\ Displaystyle B \ lor C, \ lnot C \ vdash B}$              ${\ displaystyle (I)}$ ${\ Displaystyle \ lnot A \ vdash \ lnot A}$         ${\ Displaystyle (\ rightarrow L)}$ ${\ Displaystyle \ влево (В \ лор С \ вправо), \ лнот С, \ влево (В \ вправо \ лнот А \ вправо) \ вдаш \ лнот А}$     ${\ Displaystyle (\ земля L_ {1})}$ ${\ displaystyle \ left (B \ lor C \ right), \ lnot C, \ left (\ left (B \ rightarrow \ lnot A \ right) \ land \ lnot C \ right) \ vdash \ lnot A}$     ${\ displaystyle (PL)}$ ${\ displaystyle \ left (B \ lor C \ right), \ left (\ left (B \ rightarrow \ lnot A \ right) \ land \ lnot C \ right), \ lnot C \ vdash \ lnot A}$     ${\ Displaystyle (\ земля L_ {2})}$ ${\ displaystyle \ 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}$     ${\ displaystyle (CL)}$ ${\ displaystyle \ left (B \ lor C \ right), \ left (\ left (B \ rightarrow \ lnot A \ right) \ land \ lnot C \ right) \ vdash \ lnot A}$     ${\ displaystyle (PL)}$ ${\ Displaystyle \ left (\ left (B \ rightarrow \ lnot A \ right) \ land \ lnot C \ right), \ left (B \ lor C \ right) \ vdash \ lnot A}$		${\ Displaystyle (\ rightarrow L)}$
${\ displaystyle \ 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}$
		${\ displaystyle (CR)}$
${\ displaystyle \ left (\ left (B \ rightarrow \ lnot A \ right) \ land \ lnot C \ right), \ left (A \ rightarrow \ left (B \ lor C \ right) \ right) \ vdash \ lnot A}$
		${\ displaystyle (PL)}$
${\ displaystyle \ left (A \ rightarrow \ left (B \ lor C \ right) \ right), \ left (\ left (B \ rightarrow \ lnot A \ right) \ land \ lnot C \ right) \ vdash \ lnot A}$
		${\ Displaystyle (\ rightarrow R)}$
${\ displaystyle \ 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)}$
		${\ Displaystyle (\ rightarrow R)}$
${\ Displaystyle \ 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 встраивает его в саму систему.

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

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

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

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

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

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

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

Свойства системы LK

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

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

Варианты

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

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

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

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

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

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

Абсурд

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

${\ displaystyle {\ cfrac {} {\ bot \ vdash \ quad}}}$

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

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

С отрицание может быть отнесено к частному случаю импликации через определение . ${\ displaystyle \ bot}$${\ displaystyle \ neg A \ iff A \ to \ bot}$

Субструктурная логика

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

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

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

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

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

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

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

Это составляет пропозициональную формулу , классическую тавтологию, которая не имеет конструктивного значения. ${\ Displaystyle (А \ к (В \ лор С)) \ к ((А \ к В) \ лор С)}$

Смотрите также

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

Примечания

использованная литература

• Басс, Сэмюэл Р. (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]
• Краткое отступление: последовательное исчисление
• Интерактивное руководство по последовательному исчислению