Открыть главное меню

Исчисление секвенций — вариант логических исчислений, использующий для доказательства утверждений не произвольные цепочки тавтологий, а последовательности условных суждений — секвенций[⇨]. Наиболее известные исчисления секвенций — [⇨] и [⇨] для классического и интуиционистского исчислений предикатов — построены Генценом в 1934 году, позднее сформулированы секвенциальные варианты для широкого класса прикладных исчислений (арифметики, анализа), теорий типов, неклассических логик.

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

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

Содержание

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

Понятие секвенции для систематического использования в доказательствах в форме дерева вывода ввёл в 1929 году немецкий физик и логик Пауль Герц (нем. Paul Hertz; 1881—1940)[1], но целостного исчисления для какой-либо логической теории в его трудах построено не было[2]. В работе 1932 года Генцен попытался развить подход Герца[3], но в 1934 году отказался от наработок Герца: ввёл системы натурального вывода   и   для классического и интуиционистского исчислений предикатов соответственно, использующие обычные тавтологии и деревья вывода, и, как их структурное развитие, — секвенциальные системы   и  . Для   и   Генценом доказана устранимость сечения, что дало значительный методологический импульс намеченной Гильбертом теории доказательств: в той же работе Генцен впервые доказал полноту интуиционистского исчисления предикатов, а в 1936 году — доказал непротиворечивость аксиоматики Пеано для целых чисел, расширив её с помощью секвенциального варианта   трансфинитной индукцией до ординала  . Последний результат имел также и особую идеологическую значимость в свете пессимизма начала 1930-х годов в связи с теоремой Гёделя о неполноте, согласно которой непротиворечивость арифметики невозможно установить её собственными средствами: нашлось достаточно естественное расширение арифметики логикой, устраняющее это ограничение.

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

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

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

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

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

Секвенцией называется выражение вида  , где   и   — конечные (возможно пустые) последовательности логических формул, называемые цедентами:   — антецедентом, а   — сукцедентом (иногда — консеквентом). Интуитивный смысл, закладываемый в секвенцию   — если выполнена конъюнкция формул антецедента  , то имеет место (выводится) дизъюнкция формул сукцедента  . Иногда вместо стрелки в обозначении секвенции используется знак выводимости ( ) или знак импликации ( ).

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

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

  и  ,

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

 ,

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

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

Наиболее часто применяемым исчислением секвенций для классического исчисления предикатов является система  , построенная Генценом в 1934 году. В системе одна схема аксиом —   и 21 правило вывода, которые делятся на структурные и логические[11].

Структурные правила ( ,   — формулы,  ,  ,  ,   — списки формул):

  • ослабление слева:   и справа:  ;
  • сокращение слева:   и справа:  ;
  • перестановка слева:   и справа:  ,
  • сечение:  .

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

  •  -слева:  ;  -справа:  ;
  •  -слева:   и  ;  -справа:  ,
  •  -слева:  ;  -справа:   и  ,
  •  -слева:   и  -справа:  .

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

  •  -слева:   и  -справа:  ;
  •  -слева:   и  -справа:  .

Дополнительное условие в кванторных правилах — невхождение свободной переменной   в нижние формулы секвенций в правилах  -справа и  -слева.

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

 

— в нём вывод начат с единственной аксиомы, далее — последовательно применены правила  -справа,  -справа, перестановка справа,  -справа и сокращение справа.

Исчисление   эквивалентно классическому исчислению предикатов первой ступени: формула   общезначима в исчислении предикатов тогда и только тогда, когда в   выводима секвенция  . Ключевой результат, который назван Генценом «основной теоремой» (нем. Hauptsatz) ­— возможность провести любой  -вывод без применения правила сечения, именно благодаря этому свойству устанавливаются все основные свойства  , в том числе корректность, непротиворечивость и полнота.

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

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

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

Создано большое количество эквивалентных и удобных для тех или иных целей вариантов исчисления секвенций для классической и интуиционисткой логик. Часть таких исчислений наследует построение Генцена, применённое при доказательстве непротиворечивости арифметики Пеано, и включает элементы систем натурального вывода, среди таковых — система Саппса (англ. Patrick Suppes; 1922—2014) 1957 года[12] (почерпнутая из замечаний Фейса[en] и Ладриера[fr] к французскому переводу статьи Генцена), и её усовершенствованная версия, опубликованная в 1965 году Леммоном (англ. John Lemmon; 1930—1966)[13], устраняющие практические неудобства использования изначальной нутрально-секвенциальной Генцена[14]. Более радикальные усовершенствования для практического удобства вывода натурального типа в секвенциальных исчислениях были предложены Хермесом (нем. Hans Hermes; 1912—2003)[15]: в его системе для классической логики применены две аксиомы (  и  , а в правилах вывода пропозициональные связки используются не только в сукцедентах, но и в антецедентах, притом как в нижних, так и в верхних секвенциях[16].

СимметрияПравить

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

ПримечанияПравить

  1. Hertz P. Über Axiomensysteme für beliebige Satzsysteme (нем.) // Mathematische Annalen. — 1929. — Bd. 101. — S. 457–514. — DOI:10.1007/BF01454856.
  2. Инджейчак, 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.
  3. Gentzen G. Über die Existenz unabhängiger Axiomensysteme zu unendlichen Satzsystemen (нем.) // Mathematische Annalen. — 1932. — Bd. 107. — S. 329–350. — DOI:10.1007/BF01448897.
  4. 1 2 Ян фон Плато, 2008.
  5. Bernays P. Review: Oiva Ketonen, Untersuchungen zum Pradikatenkalkul (англ.) // Journal of Symbolic Logic. — 1945. — Vol. 10, no. 4. — P. 127—130.
  6. Suszko R. Formalna teoria wartości logicznych (польск.) // Studia Logica. — 1957. — T. 6. — S. 145–320.
  7. Инджейчак, 2014, 1310—1315, p. 1310.
  8. Клини, 1958, с. 389—406.
  9. Клини, 1958, с. 424—434.
  10. Takahashi M. A proof of cut-elimination theorem in simple type-theory // Journal of Japanese Mathematical Society. — 1967. — Т. 19, № 4. — С. 399—410. — DOI:10.2969/jmsj/01940399.
  11. Такеути, 1978.
  12. Suppes P. Introduction to Logic. — Princeton: Van Nostrand, 1957.
  13. Lemmon E. J. Beginning Logic. — London: Nelson, 1965.
  14. Инджейчак, 2014, p. 1300.
  15. Hermes H. Einführung in die Mathematische Logik. — Stuttgart: Teubner, 1963.
  16. Инджейчак, 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.

ЛитератураПравить