Исчисление секвенций
Исчисление секвенций — вариант
В секвенциальном подходе вместо широких наборов аксиом используются развитые системы правил вывода, а доказательство ведётся в форме дерева вывода; по этому признаку (наряду с системами натурального вывода) исчисления секвенций относятся к генценовскому типу, в противоположность аксиоматическим гильбертовским исчислениям[англ.], в которых при развитом наборе аксиом количество правил вывода сведено к минимуму.
Основное свойство секвенциальной формы — симметричное устройствоустранимости сечений, и, как следствие, исчисления секвенций являются основными исследуемыми системами в теории доказательств.
, обеспечивающее удобство доказательстваИстория
Понятие секвенции для систематического использования в доказательствах в форме дерева вывода ввёл в 1929 году немецкий физик и логик Пауль Герц (нем. Paul Hertz; 1881–1940)[1], но целостного исчисления для какой-либо логической теории в его трудах построено не было[2]. В работе 1932 года Генцен попытался развить подход Герца[3], но в 1934 году отказался от наработок Герца: ввёл системы натурального вывода и для классического и интуиционистского исчислений предикатов соответственно, использующие обычные тавтологии и деревья вывода, и, как их структурное развитие, — секвенциальные системы и . Для и Генценом доказана устранимость сечения, что дало значительный методологический импульс намеченной Гильбертом теории доказательств: в той же работе Генцен впервые доказал
Следующим значительным шагом в развитии секвенциальных исчислений стала разработка в 1944 году Ойвой Кетоненом (фин. Oiva Ketonen; 1913—2000) исчисления для классической логики, все правила вывода в котором обратимы; тогда же Кетонен предложил декомпозиционный подход к поиску доказательств, использующий свойство обратимости[4][5]. Опубликованное в 1949 году в диссертации Романа Сушко безаксиомное исчисление было близко по форме к построениям Герца, явившись первым воплощением для секвенциальных систем герцевского типа[6][7].
В
Начиная с 1950-х годов основное внимание уделено переносу результатов о непротиворечивости и полноте на исчисления предикатов высших порядков, теории типов, неклассические логики. В 1953 году Гаиси Такеути (яп. 竹内外史; 1926—2017) построил исчисление секвенций для простой теории типов, выражающей исчисления предикатов высших порядков, и предположил, что для него имеет место устранимость сечений (гипотеза Такеути). В 1966 году Уильям Тэйт (англ. род. 1929) доказал устранимость сечений для логики второго порядка, вскоре гипотеза была полностью доказана в работах Мотоо Такахаси[10] и Дага Правица (швед. Dag Prawitz; род. 1936). В 1970-е годы результаты значительно расширены: Драгалиным найдены доказательства устранимости сечений для серии неклассических логик высших порядков, а Жирар[фр.] — для системы F.
Начиная с 1980-х годов секвенциальные системы играют ключевую роль в развитии систем
Основные понятия
Секвенцией называется выражение вида , где и — конечные (возможно пустые) последовательности логических формул, называемые цедентами: — антецедентом, а —
Если антецедент пуст (), то подразумевается выполнение дизъюнкции формул сукцедента ; пустой сукцедент () интерпретируется как противоречивость конъюнкции формул антецедента. Пустая секвенция означает, что в рассматриваемой системе имеется противоречие. Порядок формул в цедентах значимым не является, однако количество вхождений экземпляра формулы в цедент имеет значение. Запись в цедентах в виде или , где — последовательность формул, а — формула, означает добавление формулы в цедент (возможно, в ещё одном экземпляре).
Аксиомами считаются исходные секвенции, принимаемые без доказательств; в секвенциальном подходе число аксиом минимизируется, так, в генценовских исчислениях и задаётся только одна схема аксиом — .
- и ,
интерпретируются они как утверждение о выводимости из верхней секвенции (верхних секвенций и ) нижней секвенции . Доказательство в секвенциальных исчислениях (как и в системах натурального вывода) записывается в древовидной форме сверху вниз, например:
- ,
где каждая черта означает непосредственный вывод — переход от верхних секвенций к нижней согласно какому-либо из принятых в данной системе правил вывода. Таким образом, существование дерева вывода, начинающегося от аксиом (начальных секвенций), и приводящих к секвенции , означает её выводимость в данной логической системе: .
Классическое генценовское исчисление секвенций
Наиболее часто применяемым исчислением секвенций для классического исчисления предикатов является система , построенная Генценом в 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.
- .
- ↑ 1 2 Ян фон Плато, 2008.
- ↑ Bernays P. Review: Oiva Ketonen, Untersuchungen zum Pradikatenkalkul (англ.) // Journal of Symbolic Logic. — 1945. — Vol. 10, no. 4. — P. 127—130. Архивировано 21 января 2019 года.
- ↑ Suszko R. Formalna teoria wartości logicznych (пол.) // Studia Logica. — 1957. — T. 6. — S. 145–320.
- ↑ Инджейчак, 2014, 1310—1315, p. 1310.
- ↑ Клини, 1958, с. 389—406.
- ↑ Клини, 1958, с. 424—434.
- 21 января 2019 года.
- ↑ Такеути, 1978.
- ↑ Suppes P. Introduction to Logic. — Princeton: Van Nostrand, 1957.
- ↑ Lemmon E. J. Beginning Logic. — London: Nelson, 1965.
- ↑ Инджейчак, 2014, p. 1300.
- ↑ 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).
- Драгалин А. Г. Секвенций исчисление // Математическая энциклопедия : [в 5 т.] / Гл. ред. И. М. Виноградов. — М.: Советская энциклопедия, 1984. — Т. 4: Ок — Сло. — С. 1104. — 1216 стб. : ил. — 150 000 экз.
- Быстров П. И. Исчисление секвенций // Мысль, 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 // .
- Jan von Plato. The Development of Proof Theory . Stanford Encyclopaedia of Philosophy(16 апреля 2008).