切消定理

维基百科，自由的百科全书

切消定理是确立相继式演算重要性的主要结果。它最初由格哈德·根岑在他的划时代论文《逻辑演绎研究》对分别形式化直觉逻辑和经典逻辑的系统 LJ 和 LK 做的证明。切削定理声称在相继式演算中，拥有利用了切规则的证明的任何判断，也拥有无切证明，就是说，不利用切规则的证明。

相继式是与多个句子有关的逻辑表达式，形式为 " $A, B, C, \ldots \vdash N, O, P$ "，它可以被读做 "A, B, C, $\ldots$ 证明 N, O, P"，并且(按 Gentzen 的注释)应当被理解为等价于真值函数 "如果 (A & B & C $\ldots$ ) 那么 (N or O or P)"。注意 LHS(左手端)是合取(and)而 RHS(右手端)是析取(or)。LHS 可以有任意多个公式；在 LHS 为空的时候，RHS 是重言式。在 LK 中，RHS 也可以有任意数目的公式--如果没有，则 LHS 是个矛盾，而在 LJ 中，RHS 只能没有或有一个公式: 在右紧缩规则前面，允许 RHS 有多于一个公式，等价于容许排中律。注意，相继式演算是相当有表达力的框架，已经为直觉逻辑提议了允许 RHS 有多个公式的相继式演算，而来自 Jean-Yves Girard 的逻辑 LC 得到了 RHS 最多有一个公式的经典逻辑的更加自然的形式化；逻辑和结构规则的相互作用是它的关键。

"切"是在相继式演算的正规陈述中的一个规则，并等价于在其他证明论中的规则变体，给出

(1) $(A, B, \ldots) \vdash C$

和

(2) $C \vdash (D, E, \ldots)$

你可以推出

(3) $(A, B, \ldots) \vdash (D, E, \ldots)$

就是说，在推论关系中"切掉"公式 "C" 的出现。

切消定理声称(对于一个给定的系统) 使用切规则的任何相继式证明也可以不使用这个规则来证明。如果我们认为 $(D, E, \ldots)$ 是一个定理，则切消简单的声称用来证明这个定理的引理 $C$ 可以被内嵌(inline)。在这个定理的证明提及引理 $C$ 的时候，我们可以把它代换为 $C$ 的证明。因此，切规则是可接纳的。