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

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

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

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

ИсторияПравить

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

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

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

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

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

Основные понятияПравить

Секвенцией называется выражение вида $\mathrm{\Gamma <!--\; \Gamma \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->}$$\Gamma \rightarrow \Delta$ , где $\mathrm{\Gamma <!--\; \Gamma \; -->}$$\Gamma$  и $\mathrm{\Delta <!--\; \Delta \; -->}$$\Delta$  — конечные (возможно пустые) последовательности логических формул, называемые цедентами: $\mathrm{\Gamma <!--\; \Gamma \; -->}$$\Gamma$  — антецедентом, а $\mathrm{\Delta <!--\; \Delta \; -->}$$\Delta$  — сукцедентом (иногда — консеквентом). Интуитивный смысл, закладываемый в секвенцию $A_1,\dots <!--\; \dots \; -->,A_n\to <!--\; \to \; -->B_1,\dots <!--\; \dots \; -->,B_m$$A_{1},\ldots ,A_{n}\rightarrow B_{1},\ldots ,B_{m}$  — если выполнена конъюнкция формул антецедента $A_1\wedge <!--\; \wedge \; -->\dots <!--\; \dots \; -->\wedge <!--\; \wedge \; -->A_n$$A_{1}\land \ldots \land A_{n}$ , то имеет место (выводится) дизъюнкция формул сукцедента $B_1\vee <!--\; \vee \; -->\dots <!--\; \dots \; -->\vee <!--\; \vee \; -->B_m$$B_{1}\lor \ldots \lor B_{m}$ . Иногда вместо стрелки в обозначении секвенции используется знак выводимости ($\mathrm{\Gamma <!--\; \Gamma \; -->}⊢<!--\; ⊢\; -->\mathrm{\Delta <!--\; \Delta \; -->}$$\Gamma \vdash \Delta$ ) или знак импликации ($\mathrm{\Gamma <!--\; \Gamma \; -->}\Rightarrow <!--\; \Rightarrow \; -->\mathrm{\Delta <!--\; \Delta \; -->}$$\Gamma \Rightarrow \Delta$ ).

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

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

$\frac{S_1}{T}$${\cfrac {\;S_{1}\;}{T}}$  и $\frac{S_1{S}_2}{T}$${\cfrac {\;S_{1}\;\;\;S_{2}\;}{\;\;T}}$ ,

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

$\frac{\frac{S_1{S}_2}{T_1}\frac{S_3}{T_2}}{U}$${\cfrac {{\cfrac {\;S_{1}\;\;\;S_{2}\;}{\;T_{1}}}\;\;\;\;{\cfrac {\;S_{3}\;}{T_{2}}}}{U}}$ ,

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

Классическое генценовское исчисление секвенцийПравить

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

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

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

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

• $\mathrm{\neg <!--\; \neg \; -->}$$\lnot$ -слева: $\frac{\mathrm{\Gamma <!--\; \Gamma \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->},A}{\mathrm{\neg <!--\; \neg \; -->}A,\mathrm{\Gamma <!--\; \Gamma \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->}}$${\cfrac {\qquad \Gamma \ \rightarrow \ \Delta ,\ A}{\ \lnot A,\ \Gamma \ \rightarrow \ \Delta \qquad }}$ ; $\mathrm{\neg <!--\; \neg \; -->}$$\lnot$ -справа: $\frac{A,\mathrm{\Gamma <!--\; \Gamma \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->}}{\mathrm{\Gamma <!--\; \Gamma \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->},\mathrm{\neg <!--\; \neg \; -->}A}$${\cfrac {A,\ \Gamma \ \rightarrow \ \Delta \qquad }{\qquad \Gamma \ \rightarrow \ \Delta ,\ \lnot A\ }}$ ;
• $\wedge <!--\; \wedge \; -->$$\land$ -слева: $\frac{A,\mathrm{\Gamma <!--\; \Gamma \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->}}{A\wedge <!--\; \wedge \; -->B,\mathrm{\Gamma <!--\; \Gamma \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->}}$${\cfrac {\qquad A,\ \Gamma \ \rightarrow \ \Delta }{\ A\land B,\ \Gamma \ \rightarrow \ \Delta \ }}$  и $\frac{B,\mathrm{\Gamma <!--\; \Gamma \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->}}{A\wedge <!--\; \wedge \; -->B,\mathrm{\Gamma <!--\; \Gamma \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->}}$${\cfrac {\qquad B,\ \Gamma \ \rightarrow \ \Delta }{\ A\land B,\ \Gamma \ \rightarrow \ \Delta \ }}$ ; $\wedge <!--\; \wedge \; -->$$\land$ -справа: $\frac{\mathrm{\Gamma <!--\; \Gamma \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->},A\mathrm{\Gamma <!--\; \Gamma \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->},B}{\mathrm{\Gamma <!--\; \Gamma \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->},A\wedge <!--\; \wedge \; -->B}$${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A\qquad \Gamma \ \rightarrow \ \Delta ,\ B}{\ \qquad \ \Gamma \ \rightarrow \ \Delta ,\ A\land B\ }}$ ,
• $\vee <!--\; \vee \; -->$$\lor$ -слева: $\frac{A,\mathrm{\Gamma <!--\; \Gamma \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->}B,\mathrm{\Gamma <!--\; \Gamma \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->}}{A\vee <!--\; \vee \; -->B,\mathrm{\Gamma <!--\; \Gamma \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->}}$$\ {\cfrac {A,\ \Gamma \ \rightarrow \ \Delta \qquad B,\ \Gamma \ \rightarrow \ \Delta \ }{\ A\lor B,\ \Gamma \ \rightarrow \ \Delta \ \qquad }}$ ; $\vee <!--\; \vee \; -->$$\lor$ -справа: $\frac{\mathrm{\Gamma <!--\; \Gamma \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->},A}{\mathrm{\Gamma <!--\; \Gamma \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->},A\vee <!--\; \vee \; -->B}$${\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A\qquad }{\ \Gamma \ \rightarrow \ \Delta ,\ A\lor B\ }}$  и $\frac{\mathrm{\Gamma <!--\; \Gamma \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->},B}{\mathrm{\Gamma <!--\; \Gamma \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->},A\vee <!--\; \vee \; -->B}$${\cfrac {\Gamma \rightarrow \Delta ,\ B\qquad }{\ \Gamma \rightarrow \Delta ,\ A\lor B\ }}$ ,
• $\Rightarrow <!--\; \Rightarrow \; -->$$\Rightarrow$ -слева: $\frac{\mathrm{\Gamma <!--\; \Gamma \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->},AB,\mathrm{\Theta <!--\; \Theta \; -->}\to <!--\; \to \; -->\mathrm{\Lambda <!--\; \Lambda \; -->}}{A\Rightarrow <!--\; \Rightarrow \; -->B,\mathrm{\Gamma <!--\; \Gamma \; -->},\mathrm{\Theta <!--\; \Theta \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->},\mathrm{\Lambda <!--\; \Lambda \; -->}}$$\ {\cfrac {\Gamma \ \rightarrow \ \Delta ,\ A\qquad \qquad B,\ \Theta \ \rightarrow \ \Lambda \ }{A\Rightarrow B,\ \Gamma ,\ \Theta \ \rightarrow \ \Delta ,\Lambda \qquad }}$  и $\Rightarrow <!--\; \Rightarrow \; -->$$\Rightarrow$ -справа: $\frac{A,\mathrm{\Gamma <!--\; \Gamma \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->},B}{\mathrm{\Gamma <!--\; \Gamma \; -->}\to <!--\; \to \; -->\mathrm{\Delta <!--\; \Delta \; -->},A\Rightarrow <!--\; \Rightarrow \; -->B}$${\cfrac {A,\ \Gamma \ \rightarrow \ \Delta ,\ B\qquad }{\qquad \Gamma \ \rightarrow \ \Delta ,\ A\Rightarrow B\ }}$ .

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

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

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

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

$\frac{\frac{\frac{\frac{\frac{A\to <!--\; \to \; -->A}{\to <!--\; \to \; -->A,\mathrm{\neg <!--\; \neg \; -->}A}}{\to <!--\; \to \; -->A,A\vee <!--\; \vee \; -->\mathrm{\neg <!--\; \neg \; -->}A}}{\to <!--\; \to \; -->A\vee <!--\; \vee \; -->\mathrm{\neg <!--\; \neg \; -->}A,A}}{\to <!--\; \to \; -->A\vee <!--\; \vee \; -->\mathrm{\neg <!--\; \neg \; -->}A,A\vee <!--\; \vee \; -->\mathrm{\neg <!--\; \neg \; -->}A}}{\to <!--\; \to \; -->A\vee <!--\; \vee \; -->\mathrm{\neg <!--\; \neg \; -->}A}$${\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}}$ 

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

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

Интуиционистское генценовское исчисление секвенцийПравить

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

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

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