| dbpprop:abstract
|
- The cut-elimination theorem is the central result establishing the significance of the sequent calculus. It was originally proved by Gerhard Gentzen 1934 in his landmark paper "Investigations in Logical Deduction" for the systems LJ and LK formalising intuitionistic and classical logic respectively. The cut-elimination theorem (Hauptsatz) states that any judgement that possesses a proof in the sequent calculus that makes use of the cut rule also possesses a cut-free proof, that is, a proof that does not make use of the cut rule. A sequent is a logical expression relating multiple sentences, in the form "<math>A, B, C, \ldots \vdash N, O, P</math>", which is to be read as "A, B, C, <math>\ldots</math> proves N, O, P", and (as glossed by Gentzen) should be understood as equivalent to the truth-function "If (A and B and C <math>\ldots</math>) then (N or O or P). " Note that the left-hand side (LHS) is a conjunction (and) and the RHS is a disjunction (or). The LHS may have arbitrarily many or few formulae; when the LHS is empty, the RHS is a tautology. In LK, the RHS may also have any number of formulae—if it has none, the LHS is a contradiction, whereas in LJ the RHS may have only none or one formula: here we see that allowing more than one formula in the RHS is equivalent, in the presence of the right contraction rule, to the admissibility of the law of the excluded middle. However, the sequent calculus is a fairly expressive framework, and there have been sequent calculi for intuitionistic logic proposed that allow many formulae in the RHS. From Jean-Yves Girard's logic LC it is easy to obtain a rather natural formalisation of classical logic where the RHS contains at most one formula; it is the interplay of the logical and structural rules that is the key here. "Cut" is a rule in the normal statement of the sequent calculus, and equivalent to a variety of rules in other proof theories, which, given (1) <math> (A, B, \ldots) \vdash C</math> and (2) <math>C \vdash (D, E, \ldots)</math> allows one to infer (3) <math>(A, B, \ldots) \vdash (D, E, \ldots). </math> That is, it "cuts" the occurrences of the formula "C" out of the inferential relation. The cut-elimination theorem states that (for a given system) any sequent provable using the rule Cut can be proved without use of this rule. If we think of <math>(D, E, \ldots)</math> as a theorem, then cut-elimination simply says that a lemma <math>C</math> used to prove this theorem can be inlined. Whenever the theorem's proof mentions lemma <math>C</math>, we can substitute the occurrences for the proof of <math>C</math>. Consequently, the cut rule is admissible. For systems formulated in the sequent calculus, analytic proofs are those proofs that do not use Cut. Typically such a proof will be longer, of course, and not necessarily trivially so. In his essay "Don't Eliminate Cut!" George Boolos demonstrated that there was a derivation that could be completed in a page using cut, but whose analytic proof could not be completed in the lifespan of the universe. The theorem has many, rich consequences: A system is inconsistent if it admits a proof of the absurd. If the system has a cut elimination theorem, then if it has a proof of the absurd, or of the empty sequent, it should also have a proof of the absurd (or the empty sequent), without cuts. It is typically very easy to check that there are no such proofs. Thus, once a system is shown to have a cut elimination theorem, it is normally immediate that the system is consistent. Normally also the system has, at least in first order logic, the subformula property, an important property in several approaches to proof-theoretic semantics. Cut elimination is one of the most powerful tools for proving interpolation theorems. The possibility of carrying out proof search based on resolution, the essential insight leading to the Prolog programming language, depends upon the admissibility of Cut in the appropriate system. For proof systems based on higher-order typed lambda calculus through a Curry-Howard isomorphism, cut elimination algorithms correspond to the strong reduction property (every proof term has a normal form and this normal form is reached by any complete sequence of reductions).
- Der Gentzensche Hauptsatz oder Schnittsatz ist ein Satz der mathematischen Logik, der besagt, dass die Schnittregel in Gentzentypkalkülen gültig ist. Er ist nach Gerhard Gentzen benannt, der ihn 1934 aufstellte und bewies.
- カット除去定理（英: Cut-elimination theorem）とは、シークエント計算の重要性を構成する主要な結果の1つである。ゲルハルト・ゲンツェンが1934年に書いた記念碑的論文 "Investigations in Logical Deduction" で、直観論理や古典論理学の論理体系を形式化した LJ や LK で最初に証明された。カット除去定理は、シークエント計算でカット規則を使った証明の存在する論理的主張には、必ずカット規則を使わない証明も存在することを示したものである。
- 切消定理是确立相继式演算重要性的主要结果。它最初由格哈德·根岑在他的划时代论文《逻辑演绎研究》对分别形式化直觉逻辑和经典逻辑的系统 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 编程语言的本质洞察，依赖于在适当的系统中接纳切规则。
|
![[RDF Data]](/statics/sw-cube.png)
