カット除去定理

カット除去定理の最新ニュースをまとめて検索！

カット除去定理（カットじょきょていり、英: Cut-elimination theorem）は、シークエント計算の重要性を構成する主要な結果の1つである。ゲルハルト・ゲンツェンが1934年に書いた記念碑的論文 "Investigations in Logical Deduction" で、直観論理や古典論理学の論理体系を形式化した LJ や LK で最初に証明された。カット除去定理は、シークエント計算でカット規則を使った証明の存在する論理的主張には、必ずカット規則を使わない証明も存在することを示したものである。

[編集] シークエント

シークエントは複数の文からなる論理表現であり、" $A, B, C, \ldots \vdash N, O, P$ " という形式である。これは「A, B, C, $\ldots$ により、N, O, P が証明される」という意味であり、"If (A and B and C $\ldots$ ) then (N or O or P)" という真理値関数と等価と理解できる。ここで、左辺が論理積で、右辺が論理和であることに注意されたい。左辺は任意個の論理式からなり、左辺が空なら、右辺はトートロジーを表す。LK では、右辺は任意個の論理式からなり、右辺が空なら、左辺は矛盾を示している。一方 LJ では右辺は高々1つの論理式からなる。右辺に複数の論理式が存在可能であることと、右縮約規則があるときに排中律が成り立つことは等価である。ただし、シークエント計算は非常に表現能力が高く、右辺に多数の論理式のある直観論理のシークエント計算も存在する。Jean-Yves Girard の論理体系 LC によれば、右辺に高々1つの論理式しか持たない古典論理の自然な定式化も容易に得られる。ここで鍵となるのは、論理規則と構造規則の相互作用である。

[編集] カット規則

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

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

と

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

が成り立つとき、次が導かれる。

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

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

[編集] カット除去定理

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

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

この定理から様々なものが派生する。

不合理な証明を認める論理体系は一貫性に欠ける。ある論理体系でカット除去定理が成り立つとき、その体系で不合理な証明が可能であるとすると、その証明をカット規則を用いずに行うこともできるはずである。そのような証明が存在しないことは一般に容易にチェックできる。従って、カット除去定理のある論理体系は一貫性も備えている。
一般に論理体系は部分論理式属性 (subformula property) も持つ。これは証明理論における意味論によっては、重要な属性とされる。

カット除去は、クレイグの補間定理を証明する際に強力な道具となる。Prolog というプログラミング言語を考案する元となった導出に基づいた証明探索手法の可能性は、適切な論理体系におけるカット規則の許容性 (admissibility) に依存している。

カリー・ハワード同型対応を使った高階ラムダ計算に基づく証明体系では、カット除去アルゴリズムは強い推論属性に対応している（全ての証明項には正規形があり、その正規形には任意の推論の完全なシーケンスから到達可能である）。

[編集] 参考文献

Gentzen, Gerhard (1934年-1935年). “Untersuchungen über das logische Schließen”. Mathematische Zeitschrift 39: 405-431.

[編集] 外部リンク

Alex Sakharov. Cut Elimination Theorem, MathWorld.（英語）

この項目「カット除去定理」は、数学に関連した書きかけの項目です。加筆・訂正などをして下さる協力者を求めています。（P:数学／PJ:数学）

フリー百科事典『ウィキペディア（Wikipedia）』 Text is available under GNU Free Documentation License.

最終更新 2009年10月1日 (木) 07:59 （日時は個人設定で未設定ならばUTC）。
【カット除去定理】変更履歴