カット除去定理
「カット規則」とは、シークエント計算の一般的な推論規則であり、次のような形式で表現される。
(1) ( A , B , ... ) ⊢ C {\displaystyle (A,B,\ldots )\vdash C}
と
(2) C ⊢ ( D , E , ... ) {\displaystyle C\vdash (D,E,\ldots )}
とが、ともに成立しているとき、次を導出できる。
(3) ( A , B , ... ) ⊢ ( D , E , ... ) {\displaystyle (A,B,\ldots )\vdash (D,E,\ldots )}
すなわち、ここでは論理式 C が帰結からカットされている。