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

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

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

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

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

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

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

Обзор

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

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

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

${\displaystyle B}$

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

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

Системы натурального вычета

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

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

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

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

Слово «sequent» взято из слова «Sequenz» в статье Генцена 1934 года. ^[1] Клини делает следующий комментарий по поводу перевода на английский язык: «Гентцен говорит „Sequenz“, что мы переводим как „sequent“, потому что мы уже использовали „sequence“ для любой последовательности объектов, тогда как в немецком языке это „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]

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

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

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

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

Последовательное исчисление связано с другими аксиоматизациями классического исчисления высказываний, такими как пропозициональное исчисление Фреге или аксиоматизация Яна Лукасевича (которая сама является частью стандартной системы Гильберта ): Каждая формула, которая может быть доказана в них, имеет дерево редукции. Это можно показать следующим образом: Каждое доказательство в пропозициональном исчислении использует только аксиомы и правила вывода. Каждое использование схемы аксиом дает истинную логическую формулу и, таким образом, может быть доказано в секвенциальном исчислении; примеры для них приведены ниже. Единственное правило вывода в системах, упомянутых выше, — это 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) и правило (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 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). Интуитивное прочтение этого очевидно: каждая формула доказывает себя. Как и правило сечения, аксиома тождества несколько избыточна: полнота атомарных начальных секвенций утверждает, что правило может быть ограничено атомарными формулами без какой-либо потери доказуемости.

Обратите внимание, что все правила имеют зеркальные компаньоны, за исключением правил для импликации. Это отражает тот факт, что обычный язык логики первого порядка не включает связку "is not implied by", которая была бы дуальной для импликации по Де Моргану. Добавление такой связки с ее естественными правилами сделало бы исчисление полностью лево-правосимметричным. ${\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)}}$

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

Отношение к аналитическим таблицам

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

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

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

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

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

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

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

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

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

Варианты

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

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

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

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

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

Можно также изменить, будут ли правила с более чем одной предпосылкой использовать один и тот же контекст для каждой из этих предпосылок или разделять их контексты между ними: например, вместо этого можно сформулировать как ${\displaystyle ({\lor }L)}$

${\displaystyle {\cfrac {\Gamma ,A\vdash \Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\lor B\vdash \Delta ,\Pi }}.}$

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

Абсурд

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

${\displaystyle {\cfrac {\Gamma ,A\vdash C\qquad \Gamma ,B\vdash C}{\Gamma ,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. Curry 1977, стр. 189–244, называет системы Генцена системами LC. Карри больше внимания уделяет теории, чем практическим логическим доказательствам.
5. Kleene 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. Шанкар, Натараджан ; Оуре, Сэм; Рашби, Джон М.; Стрингер-Калверт, Дэвид У. Дж. (01.11.2001). "PVS Prover Guide" (PDF) . Руководство пользователя . SRI International . Получено 29.05.2015 .
13. Для объяснения дизъюнктивной семантики для правой части секвенций см. Curry 1977, стр. 189–190, Kleene 2002, стр. 290, 297, Kleene 2009, стр. 441, Hilbert & Bernays 1970, стр. 385, Smullyan 1995, стр. 104–105 и Gentzen 1934, стр. 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 логистишен klassichen 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' bestimmt und kann daher vorläufig nicht näher ründet werden."
19. Клини 2002, стр. 441.
20. Applied Logic, Univ. of Cornell: Lecture 9. Последнее обращение: 2016-06-25
21. "Помните, способ доказательства импликации заключается в принятии гипотезы " . — Филип Уодлер , 2 ноября 2015 г., в своем докладе: "Предложения как типы". Минута 14:36 ​​/55:28 видеоклипа Code Mesh
22. Tait WW (2010). «Оригинальное доказательство согласованности Генцена и теорема Бара» (PDF) . В Kahle R, Rathjen M (ред.). Gentzen's Centenary: The Quest for Consistency . New York: Springer. стр. 213–228.
23. Ян фон Платон, Элементы логического рассуждения , Cambridge University Press, 2014, стр. 32.
24. Анджей-Инджейчак, Введение в теорию и применение пропозициональных секвенциальных исчислений (2021, глава «Гентценовское секвенциальное исчисление LK»). Доступ 3 августа 2022 г.
25. Смаллиан 1995, стр. 107
26. Kleene 2002, стр. 336, писал в 1967 году, что «главным логическим открытием Генцена 1934–5 было то, что, когда есть какое-либо (чисто логическое) доказательство предложения, есть и прямое доказательство. Последствия этого открытия заключаются в теоретических логических исследованиях, а не в построении коллекций доказанных формул».
27. Генцен 1934, с. 194, писал: «Der Unterschied zwischen intuitionistischer und klassischer Logik ist bei den Kalkülen LJ und LK äußerlich ganz anderer Art als bei NJ und NK . Dort bestand er in Weglassung bzw. Hinzunahme des Satzes vom ausgeschlossenen Dritten, während er hier durch die Sukzedensbedingung ausgedrückt wird." Английский перевод: «Разница между интуиционистской и классической логикой в ​​случае исчислений LJ и LK совершенно иная, чем в случае NJ и NK . В последнем случае она заключалась в удалении или добавлении соответственно правило исключенного среднего, тогда как в первом случае оно выражается через последующие условия».
28. М. Темкин, «Доказательство недоказуемости», стр. 22–26. В трудах Третьего ежегодного симпозиума по логике в информатике, 5–8 июля 1988 г. (1988), IEEE. ISBN 0-8186-0853-6.

Ссылки

• Басс, Сэмюэл Р. (1998). «Введение в теорию доказательств». В Сэмюэле Р. Бассе (ред.). Справочник по теории доказательств. Elsevier. стр. 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. S2CID  121546341.
• Генцен, Герхард Карл Эрих (1935). «Untersuchungen über das logische Schließen. II». Mathematische Zeitschrift . 39 (3): 405–431. дои : 10.1007/bf01201363. S2CID  186239837.
• Жирар, Жан-Ив ; Пол Тейлор; Ив Лафон (1990) [1989]. Доказательства и типы . Cambridge University Press (Cambridge Tracts in Theoretical Computer Science, 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.
• Манкосу, Паоло; Гальван, Серджио; Зак, Ричард (2021). Введение в теорию доказательств — Нормализация, исключение сечений и доказательства согласованности . Oxford University Press . стр. 431. ISBN 978-0-19-289593-6.
• Смаллиан, Рэймонд Меррилл (1995) [1968]. Логика первого порядка . Нью-Йорк: Dover Publications. ISBN 978-0-486-68370-6.
• Suppes, Patrick Colonel (1999) [1957]. Введение в логику . Минеола, Нью-Йорк: Dover Publications. ISBN 978-0-486-40687-9.

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

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