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

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

Правило обрезки [ править ]

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

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

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

$\Gamma \vdash A,\Delta$

и

$\Pi ,A\vdash \Lambda$

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

$\Gamma ,\Pi \vdash \Delta ,\Lambda$

То есть «обрезает» вхождения формулы $A$ вне отношения вывода.

Удаление выреза [ править ]

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

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

$\Gamma \vdash A$

и

$\Pi ,A\vdash B$

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

$\Gamma ,\Pi \vdash B$

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

Следствия теоремы [ править ]

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

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

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

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

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

См. также [ править ]

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

^ Карри 1977 , стр. 208–213, дает 5-страничное доказательство теоремы исключения. См. также стр. 188, 250.
^ Kleene 2009 , стр. 453, дает очень краткое доказательство теоремы об исключении разреза.
^ Вильфрид Бухгольц, Beweistheorie (конспекты университетских лекций об исключении порезов, немецкий, 2002–2003 гг.)
^ Булос 1984 , стр. 373–378.

Ссылки [ править ]

Генцен, Герхард (1935). «Исследования по логическим рассуждениям. И.». Математический журнал . 39 : 176-210. дои : 10.1007/BF01201353 .
- Исследования логических рассуждений I (Archive.org)
- Генцен, Герхард (1964). «Исследования по логической дедукции». Американский философский ежеквартальный журнал . 1 (4): 249–287.
Генцен, Герхард (1935). «Исследования по логическим рассуждениям. II». Математический журнал . 39 : 405–431. дои : 10.1007/BF01201363 .
- Исследования логических рассуждений II (Archive.org)
- Генцен, Герхард (1965). «Исследования по логической дедукции». Американский философский ежеквартальный журнал . 2 (3): 204–218.
Карри, Хаскелл Брукс (1977) [1963]. Основы математической логики . Dover Publications Inc. Нью-Йорк: ISBN 978-0-486-63462-3 .
Клини, Стивен Коул (2009) [1952]. Введение в метаматематику . Иши Пресс Интернешнл. ISBN 978-0-923891-57-2 .
Булос, Джордж (1984). «Не устраняйте обрезку». Журнал философской логики . 13 (4): 373–378.

Внешние ссылки [ править ]

Алексей Сахаров. «Теорема исключения разреза» . Математический мир .
Драгалин, А.Г. (2001) [1994], «Секвенционное исчисление» , Энциклопедия математики , EMS Press

[1] Карри 1977 , стр. 208–213, дает 5-страничное доказательство теоремы исключения. См. также стр. 188, 250.

[2] Kleene 2009 , стр. 453, дает очень краткое доказательство теоремы об исключении разреза.

[3] Вильфрид Бухгольц, Beweistheorie (конспекты университетских лекций об исключении порезов, немецкий, 2002–2003 гг.)

[4] Булос 1984 , стр. 373–378.

[1]

[2]

[3]

[4]