Исчисление секвенций

Исчисление секвенций — вариант логических исчислений, использующий для доказательства утверждений не произвольные цепочки тавтологий, а последовательности условных суждений — секвенций. Наиболее известные исчисления секвенций — $\mathbf {LK}$ и $\mathbf {LJ}$ для классического и интуиционистского исчислений предикатов — построены Генценом в 1934 году, позднее сформулированы секвенциальные варианты для широкого класса прикладных исчислений (арифметики, анализа), теорий типов, неклассических логик.

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

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

История

Понятие секвенции для систематического использования в доказательствах в форме дерева вывода ввёл в 1929 году немецкий физик и логик Пауль Герц (нем. Paul Hertz; 1881–1940), но целостного исчисления для какой-либо логической теории в его трудах построено не было. В работе 1932 года Генцен попытался развить подход Герца, но в 1934 году отказался от наработок Герца: ввёл системы натурального вывода $\mathbf {NK}$ и $\mathbf {NJ}$ для классического и интуиционистского исчислений предикатов соответственно, использующие обычные тавтологии и деревья вывода, и, как их структурное развитие, — секвенциальные системы $\mathbf {LK}$ и $\mathbf {LJ}$. Для $\mathbf {LK}$ и $\mathbf {LJ}$ Генценом доказана устранимость сечения, что дало значительный методологический импульс намеченной Гильбертом теории доказательств: в той же работе Генцен впервые доказал полноту интуиционистского исчисления предикатов, а в 1936 году — доказал непротиворечивость аксиоматики Пеано для целых чисел, расширив её с помощью секвенциального варианта $\mathbf {NK}$ трансфинитной индукцией до ординала $\epsilon _{0}$. Последний результат имел также и особую идеологическую значимость в свете пессимизма начала 1930-х годов в связи с теоремой Гёделя о неполноте, согласно которой непротиворечивость арифметики невозможно установить её собственными средствами: нашлось достаточно естественное расширение арифметики логикой, устраняющее это ограничение.

Следующим значительным шагом в развитии секвенциальных исчислений стала разработка в 1944 году Ойвой Кетоненом (фин. Oiva Ketonen; 1913—2000) исчисления для классической логики, все правила вывода в котором обратимы; тогда же Кетонен предложил декомпозиционный подход к поиску доказательств, использующий свойство обратимости. Опубликованное в 1949 году в диссертации Романа Сушко безаксиомное исчисление было близко по форме к построениям Герца, явившись первым воплощением для секвенциальных систем герцевского типа.

В 1952 году Стивен Клини во «Введении в метаматематику» на основе исчисления Кетонена построил интуиционистское исчисление секвенций с обратимыми правилами вывода, там же ввёл исчисления генценовского типа $G3i$ и $G3c$, в которых не требовались структурные правила вывода, и, в целом, после публикации книги исчисления секвенций получили известность в широком кругу специалистов.

Начиная с 1950-х годов основное внимание уделено переносу результатов о непротиворечивости и полноте на исчисления предикатов высших порядков, теории типов, неклассические логики. В 1953 году Гаиси Такеути (яп. 竹内外史; 1926—2017) построил исчисление секвенций для простой теории типов, выражающей исчисления предикатов высших порядков, и предположил, что для него имеет место устранимость сечений (гипотеза Такеути). В 1966 году Уильям Тэйт (англ. род. 1929) доказал устранимость сечений для логики второго порядка, вскоре гипотеза была полностью доказана в работах Мотоо Такахаси и Дага Правица (швед. Dag Prawitz; род. 1936). В 1970-е годы результаты значительно расширены: Драгалиным найдены доказательства устранимости сечений для серии неклассических логик высших порядков, а Жирар — для системы F.

Начиная с 1980-х годов секвенциальные системы играют ключевую роль в развитии систем автоматического доказательства, в частности, разработанное Тьерри Коканом и Жераром Юэ в 1986 году секвенциальное исчисление конструкций — полиморфное λ-исчисление высшего порядка с зависимыми типами, занимающее высшую точку в λ-кубе Барендрегта — используется как основа программной системы Coq.

Основные понятия

Секвенцией называется выражение вида $\Gamma \rightarrow \Delta$, где $\Gamma$ и $\Delta$ — конечные (возможно пустые) последовательности логических формул, называемые цедентами: $\Gamma$ — антецедентом, а $\Delta$ — сукцедентом (иногда — консеквентом). Интуитивный смысл, закладываемый в секвенцию $A_{1},\ldots ,A_{n}\rightarrow B_{1},\ldots ,B_{m}$ — если выполнена конъюнкция формул антецедента $A_{1}\land \ldots \land A_{n}$, то имеет место (выводится) дизъюнкция формул сукцедента $B_{1}\lor \ldots \lor B_{m}$. Иногда вместо стрелки в обозначении секвенции используется знак выводимости ($\Gamma \vdash \Delta$) или знак импликации ($\Gamma \Rightarrow \Delta$).

Если антецедент пуст ($\rightarrow B_{1},\ldots ,B_{m}$), то подразумевается выполнение дизъюнкции формул сукцедента $B_{1}\lor \ldots \lor B_{m}$; пустой сукцедент ($A_{1},\ldots ,A_{n}\rightarrow$) интерпретируется как противоречивость конъюнкции формул антецедента. Пустая секвенция $\rightarrow$ означает, что в рассматриваемой системе имеется противоречие. Порядок формул в цедентах значимым не является, однако количество вхождений экземпляра формулы в цедент имеет значение. Запись в цедентах в виде $A,\Gamma$ или $\Gamma ,A$, где $\Gamma$ — последовательность формул, а $A$ — формула, означает добавление формулы $A$ в цедент (возможно, в ещё одном экземпляре).

Аксиомами считаются исходные секвенции, принимаемые без доказательств; в секвенциальном подходе число аксиом минимизируется, так, в генценовских исчислениях $\mathrm {LK}$ и $\mathrm {LJ}$ задаётся только одна схема аксиом — $A\rightarrow A$. Правила вывода в секвенциальной форме записываются как следующие выражения:

${\cfrac {\;S_{1}\;}{T}}$ и ${\cfrac {\;S_{1}\;\;\;S_{2}\;}{\;\;T}}$,

интерпретируются они как утверждение о выводимости из верхней секвенции $S_{1}$ (верхних секвенций $S_{1}$ и $S_{2}$) нижней секвенции $T$. Доказательство в секвенциальных исчислениях (как и в системах натурального вывода) записывается в древовидной форме сверху вниз, например:

${\cfrac {{\cfrac {\;S_{1}\;\;\;S_{2}\;}{\;T_{1}}}\;\;\;\;{\cfrac {\;S_{3}\;}{T_{2}}}}{U}}$,

где каждая черта означает непосредственный вывод — переход от верхних секвенций к нижней согласно какому-либо из принятых в данной системе правил вывода. Таким образом, существование дерева вывода, начинающегося от аксиом (начальных секвенций), и приводящих к секвенции $S$, означает её выводимость в данной логической системе: $\vDash S$.

Классическое генценовское исчисление секвенций

Наиболее часто применяемым исчислением секвенций для классического исчисления предикатов является система $\mathbf {LK}$, построенная Генценом в 1934 году. В системе одна схема аксиом — $A\rightarrow A$ и 21 правило вывода, которые делятся на структурные и логические.

Структурные правила ($A$, $B$ — формулы, $\Gamma$, $\Delta$, $\Theta$, $\Lambda$ — списки формул):

• ослабление слева: ${\cfrac {\qquad \Gamma \ \rightarrow \ \Delta \ }{\ A,\ \Gamma \ \rightarrow \ \Delta }}$ и справа: ${\cfrac {\Gamma \ \rightarrow \ \Delta \quad }{\ \Gamma \ \rightarrow \ \Delta ,\ A}}$;
• сокращение слева: ${\cfrac {\,\,A,\ A,\ \Gamma \ \rightarrow \ \Delta }{\qquad A,\ \Gamma \ \rightarrow \ \Delta \ }}$ и справа: ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A,\ A}{\,\,\,\Gamma \ \rightarrow \ \Delta ,\ A\qquad }}$;
• перестановка слева: ${\cfrac {\ \Gamma ,\ A,\ B,\ \Theta \ \rightarrow \ \Delta \ }{\ \Gamma ,\ B,\ A,\ \Theta \ \rightarrow \ \Delta }}$ и справа: ${\cfrac {\ \Gamma \ \rightarrow \ \Delta ,\ A,\ B,\ \Lambda \ }{\ \Gamma \ \rightarrow \ \Delta ,\ B,\ A,\ \Lambda \ }}$,
• сечение: ${\cfrac {\ \Gamma \ \rightarrow \ \Delta ,\ A\qquad A,\ \Theta \ \rightarrow \ \Lambda \ }{\Gamma ,\ \Theta \ \rightarrow \ \Delta ,\ \Lambda }}$.

Логические пропозициональные правила предназначены для добавления в вывод пропозициональных связок:

• $\lnot$-слева: ${\cfrac {\qquad \Gamma \ \rightarrow \ \Delta ,\ A}{\ \lnot A,\ \Gamma \ \rightarrow \ \Delta \qquad }}$; $\lnot$-справа: ${\cfrac {A,\ \Gamma \ \rightarrow \ \Delta \qquad }{\qquad \Gamma \ \rightarrow \ \Delta ,\ \lnot A\ }}$;
• $\land$-слева: ${\cfrac {\qquad A,\ \Gamma \ \rightarrow \ \Delta }{\ A\land B,\ \Gamma \ \rightarrow \ \Delta \ }}$ и ${\cfrac {\qquad B,\ \Gamma \ \rightarrow \ \Delta }{\ A\land B,\ \Gamma \ \rightarrow \ \Delta \ }}$; $\land$-справа: ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A\qquad \Gamma \ \rightarrow \ \Delta ,\ B}{\ \qquad \ \Gamma \ \rightarrow \ \Delta ,\ A\land B\ }}$,
• $\lor$-слева: $\ {\cfrac {A,\ \Gamma \ \rightarrow \ \Delta \qquad B,\ \Gamma \ \rightarrow \ \Delta \ }{\ A\lor B,\ \Gamma \ \rightarrow \ \Delta \ \qquad }}$; $\lor$-справа: ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A\qquad }{\ \Gamma \ \rightarrow \ \Delta ,\ A\lor B\ }}$ и ${\cfrac {\Gamma \rightarrow \Delta ,\ B\qquad }{\ \Gamma \rightarrow \Delta ,\ A\lor B\ }}$,
• $\Rightarrow$-слева: $\ {\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A\qquad \qquad B,\ \Theta \ \rightarrow \ \Lambda \ }{A\Rightarrow B,\ \Gamma ,\ \Theta \ \rightarrow \ \Delta ,\Lambda \qquad }}$ и $\Rightarrow$-справа: ${\cfrac {A,\ \Gamma \ \rightarrow \ \Delta ,\ B\qquad }{\qquad \Gamma \ \rightarrow \ \Delta ,\ A\Rightarrow B\ }}$.

Логические кванторные правила вводят кванторы всеобщности и существования в вывод ($F(a)$ — формула со свободной переменной $a$, $t$ — произвольный терм, а $F(t)$ — замена всех вхождений свободной переменной $a$ на терм $t$):

• $\forall$-слева: ${\cfrac {\qquad F(t),\ \Gamma \ \rightarrow \ \Delta }{\ \forall x:F(x),\ \Gamma \ \rightarrow \ \Delta \ }}$ и $\forall$-справа: ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ F(a)\qquad }{\ \Gamma \ \rightarrow \ \Delta ,\ \forall x:F(x)}}$;
• $\exists$-слева: ${\cfrac {\qquad F(a),\ \Gamma \ \rightarrow \ \Delta }{\ \exists x:F(x),\ \Gamma \ \rightarrow \ \Delta \ }}$ и $\exists$-справа: ${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ F(t)\qquad }{\ \Gamma \ \rightarrow \ \Delta ,\ \exists x:F(x)}}$.

Дополнительное условие в кванторных правилах — невхождение свободной переменной $a$ в нижние формулы секвенций в правилах $\forall$-справа и $\exists$-слева.

Пример $\mathbf {LK}$-вывода закона исключённого третьего:

${\cfrac {\cfrac {\cfrac {\cfrac {\cfrac {A\ \rightarrow \ A\qquad }{\qquad \quad \rightarrow \ A,\ \lnot A\qquad }}{\qquad \qquad \rightarrow \ A,\ A\lor \lnot A\quad }}{\qquad \quad \rightarrow \ A\lor \lnot A,\ A}}{\qquad \qquad \qquad \ \rightarrow \ A\lor \lnot A,\ A\lor \lnot A\quad }}{\quad \ \rightarrow \ A\lor \lnot A}}$

— в нём вывод начат с единственной аксиомы, далее — последовательно применены правила $\lnot$-справа, $\lor$-справа, перестановка справа, $\lor$-справа и сокращение справа.

Исчисление $\mathbf {LK}$ эквивалентно классическому исчислению предикатов первой ступени: формула $A$ общезначима в исчислении предикатов тогда и только тогда, когда в $\mathbf {LK}$ выводима секвенция $\rightarrow A$. Ключевой результат, который назван Генценом «основной теоремой» (нем. Hauptsatz) — возможность провести любой $\mathbf {LK}$-вывод без применения правила сечения, именно благодаря этому свойству устанавливаются все основные свойства $\mathbf {LK}$, в том числе корректность, непротиворечивость и полнота.

Интуиционистское генценовское исчисление секвенций

Исчисление $\mathbf {LJ}$ получается из $\mathbf {LK}$ добавлением ограничения на сукцеденты секвенций в правилах вывода: в них допустимо использование только одной формулы, а правила перестановки справа и сокращения справа (оперирующие с нескольким формулами в сукцедентах) исключаются. Таким образом, при минимальных модификациях получается система, в которой невыводимы законы двойного отрицания и исключённого третьего, но действуют все прочие основные логические законы, и, например, выводима эквивалентность $\lnot \lnot \lnot A\Leftrightarrow \lnot A$. Полученная система эквивалентна интуиционистскому исчислению предикатов с аксиоматикой Гейтинга. В исчислении $\mathbf {LJ}$ также устранимы сечения, оно также корректно, непротиворечиво и полно, притом последний результат для интуиционистского исчисления предикатов впервые получен именно для $\mathbf {LJ}$.

Нестандартные исчисления секвенций

Создано большое количество эквивалентных и удобных для тех или иных целей вариантов исчисления секвенций для классической и интуиционистской логик. Часть таких исчислений наследует построение Генцена, применённое при доказательстве непротиворечивости арифметики Пеано, и включает элементы систем натурального вывода, среди таковых — система Саппса (англ. Patrick Suppes; 1922–2014) 1957 года (почерпнутая из замечаний Фейса и Ладриера к французскому переводу статьи Генцена), и её усовершенствованная версия, опубликованная в 1965 году Леммоном (англ. John Lemmon; 1930–1966), устраняющие практические неудобства использования изначальной нутрально-секвенциальной Генцена. Более радикальные усовершенствования для практического удобства вывода натурального типа в секвенциальных исчислениях были предложены Хермесом (нем. Hans Hermes; 1912–2003): в его системе для классической логики применены две аксиомы ($A\rightarrow A$ и $\rightarrow A=A$, а в правилах вывода пропозициональные связки используются не только в сукцедентах, но и в антецедентах, притом как в нижних, так и в верхних секвенциях.

Симметрия

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

Литература

• Секвенций исчисление // Сафлор — Соан. — М. : Советская энциклопедия, 1976. — С. 181—182; ст. 530—532. — (Большая советская энциклопедия : [в 30 т.] / гл. ред. А. М. Прохоров ; 1969—1978, т. 23).
• Драгалин А. Г. Секвенций исчисление // Математическая энциклопедия : [в 5 т.] / Гл. ред. И. М. Виноградов. — М.: Советская энциклопедия, 1984. — Т. 4: Ок — Сло. — С. 1104. — 1216 стб. : ил. — 150 000 экз.
• Быстров П. И. Исчисление секвенций // Новая философская энциклопедия / Ин-т философии РАН; Нац. обществ.-науч. фонд; Предс. научно-ред. совета В. С. Стёпин, заместители предс.: А. А. Гусейнов, Г. Ю. Семигин, уч. секр. А. П. Огурцов. — 2-е изд., испр. и допол. — М.: Мысль, 2010. — ISBN 978-5-244-01115-9.
• Генцен Г. Исследования логических выводов = Untersuchungen über das logische Schließen // Mathematische Zeitschrift, Bd. 39 (1934–1935), S. 405–431 // Идельсон А. В., Минц Г. Е. Математическая теория логического вывода / перевод А. В. Идельсона. — М.: Наука, 1967. — С. 9—76.
• Драгалин А. Г. Математический интуиционизм. Введение в теорию доказательств. — М.: Наука, 1979. — 256 с. — (Математическая логика и основания математики).
• Клини С. Введение в метаматематику / перевод с английского А. С. Есенина-Вольпина под редакцией В. А. Успенского. — М.: ИЛ, 1958. — 527 с.
• Такеути Г. Теория доказательств. — М.: Мир, 1978. — 412 с.
• Indrzejczak A. A Survey of Nonstandard Sequent Calculi // Studia Logica. — 2014. — Декабрь (т. 102, № 6). — С. 1295–1322. — doi:10.1007/s11225-014-9567-y.
• Jan von Plato. The Development of Proof Theory  (неопр.). Stanford Encyclopaedia of Philosophy (16 апреля 2008).