자름-제거 정리
From Wikipedia, the free encyclopedia
자름-제거 정리 또는 컷-제거 정리(영어: cut-elimination theorem)는 시퀀트 계산의 중요성을 보여주는 증명론의 중요 정리이다. 이는 본래 게르하르트 겐첸이 1934년 논문 "논리적 연역에 관한 연구(Untersuchungen über das logische Schließen)"에서 고전 논리와 직관 논리를 각각 형식화하는 시퀀트 계산 체계인 LJ와 LK를 제시하면서 증명한 것이다. 컷-제거 정리의 핵심은, 시퀀트 연산에서 자름 규칙(cut rule)을 사용하여 증명 가능한 식은 자름 규칙을 사용하지 않고도 증명하는 것이 가능하다는 내용이다.