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

редактировать

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

Содержание

1 Правило отсечения
2 Исключение отсечения
3 Последствия теоремы
4 См. также
5 Примечания
6 Ссылки
7 Внешние ссылки

Правило вырезания

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

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

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

$Γ ⊢ A, Δ {\ displaystyle \ Gamma \ vdash A, \ Delta}$ $\ Gamma \ vdash A, \ Delta$

$Π, A ⊢ Λ {\ displaystyle \ Pi, A \ vdash \ Lambda}$ $\ Pi, A \ vdash \ Lambda$

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

$Γ, Π ⊢ Δ, Λ {\ displaystyle \ Gamma, \ Pi \ vdash \ Delta, \ Lambda}$ $\ Gamma, \ Pi \ vdash \ Delta, \ Lambda$

То есть "отсекает" количество вхождений формулы $A {\ displaystyle A}$ $A$ вне отношения вывода.

Исключение отсечения

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

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

$Γ ⊢ A {\ displaystyle \ Gamma \ vdash A}$ $\ Gamma \ vdash A$

$Π, A ⊢ B {\ displaystyle \ Pi, A \ vdash B}$ $\ Pi, A \ vdash B$

позволяет вывести

$Γ, Π ⊢ B {\ displaystyle \ Gamma, \ Pi \ vdash B}$ $\ Gamma, \ Pi \ vdash B$

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

Следствия теоремы

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

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

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

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

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

См. Также

Примечания

Ссылки

Гентцен, Герхард (1934 –1935). "Untersuchungen über das logische Schließen". Mathematische Zeitschrift. 39 : 405–431. doi : 10.1007 / BF01201363.
Гентцен, Герхард (1964). «Исследования по логической дедукции». American Philosophical Quarterly. 1 (4): 249–287.
Генцен, Герхард (1965). «Исследования по логической дедукции». American Philosophical Quarterly. 2 (3): 204–218.
Untersuchungen über das logische Schließen I
Untersuchungen über das logische Schließen II
Curry, Haskell Brooks (1977) [1963]. Основы математической логики. Нью-Йорк: Dover Publications Inc. ISBN 978-0-486-63462-3. CS1 maint: ref = harv (ссылка )
Клини, Стивен Коул (2009) [1952]. Введение в метаматематику. Ishi Press International. ISBN 978-0-923891-57-2. CS1 maint: ref = harv (ссылка )

Внешние ссылки

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