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

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

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

История

Понятие секвенции для систематического использования в доказательствах в форме дерева вывода ввёл в 1929 году немецкий физик и логик ( нем. ; 1881–1940) , но целостного исчисления для какой-либо логической теории в его трудах построено не было . В работе 1932 года Генцен попытался развить подход Герца , но в 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 году ( фин. ; 1913—2000) исчисления для классической логики, все правила вывода в котором обратимы; тогда же Кетонен предложил декомпозиционный подход к поиску доказательств, использующий свойство обратимости . Опубликованное в 1949 году в диссертации Романа Сушко безаксиомное исчисление было близко по форме к построениям Герца, явившись первым воплощением для секвенциальных систем герцевского типа .

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

Начиная с 1950-х годов основное внимание уделено переносу результатов о непротиворечивости и полноте на исчисления предикатов высших порядков, теории типов , неклассические логики . В 1953 году ( яп. ; 1926—2017) построил исчисление секвенций для простой теории типов, выражающей исчисления предикатов высших порядков, и предположил, что для него имеет место устранимость сечений ( гипотеза Такеути ). В 1966 году ( англ. ) доказал устранимость сечений для логики второго порядка , вскоре гипотеза была полностью доказана в работах и ( швед. ; род. 1936). В 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 правило вывода, которые делятся на структурные и логические .

Структурные правила ( ${\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} }$ .

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

Создано большое количество эквивалентных и удобных для тех или иных целей вариантов исчисления секвенций для классической и интуиционистской логик. Часть таких исчислений наследует построение Генцена, применённое при доказательстве непротиворечивости арифметики Пеано, и включает элементы систем натурального вывода, среди таковых — система ( англ. ; 1922–2014) 1957 года (почерпнутая из замечаний и к французскому переводу статьи Генцена), и её усовершенствованная версия, опубликованная в 1965 году ( англ. ; 1930–1966) , устраняющие практические неудобства использования изначальной нутрально-секвенциальной Генцена . Более радикальные усовершенствования для практического удобства вывода натурального типа в секвенциальных исчислениях были предложены ( нем. ; 1912–2003) : в его системе для классической логики применены две аксиомы ( ${\displaystyle A\rightarrow A}$ и ${\displaystyle \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 // . — 2014. — Декабрь ( т. 102 , № 6 ). — С. 1295–1322 . — doi : .
• Jan von Plato. (неопр.) . Stanford Encyclopaedia of Philosophy (16 апреля 2008).