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

Понятие секвенции для систематического использования в доказательствах в форме дерева вывода ввёл в 1929 году немецкий физик и логик Пауль Герц^[1], но целостного исчисления для какой-либо логической теории в его трудах построено не было^[2]. В работе 1932 года Генцен попытался развить подход Герца^[3], но в 1934 году отказался от наработок Герца: ввёл системы натурального вывода ${\displaystyle \mathbf {NK} }$ и ${\displaystyle \mathbf {NJ} }$ для классического и интуиционистского исчислений предикатов соответственно, использующие обычные тавтологии и деревья вывода, и, как их структурное развитие, — секвенциальные системы ${\displaystyle \mathbf {LK} }$ и ${\displaystyle \mathbf {LJ} }$. Для ${\displaystyle \mathbf {LK} }$ и ${\displaystyle \mathbf {LJ} }$ Генценом доказана устранимость сечения, что дало значительный методологический импульс намеченной Гильбертом теории доказательств: в той же работе Генцен впервые доказал полноту интуиционистского исчисления предикатов, а в 1936 году — доказал непротиворечивость аксиоматики Пеано для целых чисел, расширив её с помощью секвенциального варианта ${\displaystyle \mathbf {NK} }$ трансфинитной индукцией до ординала ${\displaystyle \epsilon _{0}}$. Последний результат имел также и особую идеологическую значимость в свете пессимизма начала 1930-х годов в связи с теоремой Гёделя о неполноте, согласно которой непротиворечивость арифметики невозможно установить её собственными средствами: нашлось достаточно естественное расширение арифметики логикой, устраняющее это ограничение.

Следующим значительным шагом в развитии секвенциальных исчислений стала разработка в 1944 году Ойвой Кетоненом исчисления для классической логики, все правила вывода в котором обратимы; тогда же Кетонен предложил декомпозиционный подход к поиску доказательств, использующий свойство обратимости^[4][5]. Опубликованное в 1949 году в диссертации Романа Сушко безаксиомное исчисление было близко по форме к построениям Герца, явившись первым воплощением для секвенциальных систем герцевского типа^[6][7].

В 1952 году Стивен Клини во «Введении в метаматематику» на основе исчисления Кетонена построил интуиционистское исчисление секвенций с обратимыми правилами вывода^[8], там же ввёл исчисления генценовского типа ${\displaystyle G3i}$ и ${\displaystyle G3c}$, в которых не требовались структурные^[⇨] правила вывода^[9], и, в целом, после публикации книги исчисления секвенций получили известность в широком кругу специалистов^[4].

Начиная с 1950-х годов основное внимание уделено переносу результатов о непротиворечивости и полноте на исчисления предикатов высших порядков, теории типов, неклассические логики. В 1953 году Гаиси Такеути построил исчисление секвенций для простой теории типов, выражающей исчисления предикатов высших порядков, и предположил, что для него имеет место устранимость сечений (гипотеза Такеути). В 1966 году Уильям Тэйт доказал устранимость сечений для логики второго порядка, вскоре гипотеза была полностью доказана в работах Мотоо Такахаси^[10] и Дага Правица. В 1970-е годы результаты значительно расширены: Драгалиным найдены доказательства устранимости сечений для серии неклассических логик высших порядков, а Жирар — для системы F.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Создано большое количество эквивалентных и удобных для тех или иных целей вариантов исчисления секвенций для классической и интуиционистской логик. Часть таких исчислений наследует построение Генцена, применённое при доказательстве непротиворечивости арифметики Пеано, и включает элементы систем натурального вывода, среди таковых — система Саппса 1957 года^[12] (почерпнутая из замечаний Фейса и Ладриера к французскому переводу статьи Генцена), и её усовершенствованная версия, опубликованная в 1965 году Леммоном^[13], устраняющие практические неудобства использования изначальной нутрально-секвенциальной Генцена^[14]. Более радикальные усовершенствования для практического удобства вывода натурального типа в секвенциальных исчислениях были предложены Хермесом^[15]: в его системе для классической логики применены две аксиомы (${\displaystyle A\rightarrow A}$ и ${\displaystyle \rightarrow A=A}$, а в правилах вывода пропозициональные связки используются не только в сукцедентах, но и в антецедентах, притом как в нижних, так и в верхних секвенциях^[16].

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