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

Исчисление секвенций — вариант логических исчислений, использующий для доказательства утверждений не произвольные цепочки тавтологий, а последовательности условных суждений — секвенцийШаблон:Переход. Наиболее известные исчисления секвенций — $𝐋𝐊$Шаблон:Переход и $𝐋𝐉$Шаблон:Переход для классического и интуиционистского исчислений предикатов — построены Генценом в 1934 году, позднее сформулированы секвенциальные варианты для широкого класса прикладных исчислений (арифметики, анализа), теорий типов, неклассических логик.

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

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

История

Понятие секвенции для систематического использования в доказательствах в форме дерева вывода ввёл в 1929 году немецкий физик и логик Шаблон:Нп2, но целостного исчисления для какой-либо логической теории в его трудах построено не былоШаблон:Sfn. В работе 1932 года Генцен попытался развить подход Герца, но в 1934 году отказался от наработок Герца: ввёл системы натурального вывода $𝐍𝐊$ и $𝐍𝐉$ для классического и интуиционистского исчислений предикатов соответственно, использующие обычные тавтологии и деревья вывода, и, как их структурное развитие, — секвенциальные системы $𝐋𝐊$ и $𝐋𝐉$. Для $𝐋𝐊$ и $𝐋𝐉$ Генценом доказана устранимость сечения, что дало значительный методологический импульс намеченной Гильбертом теории доказательств: в той же работе Генцен впервые доказал полноту интуиционистского исчисления предикатов, а в 1936 году — доказал непротиворечивость аксиоматики Пеано для целых чисел, расширив её с помощью секвенциального варианта $𝐍𝐊$ трансфинитной индукцией до ординала ${ϵ}_0$. Последний результат имел также и особую идеологическую значимость в свете пессимизма начала 1930-х годов в связи с теоремой Гёделя о неполноте, согласно которой непротиворечивость арифметики невозможно установить её собственными средствами: нашлось достаточно естественное расширение арифметики логикой, устраняющее это ограничение.

Следующим значительным шагом в развитии секвенциальных исчислений стала разработка в 1944 году Шаблон:Нп2 исчисления для классической логики, все правила вывода в котором обратимы; тогда же Кетонен предложил декомпозиционный подход к поиску доказательств, использующий свойство обратимостиШаблон:Sfn. Опубликованное в 1949 году в диссертации Романа Сушко безаксиомное исчисление было близко по форме к построениям Герца, явившись первым воплощением для секвенциальных систем герцевского типаШаблон:Sfn.

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

Начиная с 1950-х годов основное внимание уделено переносу результатов о непротиворечивости и полноте на исчисления предикатов высших порядков, теории типов, неклассические логики. В 1953 году Шаблон:Нп2 построил исчисление секвенций для простой теории типов, выражающей исчисления предикатов высших порядков, и предположил, что для него имеет место устранимость сечений (гипотеза Такеути). В 1966 году Шаблон:Нп2 доказал устранимость сечений для логики второго порядка, вскоре гипотеза была полностью доказана в работах Мотоо Такахаси и Шаблон:Нп2. В 1970-е годы результаты значительно расширены: Драгалиным найдены доказательства устранимости сечений для серии неклассических логик высших порядков, а Шаблон:Iw — для системы F.

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

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

Шаблон:ЯкорьСеквенцией называется выражение вида $\mathrm{\Gamma }\to \mathrm{\Delta }$, где $\mathrm{\Gamma }$ и $\mathrm{\Delta }$ — конечные (возможно пустые) последовательности логических формул, называемые цедентами: $\mathrm{\Gamma }$ — антецедентом, а $\mathrm{\Delta }$ — сукцедентом (иногда — консеквентом). Интуитивный смысл, закладываемый в секвенцию $A_1,\dots ,A_n\to B_1,\dots ,B_m$ — если выполнена конъюнкция формул антецедента $A_1\wedge \dots \wedge A_n$, то имеет место (выводится) дизъюнкция формул сукцедента $B_1\vee \dots \vee B_m$. Иногда вместо стрелки в обозначении секвенции используется знак выводимости ($\mathrm{\Gamma }⊢\mathrm{\Delta }$) или знак импликации ($\mathrm{\Gamma }\Rightarrow \mathrm{\Delta }$).

Шаблон:ЯкорьЕсли антецедент пуст ($\to B_1,\dots ,B_m$), то подразумевается выполнение дизъюнкции формул сукцедента $B_1\vee \dots \vee B_m$; пустой сукцедент ($A_1,\dots ,A_n\to$) интерпретируется как противоречивость конъюнкции формул антецедента. Пустая секвенция $\to$ означает, что в рассматриваемой системе имеется противоречие. Порядок формул в цедентах значимым не является, однако количество вхождений экземпляра формулы в цедент имеет значение. Запись в цедентах в виде $A,\mathrm{\Gamma }$ или $\mathrm{\Gamma },A$, где $\mathrm{\Gamma }$ — последовательность формул, а $A$ — формула, означает добавление формулы $A$ в цедент (возможно, в ещё одном экземпляре).

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

$\frac{S_1}{T}$ и $\frac{S_1{S}_2}{T}$,

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

$\frac{\frac{S_1{S}_2}{T_1}\frac{S_3}{T_2}}{U}$,

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

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

Наиболее часто применяемым исчислением секвенций для классического исчисления предикатов является система $𝐋𝐊$, построенная Генценом в 1934 году. В системе одна схема аксиом — $A\to A$ и 21 правило вывода, которые делятся на структурные и логическиеШаблон:Sfn.

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

• ослабление слева: $\frac{\mathrm{\Gamma }\to \mathrm{\Delta }}{A,\mathrm{\Gamma }\to \mathrm{\Delta }}$ и справа: $\frac{\mathrm{\Gamma }\to \mathrm{\Delta }}{\mathrm{\Gamma }\to \mathrm{\Delta },A}$;
• сокращение слева: $\frac{A,A,\mathrm{\Gamma }\to \mathrm{\Delta }}{A,\mathrm{\Gamma }\to \mathrm{\Delta }}$ и справа: $\frac{\mathrm{\Gamma }\to \mathrm{\Delta },A,A}{\mathrm{\Gamma }\to \mathrm{\Delta },A}$;
• перестановка слева: $\frac{\mathrm{\Gamma },A,B,\mathrm{\Theta }\to \mathrm{\Delta }}{\mathrm{\Gamma },B,A,\mathrm{\Theta }\to \mathrm{\Delta }}$ и справа: $\frac{\mathrm{\Gamma }\to \mathrm{\Delta },A,B,\mathrm{\Lambda }}{\mathrm{\Gamma }\to \mathrm{\Delta },B,A,\mathrm{\Lambda }}$,
• сечение: $\frac{\mathrm{\Gamma }\to \mathrm{\Delta },AA,\mathrm{\Theta }\to \mathrm{\Lambda }}{\mathrm{\Gamma },\mathrm{\Theta }\to \mathrm{\Delta },\mathrm{\Lambda }}$.

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

• $\mathrm{\neg }$-слева: $\frac{\mathrm{\Gamma }\to \mathrm{\Delta },A}{\mathrm{\neg }A,\mathrm{\Gamma }\to \mathrm{\Delta }}$; $\mathrm{\neg }$-справа: $\frac{A,\mathrm{\Gamma }\to \mathrm{\Delta }}{\mathrm{\Gamma }\to \mathrm{\Delta },\mathrm{\neg }A}$;
• $\wedge$-слева: $\frac{A,\mathrm{\Gamma }\to \mathrm{\Delta }}{A\wedge B,\mathrm{\Gamma }\to \mathrm{\Delta }}$ и $\frac{B,\mathrm{\Gamma }\to \mathrm{\Delta }}{A\wedge B,\mathrm{\Gamma }\to \mathrm{\Delta }}$; $\wedge$-справа: $\frac{\mathrm{\Gamma }\to \mathrm{\Delta },A\mathrm{\Gamma }\to \mathrm{\Delta },B}{\mathrm{\Gamma }\to \mathrm{\Delta },A\wedge B}$,
• $\vee$-слева: $\frac{A,\mathrm{\Gamma }\to \mathrm{\Delta }B,\mathrm{\Gamma }\to \mathrm{\Delta }}{A\vee B,\mathrm{\Gamma }\to \mathrm{\Delta }}$; $\vee$-справа: $\frac{\mathrm{\Gamma }\to \mathrm{\Delta },A}{\mathrm{\Gamma }\to \mathrm{\Delta },A\vee B}$ и $\frac{\mathrm{\Gamma }\to \mathrm{\Delta },B}{\mathrm{\Gamma }\to \mathrm{\Delta },A\vee B}$,
• $\Rightarrow$-слева: $\frac{\mathrm{\Gamma }\to \mathrm{\Delta },AB,\mathrm{\Theta }\to \mathrm{\Lambda }}{A\Rightarrow B,\mathrm{\Gamma },\mathrm{\Theta }\to \mathrm{\Delta },\mathrm{\Lambda }}$ и $\Rightarrow$-справа: $\frac{A,\mathrm{\Gamma }\to \mathrm{\Delta },B}{\mathrm{\Gamma }\to \mathrm{\Delta },A\Rightarrow B}$.

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

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

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

Пример $𝐋𝐊$-вывода закона исключённого третьего:

$\frac{\frac{\frac{\frac{\frac{A\to A}{\to A,\mathrm{\neg }A}}{\to A,A\vee \mathrm{\neg }A}}{\to A\vee \mathrm{\neg }A,A}}{\to A\vee \mathrm{\neg }A,A\vee \mathrm{\neg }A}}{\to A\vee \mathrm{\neg }A}$

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

Исчисление $𝐋𝐊$ эквивалентно классическому исчислению предикатов первой ступени: формула $A$ общезначима в исчислении предикатов тогда и только тогда, когда в $𝐋𝐊$ выводима секвенция $\to A$. Ключевой результат, который назван Генценом «основной теоремой» (Шаблон:Lang-de) — возможность провести любой $𝐋𝐊$-вывод без применения правила сечения, именно благодаря этому свойству устанавливаются все основные свойства $𝐋𝐊$, в том числе корректность, непротиворечивость и полнота.

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

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

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

Создано большое количество эквивалентных и удобных для тех или иных целей вариантов исчисления секвенций для классической и интуиционистской логик. Часть таких исчислений наследует построение Генцена, применённое при доказательстве непротиворечивости арифметики Пеано, и включает элементы систем натурального вывода, среди таковых — система Шаблон:Нп2 1957 года (почерпнутая из замечаний Шаблон:Iw и Шаблон:Iw к французскому переводу статьи Генцена), и её усовершенствованная версия, опубликованная в 1965 году Шаблон:Нп2, устраняющие практические неудобства использования изначальной нутрально-секвенциальной ГенценаШаблон:Sfn. Более радикальные усовершенствования для практического удобства вывода натурального типа в секвенциальных исчислениях были предложены Шаблон:Нп2: в его системе для классической логики применены две аксиомы ($A\to A$ и $\to A=A$, а в правилах вывода пропозициональные связки используются не только в сукцедентах, но и в антецедентах, притом как в нижних, так и в верхних секвенцияхШаблон:Sfn. Шаблон:Дополнить раздел

Симметрия

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

Литература

• Шаблон:БСЭ3
• Шаблон:Книга:Математическая энциклопедия
• Шаблон:Источник/НФЭ
• Шаблон:Статья
• Шаблон:Книга
• Шаблон:Книга
• Шаблон:Книга
• Шаблон:Статья
• Шаблон:Cite web