ja %E3%82%AB%E3%83%83%E3%83%88%E9%99%A4%E5%8E%BB%E5%AE%9A%E7%90%86

カット除去定理（カットじょきょていり、英: Cut-elimination theorem）は、シークエント計算の手法の重要性を示す、数理論理学の主要な結果のひとつである。（数理論理学の）基本定理と呼ぶこともある。ゲルハルト・ゲンツェンが1934年に書いた記念碑的論文 "Investigations into Logical Deduction" で、古典論理と直観論理の体系をそれぞれ形式化したシークエント計算の形式的体系 LK 及び LJ において、最初に証明が与えられた。カット除去定理は、シークエント計算の推論規則であるカット規則を用いて証明可能な式には、カット規則を用いない証明図もまた必ず存在することを示したものである。

シークエント

シークエントは複数の文からなる論理表現であり、

$A,B,C,\ldots \vdash P,Q,R,\ldots$

という形式をとる。これは、直観的には

「A かつ B かつ C かつ… を仮定すれば、P または Q または R または… が証明可能である」

という意味に理解することができる（ここで左辺が論理積で、右辺は論理和であることに注意されたい）。前提である左辺は任意個の論理式からなり、左辺が空のシークエントが証明できた場合、その右辺は無前提に主張可能なトートロジーだということになる。逆に、結論である右辺が空となるなら、左辺は矛盾していると言える。LK（古典論理）では、右辺もまた任意個の論理式からなるが、LJ（直観論理）では、右辺には多くとも一つの文しか置くことが許されない。右辺に複数の論理式を置けることと、右縮約規則があるときに排中律が成り立つこととは等価である。ただし、シークエント計算は非常に表現能力が高く、右辺に多数の論理式のある直観論理のシークエント計算も存在する。Jean-Yves Girard の論理体系 LC においては、右辺に高々一個の論理式しか持たない古典論理の自然な定式化も容易に得られている。ここで鍵となるのは、論理的な推論規則と構造に関する推論規則との相互作用である。

カット規則

「カット規則」とは、シークエント計算の一般的な推論規則であり、次のような形式で表現される。

(1) $(A,B,\ldots )\vdash C$

と

(2) $C\vdash (D,E,\ldots )$

とが、ともに成立しているとき、次を導出できる。

(3) $(A,B,\ldots )\vdash (D,E,\ldots )$

すなわち、ここでは論理式 C が帰結からカットされている。

カット除去定理

カット除去定理は、ある論理体系でカット規則を使って証明可能なシークエントは、この規則を使わずとも証明可能であることを示したものである。そのシークエントが定理であるとき、カット除去定理は、単に、その証明の過程で使われた補題 C をインライン化できることを示している。すなわち、定理の証明が補題 C を使っている場合、その箇所を全て C の証明に置き換えることで、新しい完全な証明図を与えることができるということである。従って、カット規則は許容できる規則 (admissible rule) である。

シークエント計算で形式化される体系では、カット規則を使わない証明を「解析的証明; analytic proof」と呼ぶ。そのような証明は必ず長くなるというわけではないが、一般的には長くなる。George Boolos の論文 "Don't Eliminate Cut!" では、カット規則を使えば1ページで表せる証明（導出）があったとき、その解析的証明が完了するまでに宇宙の寿命より長くなる例が示されている。

この定理を応用して、様々な派生的結果を示すことができる。

カット除去定理の成立する論理体系では、矛盾命題（空のシークエント）を証明することができない。いま、ある論理体系でカット除去定理が成り立っていると仮定する。このとき、その体系で矛盾命題の証明が可能である（矛盾命題に証明図が存在する）と仮定すると、その証明図と同一の帰結をもたらす証明図で、カット規則を用いないような証明図もまた存在している筈である。しかし、そのような証明図が構成可能でないことは、推論規則をチェックしてゆけば、一般に容易に確認できる（その確認を困難にするのがカット規則なのであり、カット除去定理がその除去できることを保証する）。従って、ある論理体系でカット除去定理を示すことができれば、その体系の無矛盾性をもただちに導くことができる。

通常、カット除去定理の成立する論理体系では、少なくとも一階述語論理までの体系であるならば、部分論理式性 (subformula property) も成り立つ。これは、証明図中に登場する全ての論理式が、帰結となる論理式の部分論理式になっているという性質である。証明にカット規則が用いられている場合は、その証明図からカットを除去した証明図が、この性質をみたしている。このことは、証明論に基づく意味論への幾つかのアプローチにおいて重要な役割を果たす。また、古典命題計算の体系では、部分論理式性は真偽を検証する必要のある論理式の数を有限個に限定し、このことから古典命題計算の決定可能性を導くこともできる。

カット除去は、クレイグの補間定理を証明する際に強力な道具となる。Prolog というプログラミング言語を考案する元となった導出に基づいた証明探索手法の可能性は、適切な論理体系におけるカット規則の許容性 (admissibility) に依存している。カリー・ハワード同型対応を使った高階ラムダ計算に基づく証明体系では、カット除去アルゴリズムは強い推論属性に対応している（全ての証明項には正規形があり、その正規形には任意の推論の完全なシーケンスから到達可能である）。

参考文献

Gentzen, Gerhard (1934). “Untersuchungen über das logische Schließen. I”. Mathematische Zeitschrift 39 (2): pp. 176-210.
Gentzen, Gerhard (1935). “Untersuchungen über das logische Schließen. II”. Mathematische Zeitschrift 39 (3): pp. 405-431.
Gentzen, Gerhard (1969). M. E. Szabo. ed. Collected Papers of Gerhard Gentzen. North-Holland. ISBN 0-7204-2254-X - 英訳の論文集。

外部リンク

Alex Sakharov. "Cut Elimination Theorem". mathworld.wolfram.com (英語).

この項目は、数理論理学に関連した書きかけの項目です。この項目を加筆・訂正などしてくださる協力者を求めています。