カット除去

カット除去は、補題の使用を形式化するカット規則が、任意のシーケント計算証明から除去でき、その証明が関連する論理式のみで構築された証明を残す、というゲンツェンの定理である。

Definition

カット除去とは、カット規則を用いる任意のシーケント計算導出が、それを用いない導出に変換できることを示す定理であり、構成的な手続きである。これにより、証明可能なすべてのシーケントは、最終シーケントの部分論理式のみが出現する証明を持つことになる。

Scope

このトピックでは、カット規則とそのシーケント計算における役割、カット除去手続きとその停止性、カットフリー証明の部分論理式特性、結果として生じる無矛盾性と決定可能性の帰結、および除去によって生じる証明サイズの限界について扱う。

Core questions

• カット規則は何を表現しており、その除去がなぜ重要なのか？
• カット除去手続きはどのように停止するのか？
• 部分論理式特性とは何か、そしてそれは証明探索に何を意味するのか？
• カットを除去する計算コストはどのくらいか？

Key theories

ゲンツェンの主定理 (Hauptsatz)

ゲンツェンの主定理は、シーケント計算においてカット規則が許容可能であることを述べており、したがってカットを用いる任意の証明は、同じ最終シーケントのカットフリー証明に変換できる。

部分論理式特性

カットフリー証明に出現するすべての論理式は、最終シーケントの部分論理式であり、これは証明の形状を制約し、決定手続きや無矛盾性論証の基礎となる。

カット除去による無矛盾性

空シーケントのカットフリー証明は不可能であるため、カット除去は、計算体系、ひいてはそれが形式化する理論が無矛盾であることの直接的な証明をもたらす。

Clinical relevance

カット除去は、広範な影響を持つ基礎的な結果である。それは、無矛盾性証明、自動定理証明やタブロー法に不可欠な部分論理式特性、補間定理、そして「プログラムとしての証明」対応を通じて型付きプログラムの正規化をもたらす。

History

ゲンツェンは1934年に一階述語論理に対してカット除去（彼の主定理、Hauptsatz）を証明し、この方法は構造的証明論の基礎となった。タイトとギラールは、この手法をより強力なシステムや高階論理に拡張し、カット除去における証明サイズの増大の限界は、それ自体が研究対象となった。

Key figures

• Gerhard Gentzen
• William Tait
• Jean-Yves Girard
• Gaisi Takeuti

Seminal works

• takeuti1987
• troelstra2000
• negri2001

Frequently asked questions

証明における「カット」とは何か？

カット規則は、補題を証明し、それを使用することを可能にする。ある論理式を確立する導出と、その論理式を前提として使用する別の導出から、それらを結合した結果を結論付ける。カット除去は、そのような中間補題が原理的に常に除去できることを示す。

カットを除去すると、なぜ証明が非常に長くなることがあるのか？

カットを除去するには、導出の大部分を複製する必要がある場合があり、これを繰り返すと、証明サイズが指数関数の塔（tower of exponentials）のように爆発的に増大する可能性がある。したがって、カットフリー証明は概念的にはより単純だが、カットを含む元の証明よりもはるかに大きくなることがある。