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

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

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

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

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

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

Обзор

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

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

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

${\displaystyle B}$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

${\displaystyle ((p\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)}$

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

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

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

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

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

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

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

${\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}$

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

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

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

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

Оставили:	Правильно:
${\displaystyle L\land }$ правило: ${\displaystyle \quad {\cfrac {\Gamma ,A\land B\vdash \Delta }{\Gamma ,A,B\vdash \Delta }}}$	${\displaystyle R\land }$ правило: ${\displaystyle {\cfrac {\Gamma \vdash \Delta ,A\land B}{\Gamma \vdash \Delta ,A\qquad \Gamma \vdash \Delta ,B}}}$
${\displaystyle L\lor }$ правило: ${\displaystyle {\cfrac {\Gamma ,A\lor B\vdash \Delta }{\Gamma ,A\vdash \Delta \qquad \Gamma ,B\vdash \Delta }}}$	${\displaystyle R\lor }$ правило: ${\displaystyle \quad {\cfrac {\Gamma \vdash \Delta ,A\lor B}{\Gamma \vdash \Delta ,A,B}}}$
${\displaystyle L\rightarrow }$ правило: ${\displaystyle {\cfrac {\Gamma ,A\rightarrow B\vdash \Delta }{\Gamma \vdash \Delta ,A\qquad \Gamma ,B\vdash \Delta }}}$	${\displaystyle R\rightarrow }$ правило: ${\displaystyle \quad {\cfrac {\Gamma \vdash \Delta ,A\rightarrow B}{\Gamma ,A\vdash \Delta ,B}}}$
${\displaystyle L\lnot }$ правило: ${\displaystyle \quad {\cfrac {\Gamma ,\lnot A\vdash \Delta }{\Gamma \vdash \Delta ,A}}}$	${\displaystyle R\lnot }$ правило: ${\displaystyle \quad {\cfrac {\Gamma \vdash \Delta ,\lnot A}{\Gamma ,A\vdash \Delta }}}$
Аксиома:
${\displaystyle p,r\vdash q,r}$

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

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

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

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

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

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

Система LK

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

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

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

• ${\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 \exists }$.
• ${\displaystyle A[t/x]}$ обозначает формулу, которая получается заменой члена ${\displaystyle t}$ для каждого свободного вхождения переменной ${\displaystyle x}$ в формуле ${\displaystyle A}$ с ограничением, что срок ${\displaystyle t}$ должен быть свободен для переменной ${\displaystyle x}$ в ${\displaystyle A}$ (т.е. отсутствие каких-либо переменных в ${\displaystyle t}$ становится связанным в ${\displaystyle A[t/x]}$).
• ${\displaystyle WL}$, ${\displaystyle WR}$, ${\displaystyle CL}$, ${\displaystyle CR}$, ${\displaystyle PL}$, ${\displaystyle PR}$: Эти шесть означают две версии каждого из трех структурных правил; один для использования слева ('L') ${\displaystyle \vdash }$, а другой справа ('R'). Правила обозначаются аббревиатурой "W" для Ослабление (влево / вправо), 'C' для Сокращение, и 'P' для Перестановка.

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

Аксиома:	Резать:
${\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 \Delta }}\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 ({\exists }L)}$, переменная ${\displaystyle y}$ не должно происходить свободно где-либо в соответствующих нижних секвентах.

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

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

Хотя приведенные выше правила сформулированы формально, они допускают очень интуитивное прочтение с точки зрения классической логики. Рассмотрим, например, правило ${\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}$ держит. Так можно интерпретировать все правила.

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

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

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

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

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

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

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

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

${\displaystyle (I)}$ ${\displaystyle A\vdash A}$     ${\displaystyle (\lnot R)}$ ${\displaystyle \vdash \lnot A,A}$     ${\displaystyle (PR)}$ ${\displaystyle \vdash A,\lnot A}$              ${\displaystyle (I)}$ ${\displaystyle B\vdash B}$              ${\displaystyle (I)}$ ${\displaystyle C\vdash C}$         ${\displaystyle (\lor 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 \left(B\lor C\right),\lnot C,\left(B\rightarrow \lnot A\right)\vdash \lnot A}$     ${\displaystyle (\land 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 (\land 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 встраивает его в саму систему.

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

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

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

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

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

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

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

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

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

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

Варианты

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

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

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

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

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

Независимо от этого, можно также изменить способ разделения контекстов в правилах: ${\displaystyle ({\land }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 достаточно, чтобы превратить его в систему доказательств для интуиционистская логика.^[27] С этой целью нужно ограничиться секвентами с не более чем одной формулой в правой части и изменить правила, чтобы сохранить этот инвариант. Например, ${\displaystyle ({\lor }L)}$ переформулируется следующим образом (где C - произвольная формула):

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

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

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

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

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

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

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

Примечания

1. Гентцен 1934, Гентцен 1935.
2. Карри 1977, pp. 208–213, дает 5-страничное доказательство теоремы исключения. См. Также страницы 188, 250.
3. Клини 2009, pp. 453, дает очень краткое доказательство теоремы об исключении сечения.
4. Карри 1977, pp. 189–244, называет системы Gentzen LC системами. Карри уделяет больше внимания теории, чем доказательствам практической логики.
5. Клини 2009 С. 440–516. Эта книга гораздо больше посвящена теоретическим, метаматематическим последствиям секвенциального исчисления в стиле Генцена, чем приложениям к доказательствам практической логики.
6. Клини 2002, pp. 283–312, 331–361, определяет системы Генцена и доказывает различные теоремы внутри этих систем, включая теорему Геделя о полноте и теорему Генцена.
7. Смуллян 1995, pp. 101–127, дает краткое теоретическое описание систем Генцена. Он использует стиль макета табличного доказательства.
8. Карри 1977, pp. 184–244, сравниваются системы естественного вывода, обозначенные LA, и системы Генцена, обозначенные LC. Карри делает акцент скорее на теоретическом, чем на практическом.
9. Suppes 1999, pp. 25–150, представляет собой вводную презентацию практического естественного вывода такого рода. Это стало основой Система L.
10. Лимон 1965 это элементарное введение в практический естественный вывод, основанный на удобном сокращенном стиле макета доказательства Система L на основе Suppes 1999 С. 25–150.
11. Здесь «всякий раз, когда» используется как неформальное сокращение «для каждого присвоения значений свободным переменным в суждении».
12. Шанкар, Натараджан; Оуре, Сэм; Рашби, Джон М.; Стрингер-Калверт, Дэвид У. Дж. (2001-11-01). "Руководство по проверке PVS" (PDF). Гид пользователя. SRI International. Получено 2015-05-29.
13. Для объяснения дизъюнктивной семантики для правой части секвенций см. Карри 1977, стр. 189–190, Клини 2002, стр. 290, 297, Клини 2009, п. 441, г. Гильберт и Бернейс 1970, п. 385, г. Смуллян 1995, pp. 104–105 и Гентцен 1934, п. 180.
14. Автобус 1998, п. 10
15. Гентцен 1934, п. 188. "Der Kalkül" Нью-Джерси шляпа manche formale Unschönheiten ".
16. Гентцен 1934, п. 191. "In dem klassischen Kalkül NK nahm der Satz vom ausgeschlossenen Dritten eine Sonderstellung unter den Schlußweisen ein [...], indem er sich der Einführungs- und Beseitigungssystematik nicht einfügte. Bei dem im folgenden anzugebenden logistischen klassichen Kalkül LK wird 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ül nachher zu beweisenden 'Hauptsatzülnütherden da nbstimmtv».
19. Клини 2002, п. 441.
20. Прикладная логика, Univ. Корнелла: Лекция 9. Последнее обращение: 25.06.2016
21. "Помни, как ты доказывать ан значение предполагается, что гипотеза." —Филип Вадлер, 2 ноября 2015 г., в его Keynote: «Предложения как типы». Минута 14:36 ​​/ 55: 28 видеоклипа Code Mesh
22. Тейт WW (2010). "Оригинальное доказательство непротиворечивости Генцена и теорема Бара" (PDF). В Kahle R, Rathjen M (ред.). Столетие Гентцена: в поисках последовательности. Нью-Йорк: Спрингер. С. 213–228.
23. Ян фон Платон, Элементы логического рассуждения, Cambridge University Press, 2014, стр. 32.
24. Гентцен 1934 С. 190–193.
25. Смуллян 1995, п. 107
26. Клини 2002, п. 336, писал в 1967 году, что «это было важным логическим открытием Гентцена 1934-5, когда есть какое-либо (чисто логическое) доказательство предложения, есть прямое доказательство. Следствия этого открытия лежат в теоретико-логических исследованиях, а не в построении коллекций доказанных формул ».
27. Гентцен 1934, п. 194, писал: "Der Unterschied zwischen интуиционист унд klassischer Logik ist bei den Kalkülen ЖЖ унд LK äußerlich ganz anderer Art als bei Нью-Джерси унд NK. Dort bestand er in Weglassung bzw. Hinzunahme des Satzes vom ausgeschlossenen Dritten, während er hier durch die Sukzedensbedingung ausgedrückt wird. »Английский перевод:« Разница между интуиционистский и классический логика в случае исчислений ЖЖ и LK совершенно другого рода, чем случай Нью-Джерси и NK. В последнем случае оно заключалось в удалении или добавлении, соответственно, исключенного среднего правила, тогда как в первом случае оно выражается в последующих условиях ".
28. Структурная теория доказательства (CUP, 2001), Сара Негри и Ян ван Платон

Рекомендации

• Басс, Сэмюэл Р. (1998). «Введение в теорию доказательств». В Сэмюэле Р. Бассе (ред.). Справочник по теории доказательств. Эльзевир. С. 1–78. ISBN  0-444-89840-9.
• Карри, Хаскелл Брукс (1977) [1963]. Основы математической логики. Нью-Йорк: Dover Publications Inc. ISBN  978-0-486-63462-3.
• Генцен, Герхард Карл Эрих (1934). "Untersuchungen über das logische Schließen. I". Mathematische Zeitschrift. 39 (2): 176–210. Дои:10.1007 / BF01201353.
• Генцен, Герхард Карл Эрих (1935). "Untersuchungen über das logische Schließen. II". Mathematische Zeitschrift. 39 (3): 405–431. Дои: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]
• Краткое отступление: последовательное исчисление
• Интерактивное руководство по последовательному исчислению