Теорема об исключении разрезов

Теорема об устранении сечения (или теорема Генцена ) является центральным результатом, устанавливающим значимость секвенциального исчисления . Первоначально она была доказана Герхардом Генценом в его знаковой статье 1934 года «Исследования в области логической дедукции» для систем LJ и LK, формализующих интуиционистскую и классическую логику соответственно. Теорема об устранении сечения утверждает, что любое суждение, имеющее доказательство в секвенциальном исчислении, использующее правило сечения , также имеет доказательство без сечения , то есть доказательство, которое не использует правило сечения. ^{[1] [2]}

Секвенция — это логическое выражение , связывающее несколько формул, в форме « »${\displaystyle A_{1},A_{2},A_{3},\ldots \vdash B_{1},B_{2},B_{3},\ldots }$ , которое следует читать как «${\displaystyle A_{1},A_{2},A_{3},\ldots }$ доказывает » и (в толковании Генцена) следует понимать как эквивалент функции истинности «Если ( и и …), то ( или или …)». ^[3] Обратите внимание, что левая часть (LHS) представляет собой конъюнкцию (и), а правая часть (RHS) — дизъюнкцию (или). ${\displaystyle B_{1},B_{2},B_{3},\ldots }$${\displaystyle А_{1}}$${\displaystyle A_{2}}$${\displaystyle A_{3}}$${\displaystyle B_{1}}$${\displaystyle B_{2}}$${\displaystyle B_{3}}$

LHS может иметь произвольно много или мало формул; когда LHS пуста, RHS является тавтологией . В LK RHS также может иметь любое количество формул — если нет ни одной, LHS является противоречием , тогда как в LJ RHS может иметь только одну формулу или ни одной: здесь мы видим, что допущение более чем одной формулы в RHS эквивалентно, при наличии правила правильного сокращения, допустимости закона исключенного третьего . Однако исчисление последовательностей является довольно выразительной структурой, и были предложены исчисления последовательностей для интуиционистской логики, которые допускают много формул в RHS. Из логики LC Жана-Ива Жирара легко получить довольно естественную формализацию классической логики, где RHS содержит не более одной формулы; именно взаимодействие логических и структурных правил является здесь ключом.

«Разрез» — это правило вывода в обычном утверждении секвенциального исчисления , эквивалентное множеству правил в других теориях доказательств , которые, учитывая,

1. ${\displaystyle \Гамма \vdash А,\Дельта }$

и

2. ${\displaystyle \Пи ,A\vdash \Лямбда }$

позволяет сделать вывод

3. ${\displaystyle \Гамма ,\Пи \vdash \Дельта ,\Лямбда }$

То есть он «вырезает» вхождения формулы из выводимого отношения. ${\displaystyle А}$

Теорема об устранении сечения утверждает, что (для данной системы) любая последовательность, доказуемая с использованием правила сечения, может быть доказана без использования этого правила.

Для последовательных исчислений, имеющих только одну формулу в правой части, правило «Сокращения» гласит, учитывая, что

1. ${\displaystyle \Гамма \vdash A}$

и

2. ${\displaystyle \Пи ,A\vdash B}$

позволяет сделать вывод

3. ${\displaystyle \Гамма ,\Пи \vdash B}$

Если мы думаем о как о теореме, то в этом случае исключение сечения просто говорит о том, что лемма, используемая для доказательства этой теоремы, может быть вставлена. Всякий раз, когда доказательство теоремы упоминает лемму , мы можем заменить вхождения для доказательства . Следовательно, правило сечения допустимо .${\displaystyle Б}$${\displaystyle А}$ ${\displaystyle А}$${\displaystyle А}$

Для систем, сформулированных в секвенциальном исчислении, аналитические доказательства — это те доказательства, которые не используют Cut. Обычно такое доказательство будет длиннее, конечно, и не обязательно тривиально. В своем эссе «Не исключайте Cut!» ^[4] Джордж Булос продемонстрировал, что существует вывод, который можно завершить на странице с использованием Cut, но аналитическое доказательство которого не может быть завершено за время существования вселенной.

Теорема имеет множество важных следствий:

• Система является противоречивой , если она допускает доказательство абсурда. Если система имеет теорему об устранении сечения, то если у нее есть доказательство абсурда или пустой секвенции, она также должна иметь доказательство абсурда (или пустой секвенции) без сокращений. Обычно очень легко проверить, что таких доказательств нет. Таким образом, как только показано, что система имеет теорему об устранении сечения, обычно сразу становится ясно, что система непротиворечива.
• Обычно система также имеет, по крайней мере в логике первого порядка, свойство подформулы , важное свойство в нескольких подходах к семантике теории доказательств .

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

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

• Теорема дедукции
• Доказательство непротиворечивости Генцена для аксиом Пеано

• Генцен, Герхард (1935). «Untersuchungen über das logische Schließen. I.». Mathematische Zeitschrift . 39 : 176–210. дои : 10.1007/BF01201353.
  • Untersuchungen über das logische Schließen I (Archive.org)
  • Генцен, Герхард (1964). «Исследования логической дедукции». American Philosophical Quarterly . 1 (4): 249–287.
• Генцен, Герхард (1935). «Untersuchungen über das logische Schließen. II». Mathematische Zeitschrift . 39 : 405–431. дои : 10.1007/BF01201363.
  • Untersuchungen über das logische Schließen II (Archive.org)
  • Генцен, Герхард (1965). «Исследования логической дедукции». American Philosophical Quarterly . 2 (3): 204–218.
• Карри, Хаскелл Брукс (1977) [1963]. Основы математической логики . Нью-Йорк: Dover Publications Inc. ISBN 978-0-486-63462-3.
• Клини, Стивен Коул (2009) [1952]. Введение в метаматематику . Ishi Press International. ISBN 978-0-923891-57-2.
• Булос, Джордж (1984). «Не устраняйте разрез». Журнал философской логики . 13 (4): 373–378.

• Алекс Сахаров. "Теорема об исключении разрезов". MathWorld .
• Драгалин, А.Г. (2001) [1994], "Последовательное исчисление", Энциклопедия математики , EMS Press