자름-제거 정리

자름-제거(cut-elimination) 정리, 혹은 겐첸의 Haupsatz는 시퀀트 계산에서 자름 규칙을 사용한 증명을 항상 자름 규칙을 사용하지 않은 증명으로 환원시킬 수 있음을 보여주는 정리이다.

프로그래밍 언어론 관점에서 자름-제거 정리는 hereditary substitution에 대응된다.