Русская Википедия:Исчисление секвенций

Содержание

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

Текст

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

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

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

История

Понятие секвенции для систематического использования в доказательствах в форме дерева вывода ввёл в 1929 году немецкий физик и логик Шаблон:Нп2, но целостного исчисления для какой-либо логической теории в его трудах построено не былоШаблон:Sfn. В работе 1932 года Генцен попытался развить подход Герца, но в 1934 году отказался от наработок Герца: ввёл системы натурального вывода <math>\mathbf{NK}</math> и <math>\mathbf{NJ}</math> для классического и интуиционистского исчислений предикатов соответственно, использующие обычные тавтологии и деревья вывода, и, как их структурное развитие, — секвенциальные системы <math>\mathbf{LK}</math> и <math>\mathbf{LJ}</math>. Для <math>\mathbf{LK}</math> и <math>\mathbf{LJ}</math> Генценом доказана устранимость сечения, что дало значительный методологический импульс намеченной Гильбертом теории доказательств: в той же работе Генцен впервые доказал полноту интуиционистского исчисления предикатов, а в 1936 году — доказал непротиворечивость аксиоматики Пеано для целых чисел, расширив её с помощью секвенциального варианта <math>\mathbf{NK}</math> трансфинитной индукцией до ординала <math>\epsilon_0</math>. Последний результат имел также и особую идеологическую значимость в свете пессимизма начала 1930-х годов в связи с теоремой Гёделя о неполноте, согласно которой непротиворечивость арифметики невозможно установить её собственными средствами: нашлось достаточно естественное расширение арифметики логикой, устраняющее это ограничение.

Следующим значительным шагом в развитии секвенциальных исчислений стала разработка в 1944 году Шаблон:Нп2 исчисления для классической логики, все правила вывода в котором обратимы; тогда же Кетонен предложил декомпозиционный подход к поиску доказательств, использующий свойство обратимостиШаблон:Sfn. Опубликованное в 1949 году в диссертации Романа Сушко безаксиомное исчисление было близко по форме к построениям Герца, явившись первым воплощением для секвенциальных систем герцевского типаШаблон:Sfn.

В 1952 году Стивен Клини во «Введении в метаматематику» на основе исчисления Кетонена построил интуиционистское исчисление секвенций с обратимыми правилами выводаШаблон:Sfn, там же ввёл исчисления генценовского типа <math>G3i</math> и <math>G3c</math>, в которых не требовались структурныеШаблон:Переход правила выводаШаблон:Sfn, и, в целом, после публикации книги исчисления секвенций получили известность в широком кругу специалистовШаблон:Sfn.

Начиная с 1950-х годов основное внимание уделено переносу результатов о непротиворечивости и полноте на исчисления предикатов высших порядков, теории типов, неклассические логики. В 1953 году Шаблон:Нп2 построил исчисление секвенций для простой теории типов, выражающей исчисления предикатов высших порядков, и предположил, что для него имеет место устранимость сечений (гипотеза Такеути). В 1966 году Шаблон:Нп2 доказал устранимость сечений для логики второго порядка, вскоре гипотеза была полностью доказана в работах Мотоо Такахаси и Шаблон:Нп2. В 1970-е годы результаты значительно расширены: Драгалиным найдены доказательства устранимости сечений для серии неклассических логик высших порядков, а Шаблон:Iw — для системы F.

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

Основные понятия

Секвенцией называется выражение вида <math>\Gamma \rightarrow \Delta</math>, где <math>\Gamma</math> и <math>\Delta</math> — конечные (возможно пустые) последовательности логических формул, называемые цедентами: <math>\Gamma</math> — антецедентом, а <math>\Delta</math> — сукцедентом (иногда — консеквентом). Интуитивный смысл, закладываемый в секвенцию <math>A_1, \ldots, A_n \rightarrow B_1, \ldots, B_m</math> — если выполнена конъюнкция формул антецедента <math>A_1 \land \ldots \land A_n</math>, то имеет место (выводится) дизъюнкция формул сукцедента <math>B_1 \lor \ldots \lor B_m</math>. Иногда вместо стрелки в обозначении секвенции используется знак выводимости (<math>\Gamma \vdash \Delta</math>) или знак импликации (<math>\Gamma \Rightarrow \Delta</math>).

Если антецедент пуст (<math>\rightarrow B_1, \ldots, B_m</math>), то подразумевается выполнение дизъюнкции формул сукцедента <math>B_1 \lor \ldots \lor B_m</math>; пустой сукцедент (<math>A_1, \ldots, A_n \rightarrow</math>) интерпретируется как противоречивость конъюнкции формул антецедента. Пустая секвенция <math>\rightarrow</math> означает, что в рассматриваемой системе имеется противоречие. Порядок формул в цедентах значимым не является, однако количество вхождений экземпляра формулы в цедент имеет значение. Запись в цедентах в виде <math>A, \Gamma</math> или <math>\Gamma, A</math>, где <math>\Gamma</math> — последовательность формул, а <math>A</math> — формула, означает добавление формулы <math>A</math> в цедент (возможно, в ещё одном экземпляре).

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

<math>\cfrac{\;S_1\;}{T}</math> и <math>\cfrac{\;S_1 \;\;\; S_2\;}{\;\;T}</math>,

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

<math>\cfrac{\cfrac{\;S_1 \;\;\; S_2\;}{\;T_1} \;\;\;\; \cfrac{\;S_3\;}{T_2}}{U}</math>,

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

Классическое генценовское исчисление секвенций

Наиболее часто применяемым исчислением секвенций для классического исчисления предикатов является система <math>\mathbf{LK}</math>, построенная Генценом в 1934 году. В системе одна схема аксиом — <math>A \rightarrow A</math> и 21 правило вывода, которые делятся на структурные и логическиеШаблон:Sfn.

Структурные правила (<math>A</math>, <math>B</math> — формулы, <math>\Gamma</math>, <math>\Delta</math>, <math>\Theta</math>, <math>\Lambda</math> — списки формул):

• ослабление слева: <math>\cfrac {\qquad \Gamma \ \rightarrow \ \Delta \ }{\ A, \ \Gamma \ \rightarrow \ \Delta}</math> и справа: <math>\cfrac {\Gamma \ \rightarrow \ \Delta \quad}{\ \Gamma \ \rightarrow \ \Delta, \ A}</math>;
• сокращение слева: <math>\cfrac {\,\, A, \ A, \ \Gamma \ \rightarrow \ \Delta}{\qquad A, \ \Gamma \ \rightarrow \ \Delta \ }</math> и справа: <math>\cfrac {\Gamma \ \rightarrow \ \Delta, \ A, \ A}{\,\,\, \Gamma \ \rightarrow \ \Delta, \ A \qquad}</math>;
• перестановка слева: <math>\cfrac {\ \Gamma, \ A, \ B, \ \Theta \ \rightarrow \ \Delta \ }{\ \Gamma, \ B, \ A, \ \Theta \ \rightarrow \ \Delta}</math> и справа: <math>\cfrac {\ \Gamma \ \rightarrow \ \Delta, \ A, \ B, \ \Lambda \ }{\ \Gamma \ \rightarrow \ \Delta, \ B, \ A, \ \Lambda \ }</math>,
• сечение: <math>\cfrac {\ \Gamma \ \rightarrow \ \Delta, \ A \qquad A, \ \Theta \ \rightarrow \ \Lambda \ }{\Gamma, \ \Theta \ \rightarrow \ \Delta, \ \Lambda }</math>.

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

• <math>\lnot</math>-слева: <math>\cfrac {\qquad \Gamma \ \rightarrow \ \Delta, \ A}{\ \lnot A, \ \Gamma \ \rightarrow \ \Delta \qquad}</math>; <math>\lnot</math>-справа: <math>\cfrac {A, \ \Gamma \ \rightarrow \ \Delta \qquad}{\qquad \Gamma \ \rightarrow \ \Delta, \ \lnot A \ }</math>;
• <math>\land</math>-слева: <math>\cfrac {\qquad A, \ \Gamma \ \rightarrow \ \Delta }{\ A \land B, \ \Gamma \ \rightarrow \ \Delta \ }</math> и <math>\cfrac {\qquad B, \ \Gamma \ \rightarrow \ \Delta}{\ A \land B, \ \Gamma \ \rightarrow \ \Delta \ }</math>; <math>\land</math>-справа: <math>\cfrac {\Gamma \ \rightarrow \ \Delta, \ A \qquad \Gamma \ \rightarrow \ \Delta, \ B}{\ \qquad \ \Gamma \ \rightarrow \ \Delta, \ A\land B \ } </math>,
• <math>\lor</math>-слева: <math>\ \cfrac {A, \ \Gamma \ \rightarrow \ \Delta \qquad B, \ \Gamma \ \rightarrow \ \Delta \ }{\ A \lor B, \ \Gamma \ \rightarrow \ \Delta \ \qquad}</math>; <math>\lor</math>-справа: <math>\cfrac {\Gamma \ \rightarrow \ \Delta, \ A \qquad}{\ \Gamma \ \rightarrow \ \Delta, \ A \lor B \ }</math> и <math>\cfrac {\Gamma \rightarrow \Delta, \ B \qquad}{\ \Gamma \rightarrow \Delta, \ A \lor B \ }</math>,
• <math>\Rightarrow</math>-слева: <math>\ \cfrac {\Gamma \ \rightarrow \ \Delta, \ A \qquad \qquad B, \ \Theta \ \rightarrow \ \Lambda \ }{A \Rightarrow B, \ \Gamma, \ \Theta \ \rightarrow \ \Delta, \Lambda\qquad}</math> и <math>\Rightarrow</math>-справа: <math>\cfrac {A, \ \Gamma \ \rightarrow \ \Delta, \ B \qquad }{\qquad \Gamma \ \rightarrow \ \Delta, \ A \Rightarrow B \ }</math>.

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

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

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

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

<math>\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}</math> — в нём вывод начат с единственной аксиомы, далее — последовательно применены правила <math>\lnot</math>-справа, <math>\lor</math>-справа, перестановка справа, <math>\lor</math>-справа и сокращение справа.

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

Интуиционистское генценовское исчисление секвенций

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

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

Создано большое количество эквивалентных и удобных для тех или иных целей вариантов исчисления секвенций для классической и интуиционистской логик. Часть таких исчислений наследует построение Генцена, применённое при доказательстве непротиворечивости арифметики Пеано, и включает элементы систем натурального вывода, среди таковых — система Шаблон:Нп2 1957 года (почерпнутая из замечаний Шаблон:Iw и Шаблон:Iw к французскому переводу статьи Генцена), и её усовершенствованная версия, опубликованная в 1965 году Шаблон:Нп2, устраняющие практические неудобства использования изначальной нутрально-секвенциальной ГенценаШаблон:Sfn. Более радикальные усовершенствования для практического удобства вывода натурального типа в секвенциальных исчислениях были предложены Шаблон:Нп2: в его системе для классической логики применены две аксиомы (<math>A \rightarrow A</math> и <math>\rightarrow A = A</math>, а в правилах вывода пропозициональные связки используются не только в сукцедентах, но и в антецедентах, притом как в нижних, так и в верхних секвенцияхШаблон:Sfn. Шаблон:Раздел не завершён

Симметрия

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

Литература

• Шаблон:БСЭ3
• Книга:Математическая энциклопедия
• Шаблон:Источник/НФЭ
• Шаблон:Статья
• Шаблон:Книга
• Шаблон:Книга
• Шаблон:Книга
• Шаблон:Статья
• Шаблон:Cite web