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

Стиль формальной логической аргументации

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

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

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

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

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

Обзор

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

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

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

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

или как

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

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

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

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

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

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

В случае первого решения мы перепишем as и снова разделим секвенцию, чтобы получить: ${\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]

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

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

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

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

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

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

Система ЛК

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

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

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

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

Вышеуказанные правила можно разделить на две большие группы: логические и структурные . Каждое из логических правил вводит новую логическую формулу либо слева, либо справа от турникета . Напротив, структурные правила действуют на структуру секвенций, игнорируя точную форму формул. Двумя исключениями из этой общей схемы являются аксиома тождества (I) и правило (Отсечения). ${\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 A[y/x]}$ ${\displaystyle A[y/x]}$

Вместо того, чтобы рассматривать правила как описания юридических выводов в логике предикатов, их можно также рассматривать как инструкции по построению доказательства для данного утверждения. В этом случае правила можно читать снизу вверх; например, говорит, что для доказательства того, что следует из предположений и , достаточно доказать, что можно заключить из и можно заключить из , соответственно. Обратите внимание, что, учитывая некоторую предысторию, неясно, как это разделить на и . Однако существует лишь конечное число возможностей, подлежащих проверке, поскольку антецедент по предположению конечен. Это также иллюстрирует, как теорию доказательств можно рассматривать как комбинаторную обработку доказательств: учитывая доказательства для обоих и , можно построить доказательство для . ${\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 (\forall R)}$ ${\displaystyle (\exists L)}$

Что-то более интересное мы докажем . Вывод найти несложно, что иллюстрирует полезность 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)}}$

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

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

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

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

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

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

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

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

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

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

В секвенциальном исчислении допустимо правило отсечения . Этот результат также известен как Hauptsatz Генцена («Основная теорема»). ^{[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 }$

Абсурд

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

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

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

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

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

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

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

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

Удивительно, но некоторых небольших изменений в правилах ЛК оказывается достаточно, чтобы превратить ее в систему доказательств для интуиционистской логики . ^[27] С этой целью необходимо ограничиться секвенциями с не более чем одной формулой в правой части, ^[28] и изменить правила, чтобы сохранить этот инвариант. Например, переформулируется следующим образом (где 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 {\to }R}$ ${\displaystyle ({\forall }R)}$ ${\displaystyle ({\to }R)}$ ${\displaystyle ({\forall }R)}$

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

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

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

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

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

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

Примечания

1. Генцен 1934, Генцен 1935.
2. Curry 1977, стр. 208–213, дает 5-страничное доказательство теоремы исключения. См. также стр. 188, 250.
3. Kleene 2009, стр. 453, дает очень краткое доказательство теоремы об исключении разреза.
4. Карри 1977, стр. 189–244, называет системы Генцена LC-системами. Акцент Карри делается больше на теории, чем на практических логических доказательствах.
5. Клини 2009, стр. 440–516. Эта книга гораздо больше посвящена теоретическим, метаматематическим последствиям секвентивного исчисления в стиле Генцена, чем приложениям к практическим логическим доказательствам.
6. Kleene 2002, стр. 283–312, 331–361, определяет системы Генцена и доказывает различные теоремы в этих системах, включая теорему Гёделя о полноте и теорему Генцена.
7. Smullyan 1995, стр. 101–127, дает краткое теоретическое представление систем Генцена. Он использует стиль макета табличного доказательства.
8. Карри 1977, стр. 184–244, сравнивает естественные системы дедукции, обозначенные LA, и системы Генцена, обозначенные LC. Акцент Карри носит скорее теоретический, чем практический характер.
9. Suppes 1999, стр. 25–150, представляет собой вводное изложение практических естественных выводов такого рода. Это стало основой Системы L.
10. Lemmon 1965 представляет собой элементарное введение в практический естественный вывод, основанное на удобном стиле сокращенной схемы доказательства System L , основанном на Suppes 1999, стр. 25–150.
11. Здесь «всякий раз» используется как неформальное сокращение «для каждого присвоения значений свободным переменным в решении»
12. Шанкар, Натараджан ; Оуре, Сэм; Рашби, Джон М .; Стрингер-Калверт, Дэвид У.Дж. (1 ноября 2001 г.). «Руководство по проверке PVS» (PDF) . Гид пользователя . НИИ Интернешнл . Проверено 29 мая 2015 г.
13. Объяснения дизъюнктивной семантики правой части секвенций см. в Curry 1977, стр. 189–190, Kleene 2002, стр. 290, 297, Kleene 2009, p. 441, Гильберт и Бернейс 1970, с. 385, Смуллян 1995, стр. 104–105 и Генцен 1934, стр. 104–105. 180.
14. Басс 1998, с. 10
15. Генцен 1934, с. 188. «Der Kalkül NJ шляпа формального 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 Logischen Klassichen Kalkül L K 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. не уверен."
19. Клини 2002, с. 441.
20. Прикладная логика, Univ. Корнеллского университета: Лекция 9. Последнее посещение: 25 июня 2016 г.
21. «Помните, что вы можете доказать импликацию , приняв гипотезу » . — Филип Уодлер , 2 ноября 2015 г., в своем основном докладе: «Предложения как типы». Минута 14:36/55:28 видеоклипа Code Mesh
22. Тейт WW (2010). «Оригинальное доказательство непротиворечивости Генцена и теорема Бара» (PDF) . Кале Р., Ратьен М. (ред.). Столетие Генцена: В поисках последовательности . Нью-Йорк: Спрингер. стр. 213–228.
23. Ян фон Платон, Элементы логического рассуждения , Cambridge University Press, 2014, стр. 32.
24. Анджей-Инджейчак, Введение в теорию и приложения пропозиционального секвентивного исчисления (2021, глава «Секвентивное исчисление Генцена LK»). По состоянию на 3 августа 2022 г.
25. Смуллян 1995, с. 107
26. Клини 2002, с. 336, писал в 1967 году, что «важным логическим открытием Генцена (1934–1935 гг.) было то, что, когда есть какое-либо (чисто логическое) доказательство предложения, существует и прямое доказательство. Смысл этого открытия лежит в теоретических логических исследованиях, а не создавать коллекции доказанных формул».
27. Генцен 1934, с. 194, писал: «Der Unterschied zwischen intuitionistischer und klassischer Logik ist bei den Kalkülen LJ und LK außerlich ganz anderer Art als bei NJ und NK . Dort bestand er in Weglassung bzw. Hinzunahme des Satzes vom ausgeschlossenen Dritten, während er hier durch die Sukzedensbedingung ausgedrückt вирд." Английский перевод: «Разница между интуиционистской и классической логикой в ​​случае исчислений LJ и LK совершенно иного рода, чем в случае NJ и NK . В последнем случае она заключалась в удалении или добавлении соответственно правило исключенного среднего, тогда как в первом случае оно выражается через последующие условия».
28. М. Темкин, "Доказательство недоказуемости", стр.22--26. В материалах третьего ежегодного симпозиума по логике в информатике, 5–8 июля 1988 г. (1988), IEEE. ISBN 0-8186-0853-6.

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

• Басс, Сэмюэл Р. (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. дои : 10.1007/BF01201353. S2CID  121546341.
• Генцен, Герхард Карл Эрих (1935). «Untersuchungen über das logische Schließen. II». Mathematische Zeitschrift . 39 (3): 405–431. дои : 10.1007/bf01201363. S2CID  186239837.
• Жирар, Жан-Ив ; Пол Тейлор; Ив Лафон (1990) [1989]. Доказательства и типы . Издательство Кембриджского университета (Кембриджские трактаты по теоретической информатике, 7). ISBN 0-521-37181-3.
• Гильберт, Дэвид ; Бернейс, Пол (1970) [1939]. Grundlagen der Mathematik II (второе изд.). Берлин, Нью-Йорк: Springer-Verlag. ISBN 978-3-642-86897-9.
• Клини, Стивен Коул (2009) [1952]. Введение в метаматематику . Иши Пресс Интернешнл. ISBN 978-0-923891-57-2.
• Клини, Стивен Коул (2002) [1967]. Математическая логика . Минеола, Нью-Йорк: Dover Publications. ISBN 978-0-486-42533-7.
• Леммон, Эдвард Джон (1965). Начало логики . Томас Нельсон. ISBN 0-17-712040-1.
• Манкосу, Паоло; Гальван, Серджио; Зак, Ричард (2021). Введение в теорию доказательств — нормализация, исключение разрезов и доказательства непротиворечивости . Издательство Оксфордского университета . п. 431. ИСБН 978-0-19-289593-6.
• Смуллян, Раймонд Меррилл (1995) [1968]. Логика первого порядка . Нью-Йорк: Dover Publications. ISBN 978-0-486-68370-6.
• Суппес, Патрик Полковник (1999) [1957]. Введение в логику . Минеола, Нью-Йорк: Dover Publications. ISBN 978-0-486-40687-9.

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

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