カット除去定理

カット除去定理とは

カット除去定理は、数理論理学、特にシークエント計算において、中心的な役割を果たす重要な定理です。この定理は、ある論理体系において、カット規則と呼ばれる特定の推論規則を用いて証明できる命題であれば、その規則を用いずに証明できることを主張します。つまり、カット規則は、証明をより効率的に記述するための便宜的なものであり、論理的な本質には影響を与えないということです。

シークエントとは

シークエントは、複数の文からなる論理表現で、次のような形式で記述されます。


A₁, A₂, ..., Aₙ ⊢ B₁, B₂, ..., Bₘ


この形式は、直感的には「A₁, A₂, ..., Aₙ が真であるならば、B₁, B₂, ..., Bₘ のうち少なくとも一つは真である」という意味を表します。ここで、左辺（A₁, A₂, ..., Aₙ）は前提となる論理式の集合で、右辺（B₁, B₂, ..., Bₘ）は結論となる論理式の集合です。古典論理（LK）では右辺に複数の論理式を置くことができますが、直観論理（LJ）では右辺に置ける論理式は一つまでです。

カット規則

カット規則は、シークエント計算における推論規則の一つで、次のように表現されます。


Γ ⊢ A, Δ Λ, A ⊢ Θ
-----
Γ, Λ ⊢ Δ, Θ


ここで、Aはカットされる論理式と呼ばれ、この規則は、Aが結論に含まれるシークエントと、Aが前提に含まれるシークエントから、Aを取り除いた新しいシークエントを導く操作です。カット規則は、証明の中で補題を使うような操作に対応し、複雑な証明を簡潔に記述するのに役立ちます。

カット除去定理の重要性

カット除去定理は、以下のような点で重要な意味を持ちます。

1. 論理体系の無矛盾性：カット除去定理が成立する論理体系では、矛盾した命題を証明することができません。なぜなら、もし矛盾した命題が証明可能であれば、カット規則を使わない証明も存在するはずですが、そのような証明は構成できないからです。したがって、カット除去定理は、論理体系の無矛盾性を示す強力な根拠となります。
2. 部分論理式性：カット除去定理が成立する論理体系では、証明図中に現れる全ての論理式が、結論として導きたい論理式の部分論理式となるという性質（部分論理式性）が成り立ちます。この性質は、証明論に基づく意味論や、古典命題計算の決定可能性を導く上で重要な役割を果たします。
3. 証明探索の効率化：カット除去定理は、カット規則を使わない証明が存在することを示唆するため、証明探索アルゴリズムの開発に貢献します。カット規則を使わない証明は、一般的に長くなる傾向にありますが、その構造がより明確であるため、自動的な証明探索に適しています。

カット除去定理の応用

カット除去定理は、様々な分野で応用されています。

クレイグの補間定理の証明：カット除去定理は、クレイグの補間定理を証明するための強力なツールとして利用されます。
プログラミング言語Prologの基礎：Prologの導出に基づいた証明探索手法は、適切な論理体系におけるカット規則の許容性に依存しています。
高階ラムダ計算：カリー・ハワード同型対応に基づく高階ラムダ計算では、カット除去アルゴリズムは強い推論属性に対応し、全ての証明項が正規形を持つことを保証します。

まとめ

カット除去定理は、シークエント計算における重要な定理であり、証明の構造や論理体系の性質を理解する上で不可欠な概念です。この定理は、カット規則を使わずに証明が可能であることを示し、論理体系の無矛盾性、部分論理式性、効率的な証明探索などに貢献します。また、様々な分野における応用例も多数存在し、その重要性はますます高まっています。

参考文献

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.

外部リンク

* Cut Elimination Theorem - Wolfram MathWorld

もう一度検索