자름-제거 정리
자름-제거 정리 또는 컷-제거 정리(영어: cut-elimination theorem)는 시퀀트 계산의 중요성을 보여주는 증명론의 중요 정리이다. 이는 본래 게르하르트 겐첸이 1934년 논문 "논리적 연역에 관한 연구(Untersuchungen über das logische Schließen)"에서 고전 논리와 직관 논리를 각각 형식화하는 시퀀트 계산 체계인 LJ와 LK를 제시하면서 증명한 것이다. 컷-제거 정리의 핵심은, 시퀀트 연산에서 자름 규칙(cut rule)을 사용하여 증명 가능한 식은 자름 규칙을 사용하지 않고도 증명하는 것이 가능하다는 내용이다.
시퀀트 계산과 자름 규칙 편집
시퀀트 계산(영어: sequent calculus)은 여러 개의 논리적 문장으로 이루어지는 논리 표현의 일종으로,
와 같은 형식이며, 이는 직관적으로 "A이며 B이며 C이며... 라 가정하면 P이거나 Q이거나 R이거나... 임을 증명가능하다"라는 의미를 가진다. 곧 논리곱을 전건, 논리합을 후건으로 삼는다. 참고로 직관논리(LJ)에서는 우변에 하나의 논리식만을 놓을 수 있다. 자연 연역처럼 라는 동일성의 공리만을 공리로 채택하고 많은 추론규칙들을 사용하여 증명을 구성해나가는 방식이다.
시퀀트 계산에서 '자름'(cut)은 추론 규칙 중 하나로, 예컨대 이면서 이라면, 를 추론해낼 수 있다는 규칙이다. 곧 이러한 상황에서는 논리식 를 추론 과정에서 '잘라' 버릴 수 있다는 규칙이다.
자름-제거 정리 편집
자름-제거(cut-elemination) 정리는 자름 규칙을 사용하는 임의의 증명 시퀀트에 대해서 자름 규칙을 생략하는 방법이 존재한다는 정리이다.
곧 와 로부터 를 추론 가능하다는 시퀀트 증명에서, 를 정리(theorem)라 한다면 그 증명에 쓰인 보조정리(lemma) 를 그 보조정리를 증명하는 과정으로 대체해서 새로운 증명도(證明圖)를 쓸 수 있다는 것이다. 고로 자름 규칙은 허용가능(admissable)한 규칙이다.
정리의 결과 편집
이러한 대체가 가능하기에 자름 규칙은 충분히 증명과정에 사용될만한 추론 규칙이라는 것이 보여진 것이다. 시퀀트 계산의 체계에서는 자름 규칙을 사용하지 않는 증명을 해석적 증명(영어: analytic proof)이라 하는데, 이러한 증명은 반드시는 아니지만 일반적으로 굉장히 길어지게 된다. 조지 불로스는 그의 논문 "Don't Eliminate Cut!"에서 자름 규칙을 사용하면 1페이지만에 도출 가능하지만 해석적으로 나타낼 시에 우주의 수명 안에 완료할 수 없는 증명의 예시를 보인 바 있다.
자름-제거 정리를 응용하여 여러 결과를 얻어낼 수 있다:
- 어떠한 논리체계가 그것이 모순명제(빈 시퀀트)의 증명을 허용한다면, 그 체계는 모순적(inconsistent)이다. 증명을 위해 어떤 체계에서 자름-제거 정리가 성립한다고 하자. 그러면 만약 그 체계에서 빈 시퀀트를 도출할 수 있다고 가정하면 자름규칙을 사용하지 않은 빈 시퀀트 도출 방법도 있어야 한다. 그러나 그러한 방법이 없다는 것은 추론규칙들을 체크해보면 쉽게 알 수 있다. 고로, 자름-제거 정리가 성립하는 체계는 무모순적이다.
- 또한 자름-제거 정리가 성립하는 체계에서는, 적어도 1차 논리인 경우에는, 부분식 성질(subformula property)이 성립한다. 이는 증명론적 의미론에서 중요하게 쓰이는 성질로, 증명과정(증명도)에 등장하는 모든 논리식이 귀결의 부분식(subformula)가 되는 성질이다.
- 크레이그의 보간 정리 등을 증명할 때 강력한 도구로서 활용된다.