カット除去定理

カット除去定理（カットじょきょていり、）は、シークエント計算の手法の重要性を示す、数理論理学の主要な結果のひとつである。（数理論理学の）基本定理と呼ぶこともある。ゲルハルト・ゲンツェンが1934年に書いた記念碑的論文 "" で、古典論理と直観論理の体系をそれぞれ形式化したシークエント計算の形式的体系 LK 及び LJ において、最初に証明が与えられた。カット除去定理は、シークエント計算の推論規則であるカット規則を用いて証明可能な式には、カット規則を用いない証明図もまた必ず存在することを示したものである。
シークエント.
シークエントは複数の文からなる論理表現であり、
という形式をとる。これは、直観的には
という意味に理解することができる（ここで左辺が論理積で、右辺は論理和であることに注意されたい）。前提である左辺は任意個の論理式からなり、左辺が空のシークエントが証明できた場合、その右辺は無前提に主張可能なトートロジーだということになる。逆に、結論である右辺が空となるなら、左辺は矛盾していると言える。LK（古典論理）では、右辺もまた任意個の論理式からなるが、LJ（直観論理）では、右辺には多くとも一つの文しか置くことが許されない。右辺に複数の論理式を置けることと、右縮約規則があるときに排中律が成り立つこととは等価である。ただし、シークエント計算は非常に表現能力が高く、右辺に多数の論理式のある直観論理のシークエント計算も存在する。Jean-Yves Girard の論理体系 LC においては、右辺に高々一個の論理式しか持たない古典論理の自然な定式化も容易に得られている。ここで鍵となるのは、論理的な推論規則と構造に関する推論規則との相互作用である。
カット規則.
「カット規則」とは、シークエント計算の一般的な推論規則であり、次のような形式で表現される。
と
とが、ともに成立しているとき、次を導出できる。
すなわち、ここでは論理式 C が帰結からカットされている。
カット除去定理.
カット除去定理は、ある論理体系でカット規則を使って証明可能なシークエントは、この規則を使わずとも証明可能であることを示したものである。そのシークエントが定理であるとき、カット除去定理は、単に、その証明の過程で使われた補題 C をインライン化できることを示している。すなわち、定理の証明が補題 C を使っている場合、その箇所を全て C の証明に置き換えることで、新しい完全な証明図を与えることができるということである。従って、カット規則は許容できる規則 (admissible rule) である。
シークエント計算で形式化される体系では、カット規則を使わない証明を「解析的証明; analytic proof」と呼ぶ。そのような証明は必ず長くなるというわけではないが、一般的には長くなる。 の論文 "Don't Eliminate Cut!" では、カット規則を使えば1ページで表せる証明（導出）があったとき、その解析的証明が完了するまでに宇宙の寿命より長くなる例が示されている。
この定理を応用して、様々な派生的結果を示すことができる。
カット除去は、クレイグの補間定理を証明する際に強力な道具となる。Prolog というプログラミング言語を考案する元となった導出に基づいた証明探索手法の可能性は、適切な論理体系におけるカット規則の許容性 (admissibility) に依存している。カリー・ハワード同型対応を使った高階ラムダ計算に基づく証明体系では、カット除去アルゴリズムは強い推論属性に対応している（全ての証明項には正規形があり、その正規形には任意の推論の完全なシーケンスから到達可能である）。