Исчисление секвенций — вариант логических исчислений, использующий для доказательства утверждений не произвольные цепочки тавтологий, а последовательности условных суждений — секвенций[⇨]. Наиболее известные исчисления секвенций — [⇨] и [⇨] для классического и интуиционистского исчислений предикатов — построены Генценом в 1934 году, позднее сформулированы секвенциальные варианты для широкого класса прикладных исчислений (арифметики, анализа), теорий типов, неклассических логик.
В секвенциальном подходе вместо широких наборов аксиом используются развитые системы правил вывода, а доказательство ведётся в форме дерева вывода; по этому признаку (наряду с системами натурального вывода) исчисления секвенций относятся к генценовскому типу, в противоположность аксиоматическим гильбертовским исчислениям[англ.], в которых при развитом наборе аксиом количество правил вывода сведено к минимуму.
Основное свойство секвенциальной формы — симметричное устройство[⇨], обеспечивающее удобство доказательства устранимости сечений, и, как следствие, исчисления секвенций являются основными исследуемыми системами в теории доказательств.
Понятие секвенции для систематического использования в доказательствах в форме дерева вывода ввёл в 1929 году немецкий физик и логик Пауль Герц (нем.Paul Hertz; 1881–1940)[1], но целостного исчисления для какой-либо логической теории в его трудах построено не было[2]. В работе 1932 года Генцен попытался развить подход Герца[3], но в 1934 году отказался от наработок Герца: ввёл системы натурального вывода и для классического и интуиционистского исчислений предикатов соответственно, использующие обычные тавтологии и деревья вывода, и, как их структурное развитие, — секвенциальные системы и . Для и Генценом доказана устранимость сечения, что дало значительный методологический импульс намеченной Гильбертом теории доказательств: в той же работе Генцен впервые доказал полноту интуиционистского исчисления предикатов, а в 1936 году — доказал непротиворечивостьаксиоматики Пеано для целых чисел, расширив её с помощью секвенциального варианта трансфинитной индукцией до ординала. Последний результат имел также и особую идеологическую значимость в свете пессимизма начала 1930-х годов в связи с теоремой Гёделя о неполноте, согласно которой непротиворечивость арифметики невозможно установить её собственными средствами: нашлось достаточно естественное расширение арифметики логикой, устраняющее это ограничение.
Следующим значительным шагом в развитии секвенциальных исчислений стала разработка в 1944 годуОйвой Кетоненом (фин.Oiva Ketonen; 1913—2000) исчисления для классической логики, все правила вывода в котором обратимы; тогда же Кетонен предложил декомпозиционный подход к поиску доказательств, использующий свойство обратимости[4][5]. Опубликованное в 1949 году в диссертации Романа Сушко безаксиомное исчисление было близко по форме к построениям Герца, явившись первым воплощением для секвенциальных систем герцевского типа[6][7].
В 1952 годуСтивен Клини во «Введении в метаматематику» на основе исчисления Кетонена построил интуиционистское исчисление секвенций с обратимыми правилами вывода[8], там же ввёл исчисления генценовского типа и , в которых не требовались структурные[⇨] правила вывода[9], и, в целом, после публикации книги исчисления секвенций получили известность в широком кругу специалистов[4].
Секвенцией называется выражение вида , где и — конечные (возможно пустые) последовательности логических формул, называемые цедентами: — антецедентом, а — сукцедентом (иногда — консеквентом). Интуитивный смысл, закладываемый в секвенцию — если выполнена конъюнкция формул антецедента , то имеет место (выводится) дизъюнкция формул сукцедента . Иногда вместо стрелки в обозначении секвенции используется знак выводимости () или знак импликации ().
Если антецедент пуст (), то подразумевается выполнение дизъюнкции формул сукцедента ; пустой сукцедент () интерпретируется как противоречивость конъюнкции формул антецедента. Пустая секвенция означает, что в рассматриваемой системе имеется противоречие. Порядок формул в цедентах значимым не является, однако количество вхождений экземпляра формулы в цедент имеет значение. Запись в цедентах в виде или , где — последовательность формул, а — формула, означает добавление формулы в цедент (возможно, в ещё одном экземпляре).
Аксиомами считаются исходные секвенции, принимаемые без доказательств; в секвенциальном подходе число аксиом минимизируется, так, в генценовских исчислениях и задаётся только одна схема аксиом — . Правила вывода в секвенциальной форме записываются как следующие выражения:
и ,
интерпретируются они как утверждение о выводимости из верхней секвенции (верхних секвенций и ) нижней секвенции . Доказательство в секвенциальных исчислениях (как и в системах натурального вывода) записывается в древовидной форме сверху вниз, например:
,
где каждая черта означает непосредственный вывод — переход от верхних секвенций к нижней согласно какому-либо из принятых в данной системе правил вывода. Таким образом, существование дерева вывода, начинающегося от аксиом (начальных секвенций), и приводящих к секвенции , означает её выводимость в данной логической системе: .
Классическое генценовское исчисление секвенций
Наиболее часто применяемым исчислением секвенций для классического исчисления предикатов является система , построенная Генценом в 1934 году. В системе одна схема аксиом — и 21 правило вывода, которые делятся на структурные и логические[11].
Логические пропозициональные правила предназначены для добавления в вывод пропозициональных связок:
-слева: ; -справа: ;
-слева: и ; -справа: ,
-слева: ; -справа: и ,
-слева: и -справа: .
Логические кванторные правила вводят кванторы всеобщности и существования в вывод ( — формула со свободной переменной , — произвольный терм, а — замена всех вхождений свободной переменной на терм ):
-слева: и -справа: ;
-слева: и -справа: .
Дополнительное условие в кванторных правилах — невхождение свободной переменной в нижние формулы секвенций в правилах -справа и -слева.
— в нём вывод начат с единственной аксиомы, далее — последовательно применены правила -справа, -справа, перестановка справа, -справа и сокращение справа.
Исчисление эквивалентно классическому исчислению предикатов первой ступени: формула общезначима в исчислении предикатов тогда и только тогда, когда в выводима секвенция . Ключевой результат, который назван Генценом «основной теоремой» (нем.Hauptsatz) — возможность провести любой -вывод без применения правила сечения, именно благодаря этому свойству устанавливаются все основные свойства , в том числе корректность, непротиворечивость и полнота.
Исчисление получается из добавлением ограничения на сукцеденты секвенций в правилах вывода: в них допустимо использование только одной формулы, а правила перестановки справа и сокращения справа (оперирующие с нескольким формулами в сукцедентах) исключаются. Таким образом, при минимальных модификациях получается система, в которой невыводимы законы двойного отрицания и исключённого третьего, но действуют все прочие основные логические законы, и, например, выводима эквивалентность . Полученная система эквивалентна интуиционистскому исчислению предикатов с аксиоматикой Гейтинга. В исчислении также устранимы сечения, оно также корректно, непротиворечиво и полно, притом последний результат для интуиционистского исчисления предикатов впервые получен именно для .
Нестандартные исчисления секвенций
Создано большое количество эквивалентных и удобных для тех или иных целей вариантов исчисления секвенций для классической и интуиционистской логик. Часть таких исчислений наследует построение Генцена, применённое при доказательстве непротиворечивости арифметики Пеано, и включает элементы систем натурального вывода, среди таковых — система Саппса (англ.Patrick Suppes; 1922–2014) 1957 года[12] (почерпнутая из замечаний Фейса[англ.] и Ладриера[фр.] к французскому переводу статьи Генцена), и её усовершенствованная версия, опубликованная в 1965 году Леммоном (англ.John Lemmon; 1930–1966)[13], устраняющие практические неудобства использования изначальной нутрально-секвенциальной Генцена[14]. Более радикальные усовершенствования для практического удобства вывода натурального типа в секвенциальных исчислениях были предложены Хермесом (нем.Hans Hermes; 1912–2003)[15]: в его системе для классической логики применены две аксиомы ( и , а в правилах вывода пропозициональные связки используются не только в сукцедентах, но и в антецедентах, притом как в нижних, так и в верхних секвенциях[16].
↑Инджейчак, 2014, Hertz did not present any specific system for concrete logic. His approach was abstract; he defined rather a schema of the system in which the only rules have purely structural character, p. 1310.
↑Gentzen G. Über die Existenz unabhängiger Axiomensysteme zu unendlichen Satzsystemen (нем.) // Mathematische Annalen. — 1932. — Bd. 107. — S. 329–350. — doi:10.1007/BF01448897.
↑Hermes H. Einführung in die Mathematische Logik. — Stuttgart: Teubner, 1963.
↑Инджейчак, 2014, <...> in order to obtain more flexible tool for actual proof search one can admit the possibility of making logical operations also in antecedents. <…> It seems that the first system of this sort was provided by Hermes. He also uses intuitionistic sequents with sequences of formulae in antecedents in his formalization of classical logic with identity. As primitive sequents Hermes uses only: and , p. 1300.
Литература
Секвенций исчисление // Сафлор — Соан. — М. : Советская энциклопедия, 1976. — С. 181—182; ст. 530—532. — (Большая советская энциклопедия : [в 30 т.] / гл. ред. А. М. Прохоров ; 1969—1978, т. 23).
Генцен Г. Исследования логических выводов = Untersuchungen über das logische Schließen // Mathematische Zeitschrift, Bd. 39 (1934–1935), S. 405–431 // Идельсон А. В., Минц Г. Е. Математическая теория логического вывода / перевод А. В. Идельсона. — М.: Наука, 1967. — С. 9—76.
Драгалин А. Г. Математический интуиционизм. Введение в теорию доказательств. — М.: Наука, 1979. — 256 с. — (Математическая логика и основания математики).