カット除去定理
カット除去定理は、ある論理体系でカット規則を使って証明可能なシークエントは、この規則を使わずとも証明可能であることを示したものである。そのシークエントが定理であるとき、カット除去定理は、単に、その証明の過程で使われた補題 C をインライン化できることを示している。すなわち、定理の証明が補題 C を使っている場合、その箇所を全て C の証明に置き換えることで、新しい完全な証明図を与えることができるということである。従って、カット規則は許容できる規則 (admissible rule) である。
シークエント計算で形式化される体系では、カット規則を使わない証明を「解析的証明; analytic proof」と呼ぶ。そのような証明は必ず長くなるというわけではないが、一般的には長くなる。George Boolos の論文 "Don't Eliminate Cut!" では、カット規則を使えば1ページで表せる証明(導出)があったとき、その解析的証明が完了するまでに宇宙の寿命より長くなる例が示されている。
この定理を応用して、様々な派生的結果を示すことができる。
カット除去定理の成立する論理体系では、矛盾命題(空のシークエント)を証明することができない。いま、ある論理体系でカット除去定理が成り立っていると仮定する。このとき、その体系で矛盾命題の証明が可能である(矛盾命題に証明図が存在する)と仮定すると、その証明図と同一の帰結をもたらす証明図で、カット規則を用いないような証明図もまた存在している筈である。
しかし、そのような証明図が構成可能でないことは、推論規則をチェックしてゆけば、一般に容易に確認できる(その確認を困難にするのがカット規則なのであり、カット除去定理がその除去できることを保証する)。従って、ある論理体系でカット除去定理を示すことができれば、その体系の無矛盾性をもただちに導くことができる。
通常、カット除去定理の成立する論理体系では、少なくとも一階述語論理までの体系であるならば、部分論理式属性 (subformula property) も成り立つ。これは、証明図中に登場する全ての論理式が、帰結となる論理式の部分論理式になっているという性質である。証明にカット規則が用いられている場合は、その証明図からカットを除去した証明図が、この性質をみたしている。このことは、証明論に基づく意味論への幾つかのアプローチにおいて重要な役割を果たす。また、古典命題計算の体系では、部分論理式属性は真偽を検証する必要のある論理式の数を有限個に限定し、このことから古典命題計算の決定可能性を導くこともできる。
カット除去は、クレイグの補間定理を証明する際に強力な道具となる。Prolog というプログラミング言語を考案する元となった導出に基づいた証明探索手法の可能性は、適切な論理体系におけるカット規則の許容性 (admissibility) に依存している。カリー・ハワード同型対応を使った高階ラムダ計算に基づく証明体系では、カット除去アルゴリズムは強い推論属性に対応している(全ての証明項には正規形があり、その正規形には任意の推論の完全なシーケンスから到達可能である)。