查看“︁切消定理”︁的源代码

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

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

和

:（2）<math>C \vdash(D, E, \ldots)</math>

你可以推出

:（3）<math>(A, B, \ldots) \vdash(D, E, \ldots)</math>

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

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

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

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

== 引用 ==
* {{cite journal en| first=Gerhard | last=Gentzen | authorlink=Gerhard Gentzen | title=Untersuchungen über das logische Schließen | journal=Mathematische Zeitschrift | volume=39 | pages=405-431 | year=1934–1935}}

==参见==
*[[相继式演算]]
*[[归结原理]]
*[[假言三段论]]

[[Category:证明论|Q]]
[[Category:数学定理|Q]]