カットルール

数理論理学において、カットルールはシーケント計算の推論規則である。これは古典的なモーダス・ポネンス推論規則の一般化である。その意味は、ある証明では結論として式Aが現れ、別の証明では仮説として現れる場合、式Aが現れない別の証明を演繹できるということである。これは、すべての人間は死ぬ運命にある、ソクラテスは人間である、という表現から人間の例を除去してソクラテスは死ぬ運命にある、という表現を演繹するなど、モーダス・ポネンスの事例に当てはまる。

これは通常、逐次計算記法による正式な記法で次のように記述されます。

${\displaystyle {\begin{array}{c}\Gamma \vdash A,\Delta \quad \Gamma ',A\vdash \Delta '\\\hline \Gamma ,\Gamma '\vdash \Delta ,\Delta '\end{array}}}$カット^[1]

カット規則は、重要な定理であるカット除去定理の対象です。カット規則を利用してシークエント計算で証明されるシークエントは、カットフリーの証明、つまりカット規則を利用しない証明も持つことを述べています。