形式陈述

Gentzen 切消定理（Hauptsatz）断言：在标准 LK 或 LJ 中，若相继式可证明，则它存在一个不使用切规则的证明。证明按切公式复杂度和两侧推导高度作良基归纳，通过局部变换把切向上移动；当切公式刚由两侧逻辑规则引入时，将一个复杂切化为若干更简单的切。对纯逻辑演算，切自由证明中的每个公式通常都是末相继式公式的子公式，从而得到子公式性质。含等号、理论公理或额外规则时需采用相应扩展版本，子公式性质也可能只在广义意义下成立。

直觉

切规则允许先发明一个中间引理再把它消去。切消说明任何成功证明都能展开成只处理最终命题内部材料的直接证明，尽管展开后可能非常长。

例子与边界

从 $\Gamma\Rightarrow A$$\mathrm{\Gamma }\Rightarrow A$ 与 $A\Rightarrow\Delta$$A\Rightarrow \mathrm{\Delta }$ 经切得到 $\Gamma\Rightarrow\Delta$$\mathrm{\Gamma }\Rightarrow \mathrm{\Delta }$；切消变换会把对 $A$$A$ 的使用嵌入两侧推导。它不宣称切规则“无用”：带切证明常远短于切自由证明，切消甚至可能造成非初等规模膨胀。子公式性质可用于证明某些空相继式不可导，从而给出一致性，但只有在演算的初始相继式和附加公理也受控制时才可直接使用。切消与自然演绎规范化紧密对应，却不是同一个语法定理。

推论与应用

切消给出证明系统一致性、可判定片段和插值定理的证明工具，并把证明正规化与程序化归约联系起来。Proof complexity 则研究消除中间引理所产生的长度代价。

参考资料

• A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory, 2nd ed., Cambridge University Press, 2000，Chs. 4–6, Hauptsatz and reductions of cut rank。
• Heinz-Dieter Ebbinghaus, Jörg Flum, and Wolfgang Thomas, Mathematical Logic, 2nd ed., Springer, 1994，Part A, cut-free calculi and proof-theoretic consequences。