Теорема исключения сечения (или гаупцац Гентцена ) является центральным результатом, устанавливающим значение секвенциального исчисления . Первоначально это было доказано Герхардом Генценом в его знаменательной статье 1934 года «Исследования логического вывода» для систем LJ и LK, формализующих интуиционистскую и классическую логику соответственно. Теорема об исключении отсечения утверждает, что любое суждение, имеющее доказательство в исчислении секвенций с использованием правила отсечения, также обладает доказательством без отсечения , то есть доказательством, не использующим правило отсечения. [1][2]
Правило разреза
Секвенция представляет собой логическое выражение , относящееся несколько формул, в виде "" , который следует читать как " доказывает " , и (как пояснил Гентцен) следует понимать как эквивалент функции истинности" Если ( а также а также …) тогда ( или же или же …). » [3] Обратите внимание, что левая часть (LHS) - это конъюнкция (и), а правая часть (RHS) - это дизъюнкция (или).
LHS может иметь произвольно много или мало формул; когда LHS пуста, RHS - тавтология . В LK RHS также может иметь любое количество формул - если их нет, LHS является противоречием , тогда как в LJ RHS может иметь только одну формулу или ни одной: здесь мы видим, что разрешение более одной формулы в RHS является при наличии правила правильного сокращения эквивалентно допустимости закона исключенного третьего . Однако секвенциальное исчисление является довольно выразительной структурой, и для интуиционистской логики были предложены секвентальные исчисления, допускающие множество формул в RHS. Из логики Жана-Ива Жирара LC легко получить довольно естественную формализацию классической логики, в которой RHS содержит не более одной формулы; ключевым здесь является взаимодействие логических и структурных правил.
«Отсечение» - это правило в обычной формулировке исчисления секвенций , эквивалентное множеству правил в других теориях доказательства , которые, учитывая
а также
позволяет сделать вывод
То есть "отсекает" вхождения формулы из выводного отношения.
Устранение порезов
Теорема отсечения-исключения утверждает, что (для данной системы) любая секвенция, доказуемая с помощью правила Cut, может быть доказана без использования этого правила.
Для последовательных исчислений, которые имеют только одну формулу в правой части, правило «вырезать» гласит, что
а также
позволяет сделать вывод
Если мы подумаем о как теорема, то отсечение-исключение в этом случае просто говорит, что лемма используется для доказательства этой теоремы. Всякий раз, когда в доказательстве теоремы упоминается лемма , мы можем заменить вхождения на доказательство . Следовательно, правило разреза допустимо .
Следствия теоремы
Для систем, сформулированных в исчислении секвенций, аналитические доказательства - это те доказательства, которые не используют Cut. Обычно такое доказательство, конечно, будет длиннее, и не обязательно тривиально. В своем эссе «Не устраняйте порез!» [4] Джордж Булос продемонстрировал, что существует вывод, который можно завершить на странице с помощью вырезания, но аналитическое доказательство которого не может быть завершено за время существования Вселенной.
Теорема имеет много богатых следствий:
- Система непоследовательна, если допускает доказательство абсурда. Если система имеет теорему об исключении сечения, то, если она имеет доказательство абсурда или пустой секвенции, она также должна иметь доказательство абсурда (или пустой секвенции) без сокращений. Обычно очень легко проверить, что таких доказательств нет. Таким образом, как только система демонстрирует наличие теоремы об исключении разрезов, обычно сразу становится понятно, что система является непротиворечивой.
- Обычно также система имеет, по крайней мере, в логике первого порядка, свойство подформулы , важное свойство в нескольких подходах к семантике теории доказательств .
Исключение разрезов - один из самых мощных инструментов для доказательства интерполяционных теорем . Возможность выполнения поиска на основе разрешения - важная идея, ведущая к языку программирования Prolog , - зависит от допустимости Cut в соответствующей системе.
Для систем доказательства, основанных на типизированном лямбда-исчислении более высокого порядка с помощью изоморфизма Карри – Ховарда , алгоритмы исключения разрезов соответствуют свойству строгой нормализации (каждый член доказательства приводится к нормальной форме за конечное число шагов ).
Смотрите также
Заметки
- ^ Карри 1977 , стр. 208-213, дает 5-страничное доказательство теоремы элиминации. См. Также страницы 188, 250.
- ↑ Kleene 2009 , pp. 453, дает очень краткое доказательство теоремы об исключении сечения.
- ^ Вильфрид Бухгольц, Beweistheorie (университетские конспекты о светотеневой ликвидации, немецкий, 2002-2003)
- ^ Boolos 1984 , стр. 373-378
Рекомендации
- Генцен, Герхард (1934–1935). "Untersuchungen über das logische Schließen". Mathematische Zeitschrift . 39 : 405–431. DOI : 10.1007 / BF01201363 .
- Генцен, Герхард (1964). «Исследования по логической дедукции». Американский философский квартал . 1 (4): 249–287.
- Генцен, Герхард (1965). «Исследования по логической дедукции». Американский философский квартал . 2 (3): 204–218.
- Untersuchungen über das logische Schließen I
- Untersuchungen über das logische Schließen II
- Карри, Хаскелл Брукс (1977) [1963]. Основы математической логики . Нью-Йорк: ISBN Dover Publications Inc. 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