切消定理

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

相继式是与多个句子有关的逻辑表达式,形式为"",它可以被读做"A, B, C, 证明N, O, P",并且(按Gentzen的注释)应当被理解为等价于真值函数"如果(A & B & C )那么(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)

(2)

你可以推出

(3)

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

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

对于用相继式公式化的系统,分析性证明是不使用切规则的证明。这种证明典型的会很长,当然没有必要这么做。在散文《不要消除切呀!》中,George Boolos展示了可以使用切在一页中完成的推导,而它的分析性证明要耗尽宇宙的寿命来完成。

这个定理有很多丰富的推论。一旦一个系统被证明有切消定理,这个系统通常立即就是一致的。这个系统通常也有子公式性质,这是达成证明论语义的重要性质。切削是证明插值定理的最强力工具。基于归结原理的完成证明查找的可能性,导致Prolog编程语言的本质洞察,依赖于在适当的系统中接纳切规则。

引用

  • Gentzen, Gerhard. Untersuchungen über das logische Schließen. Mathematische Zeitschrift. 1934–1935, 39: 405–431. 

参见