切消定理

切规则把“先证引理，再用引理”的做法写成一条推理规则。中间公式 $A$ 可以表达一个便于复用的事实，即使它并不出现在最终结论中。切消定理保证：在 LK、LJ 中，借助这种中间公式能证明的相继式，也有一个直接围绕目标公式展开的证明。

消切时，先把切移过与它无关的推理步骤；当两侧都在处理切公式的主联结词时，就把大切拆成小切。例如，两侧分别构造和使用 $A\wedge B$ 时，可以把这次切化为关于 $A$、$B$ 的切，再继续降低切公式的复杂度。

这种展开会复制引理的证明。一个引理若被多次使用，复制还可能嵌套，因而切自由证明可能远比原证明长。切规则负责压缩，切自由形式则把公式来源限制得更明确，便于分析整个证明的结构。

设已证 $\mathrm{\Gamma }\Rightarrow A$ 和 $A\Rightarrow \mathrm{\Delta }$，切规则把它们接成 $\mathrm{\Gamma }\Rightarrow \mathrm{\Delta }$。消切把前一份证明展开到后一份使用 $A$ 的位置，最终保留相同的前提与结论，而消去对这个中间引理的依赖。

子公式性质给出纯逻辑 LK 的一致性证明。若空相继式 $\Rightarrow$ 可证，切消定理就给出它的切自由证明。由于结论没有公式，子公式性质要求整棵证明树都没有公式；但证明树必须从含有公式的逻辑公理开始，矛盾。因此空相继式不可证。对 Peano 算术理路皮亚诺算术Peano arithmetic · PA用一阶语言公理化自然数的零、后继、加法、乘法与归纳模式的形式理论。，还要处理归纳公理；Gentzen 的一致性证明使用沿 ${\epsilon }_0$ 的超限归纳，而 Gödel 第二不完备性定理理路Gödel 第二不完备定理Gödel's second incompleteness theorem足够强且一致的可有效公理化理论不能在自身内部证明自身的一致性。说明，一致的 PA 不能在自身内部完成标准的一致性证明。

消切的规模代价可能很大：存在带切证明，使任何对应的切自由证明都发生非初等的长度增长（Statman、Orevkov 的下界）。因此，证明搜索中保留受控的切，可以显著减少重复推导。

自然演绎理路自然演绎Natural deduction用引入规则与消去规则直接刻画逻辑联结词推理行为的证明演算。中的正规化处理相近的现象：刚用引入规则构造一个公式，随即又用消去规则拆开它，这段迂回可以约去。切消与正规化分别作用于相继式演算和自然演绎；在合适的证明翻译下，可以比较两种变换如何对应。

子公式性质限制了证明搜索需要考虑的公式来源。在命题演算及一些具有合适切自由系统的模态逻辑中，这有助于构造判定过程；一阶演算还要处理项代入，因此仅有子公式性质并不保证搜索会终止。Craig 插值也可沿切自由证明逐步构造，Maehara 方法就是这一思路的典型实现。

经由 Curry–Howard 对应理路Curry–Howard 对应Curry–Howard correspondence · Propositions as types把命题对应为类型、证明对应为程序、证明化简对应为程序求值。，把一个证明代入另一个证明中使用它的位置，对应程序中的代入与归约。相应的切消和正规化性质理路正规化性质Normalization property每个良构或良类型项能否经有限归约到正规形的性质。把证明变换与类型化程序的计算联系起来，为线性逻辑和证明搜索式编程提供工具。

证明复杂性则关注展开的成本：禁止或限制切规则后，最短证明会增长多少？这一问题把“复用引理能节省多少工作”变成可以定量研究的对象。