컷 엘리미네이션 정리

컷 엘리미네이션 정리(또는 겐첸의 하우프트사츠)는 시퀀스 미적분학의 의의를 확립하는 중심적 결과물이다.Gerhard Gentzen에 의해 원래 LJ와 LK가 각각 직관과 고전적 논리를 공식화하는 시스템에 대해 1934년 그의 랜드마크 논문 "논리 추론에 대한 투자"에서 증명되었다.절단-제거 정리는 절단 규칙을 사용하는 순차 미적분학에서 증거를 소유하는 모든 판단은 절단되지 않은 증거, 즉 절단 규칙을 사용하지 않는 증거도 가지고 있다고 명시하고 있다.^[1][2]

컷 룰

A sequent is a logical expression relating multiple formulas, in the form "${\displaystyle A_{1},A_{2},A_{3},\ldots \vdash B_{1},B_{2},B_{3},\ldots }$", which is to be read as "${\displaystyle A_{1},A_{2},A_{3},\ldots }$ proves ${\displaystyle B_1}$${\displaystyle B_{1},B_{2},B_{3},\ldots }$", and (as glossed by Gentzen) should be understood as equivalent to the truth-function "If (${\displaystyle A_{1}}$ and ${\displaystyle A_{2}}$ and ${\displaystyle A_{3}}$ …) then (${\displaystyle B_{1}}$ or ${\$$displaystyle B_{2$}}: 또는$$ ${\displaystyle {B\mathrm{}}_{}}$ 3 ${\$ …"$$^[3] 왼쪽(LHS)은 접속사(및)이고 오른쪽(RHS)은 분리(또는)라는 점에 유의한다.

LHS는 임의로 많은 공식 또는 적은 공식일 수 있다. LHS가 비어 있을 때 RHS는 자동학이다.LK에서 RHS에는 공식이 얼마든지 있을 수 있다. LJ에서 RHS에는 공식이 하나만 있을 수도 있고 없을 수도 있다. 여기서 우리는 RHS에서 둘 이상의 공식을 허용하는 것은 오른쪽 수축 규칙이 있는 경우 제외된 중간 법칙의 허용 능력에 동등하다는 것을 알 수 있다.그러나, 이열 미적분은 상당히 표현적인 틀이며, RHS에서 많은 공식을 허용하는 직관적 논리에 대한 이열 미적분학이 제안되어 왔다.Jean-Yves Girard의 논리 LC로부터 RHS가 적어도 하나의 공식을 포함하는 고전적 논리의 다소 자연스러운 공식화를 얻기가 쉽다; 그것은 여기에서 핵심인 논리적 규칙과 구조적 규칙의 상호 작용이다.

"자르기"는 연속 미적분학의 정상적 진술에 있는 규칙이며, 다른 증명 이론에서는 다양한 규칙과 동등한 것으로 주어진다.

1. ${\displaystyle \Gamma \vdash A,\Delta }$

그리고

2. ${\displaystyle \Pi ,A\vdash \Lambda }$

추론할 수 있게 하다

3. $\displaystyle \Gamma ,\Pi \vdash \Delta ,\Lambda }$

즉, A $공식{\displaystyle }$ ${\displaystyle A}$의 발생을 추론적 관계에서$$ "삭제"하는 것이다.

절단 제거

컷 엘리미네이션 정리는 컷(Cut) 규칙을 사용하여 (특정 시스템에 대해) 순차적으로 증명할 수 있다는 것을 이 규칙을 사용하지 않고 증명할 수 있다고 명시한다.

RHS에 공식이 하나만 있는 시퀀스 캘커리의 경우 "컷" 규칙은 주어진 값을 읽는다.

1. ${\displaystyle \Gamma \vdash A}$

그리고

2. ${\displaystyle \Pi ,A\vdash B}$

추론할 수 있게 하다

3. ${\displaystyle \Gamma ,\Pi \vdash B}$

$우리$가 B ${\displaystyle$B}을(를) 정리라고$$ 생각한다면, 이 경우 절단-제거는 단순히 이 정리를 증명하는 데 사용된$$ 보조정리 $A{\displaystyle }$ ${\displaystyle$ A$}$이(가) 삽입될 수 있다고 말한다.정리의 증명에서 보조정리 $A{\displaystyle }$ ${\displaystyle A}$이$($가) 언급될 때마다, 우리는 $발생$을 A$${\$displaystyle$A}의 증명으로 대체할 수 있다$.$ 따라서 절단 규칙은 허용된다.

정리의 결과

시퀀스 미적분학에서 공식화된 시스템의 경우, 분석적 증명들은 Cut을 사용하지 않는 증거들이다.일반적으로 그러한 증거는 물론 더 길어질 것이며, 반드시 사소한 것은 아니다.조지 볼로스는 그의 에세이 "컷을 제거하지 말라!"^[4]에서 컷을 이용해 한 페이지에 완성할 수 있지만, 우주의 수명 동안 분석적 증거가 완성될 수 없는 파생이 있음을 보여주었다.

정리에는 다음과 같은 여러 가지 풍부한 결과가 있다.

• 시스템이 불합리한 것의 증거를 인정하면 일관성이 없다.시스템에 절삭 제거 정리가 있다면, 만약 그것이 불합리한 것에 대한 증거, 또는 빈 순서에 대한 증거를 가지고 있다면, 또한 절삭 없이 불합리한 것(또는 빈 순서에 대한 증거)을 가지고 있어야 한다.일반적으로 그러한 증거가 없다는 것을 확인하는 것은 매우 쉽다.그러므로 일단 어떤 시스템이 절단 제거 정리를 갖는 것으로 보여지면, 그 시스템이 일관성이 있다는 것은 보통 즉시다.
• 일반적으로 또한 시스템은 적어도 첫 번째 순서의 논리에서는 증명-이론적 의미론에 대한 몇 가지 접근방식에서 중요한 속성인 보조양식 특성을 가진다.

절삭 제거는 보간 이론들을 증명하는 가장 강력한 도구들 중 하나이다.Prolog 프로그래밍 언어로 이어지는 필수적인 통찰력인 해상도에 기반한 증명 검색을 수행할 가능성은 적절한 시스템에서 Cut의 능력에 달려 있다.

Curry-Howard 이형태를 통한 고차 타입의 람다 미적분학을 기반으로 하는 증명 시스템의 경우, 절단 제거 알고리즘은 강력한 정규화 속성에 해당한다(모든 증명 용어는 한정된 수의 단계로 정상 형태로 감소).

참고 항목

• 공제정리
• 페아노의 공리에 대한 겐첸의 일관성 증명

메모들

참조

• Gentzen, Gerhard (1934–1935). "Untersuchungen über das logische Schließen". Mathematische Zeitschrift. 39: 405–431. doi:10.1007/BF01201363.
• Gentzen, Gerhard (1964). "Investigations into logical deduction". American Philosophical Quarterly. 1 (4): 249–287.
• Gentzen, Gerhard (1965). "Investigations into logical deduction". American Philosophical Quarterly. 2 (3): 204–218.
• 운터수충겐 über das logische Schließen 1세
• 운터수충겐 über das logische Schließen 2세
• Curry, Haskell Brooks (1977) [1963]. Foundations of mathematical logic. New York: Dover Publications Inc. ISBN 978-0-486-63462-3.
• Kleene, Stephen Cole (2009) [1952]. Introduction to metamathematics. Ishi Press International. ISBN 978-0-923891-57-2.
• Boolos, George (1984). "Don't eliminate cut". Journal of Philosophical Logic. 13 (4): 373–378.

외부 링크

• Alex Sakharov. "Cut Elimination Theorem". MathWorld.
• Dragalin, A.G. (2001) [1994], "Sequent calculus", Encyclopedia of Mathematics, EMS Press