切消定理

切规则是"引理"在证明系统中的化身：先证一个中间命题 $A$，再拿 $A$ 去推目标——这是数学家的日常工作方式。切消定理说，引理原则上是可以拆除的脚手架：任何用了引理的证明都能机械地展开为一个"就地取材"的直接证明，其中每一步只摆弄最终结论自带的材料。归纳证明的图像值得记住：一个关于复合公式 $A\wedge B$ 的切，可以下沉为分别关于 $A$、$B$ 的两个小切，如此层层剥解直到切消失。代价是尺寸——展开引理意味着把它的证明复制粘贴到每个使用点，可能反复嵌套。因此定理的价值不在"切无用"，恰在于存在性本身：切自由证明的结构受子公式性质严格约束，成了可以整体分析的对象，而这是带切证明做不到的。

最小的例子：由 $\mathrm{\Gamma }\Rightarrow A$ 与 $A\Rightarrow \mathrm{\Delta }$ 经切得 $\mathrm{\Gamma }\Rightarrow \mathrm{\Delta }$；切消变换把对 $A$ 的这次"转手"内联进两侧推导，最终版本里 $A$ 若非 $\mathrm{\Gamma },\mathrm{\Delta }$ 的子公式便不再现身。子公式性质立刻兑现为一致性证明：空相继式 $\Rightarrow$ 没有任何子公式，而每条非切规则都只能从含公式的前提推出含公式的结论，故切自由系统推不出 $\Rightarrow$，纯逻辑 LK 一致——这正是 Gentzen 把一致性问题转化为切消问题的原始动机；对 Peano 算术公理库皮亚诺算术Peano arithmetic · PA用一阶语言公理化自然数的零、后继、加法、乘法与归纳模式的形式理论。这样的理论，同一纲领需要沿序数 ${\epsilon }_0$ 的超限归纳，其必要性由 Gödel 第二不完备性定理公理库Gödel 第二不完备定理Gödel's second incompleteness theorem足够强且一致的可有效公理化理论不能在自身内部证明自身的一致性。反衬。

边界有三。其一，规模：带切证明可以比任何切自由证明短非初等倍（Statman、Orevkov 的下界），切是压缩证明的合法而高效的手段，实际证明搜索器保留受控的切正因于此。其二，适用范围：子公式性质只对"干净"的逻辑演算无条件成立，一旦加入等号或理论公理，切只能消到公理切为止。其三，概念区分：切消与自然演绎公理库自然演绎Natural deduction用引入规则与消去规则直接刻画逻辑联结词推理行为的证明演算。的正规化（消去"引入紧接消去"的迂回）在思想与技术上互相平行、可以互译，但作用于不同演算，是两条独立陈述的定理。

切消是证明论的结构性总开关。一致性之外，子公式性质使证明搜索空间变得可控，直接支撑可判定片段的判定过程（命题逻辑、若干模态逻辑的判定即由切自由搜索给出）与插值定理（Craig 插值可沿切自由证明归纳构造，Maehara 方法）。经由 Curry–Howard 对应公理库Curry–Howard 对应Curry–Howard correspondence · Propositions as types把命题对应为类型、证明对应为程序、证明化简对应为程序求值。，切对应函数应用中的"可约式"，切消过程对应程序的归约求值，切消定理的终止性对应类型化程序的正规化性质公理库正规化性质Normalization property每个良构或良类型项能否经有限归约到正规形的性质。——这条桥梁把证明变换与程序语义连成一体，是线性逻辑、证明搜索式编程语言设计的出发点。证明复杂性理论则反向利用切：研究禁止或限制切规则后证明长度的爆炸幅度，量化"引理的价值"。