HOME

TheInfoList



OR:

The cut-elimination theorem (or Gentzen's ''Hauptsatz'') is the central result establishing the significance of the
sequent calculus In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautology i ...
. It was originally proved by
Gerhard Gentzen Gerhard Karl Erich Gentzen (24 November 1909 – 4 August 1945) was a German mathematician and logician. He made major contributions to the foundations of mathematics, proof theory, especially on natural deduction and sequent calculus. He died ...
in his landmark 1934 paper "Investigations in Logical Deduction" for the systems LJ and LK formalising
intuitionistic In the philosophy of mathematics, intuitionism, or neointuitionism (opposed to preintuitionism), is an approach where mathematics is considered to be purely the result of the constructive mental activity of humans rather than the discovery of f ...
and classical logic respectively. The cut-elimination theorem states that any judgement that possesses a proof in the sequent calculus making use of the cut rule also possesses a cut-free proof, that is, a proof that does not make use of the cut rule.


The cut rule

A
sequent In mathematical logic, a sequent is a very general kind of conditional assertion. : A_1,\,\dots,A_m \,\vdash\, B_1,\,\dots,B_n. A sequent may have any number ''m'' of condition formulas ''Ai'' (called " antecedents") and any number ''n'' of ass ...
is a logical expression relating multiple formulas, in the form , which is to be read as proves , and (as glossed by Gentzen) should be understood as equivalent to the truth-function "If (A_1 and A_2 and A_3 …) then (B_1 or B_2 or B_3 …)." Note that the left-hand side (LHS) is a conjunction (and) and the right-hand side (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 In traditional logic, a contradiction occurs when a proposition conflicts either with itself or established fact. It is often used as a tool to detect disingenuous beliefs and bias. Illustrating a general tendency in applied logic, Aristotle's ...
, whereas in LJ the RHS may only have one formula or none: 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 In logic, the law of excluded middle (or the principle of excluded middle) states that for every proposition, either this proposition or its negation is true. It is one of the so-called three laws of thought, along with the law of noncontradi ...
. 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 Jean-Yves Girard (; born 1947) is a French logician working in proof theory. He is the research director (emeritus) at the mathematical institute of the University of Aix-Marseille, at Luminy. Biography Jean-Yves Girard is an alumnus of the ...
'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 In mathematical logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard Gentzen) instead of an unconditional tautology. Each conditional tautology i ...
, and equivalent to a variety of rules in other proof theories, which, given
  1. \Gamma \vdash A,\Delta
and
  1. \Pi, A \vdash \Lambda
allows one to infer
  1. \Gamma, \Pi \vdash \Delta,\Lambda
That is, it "cuts" the occurrences of the formula A out of the inferential relation.


Cut elimination

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. For sequent calculi that have only one formula in the RHS, the "Cut" rule reads, given
  1. \Gamma \vdash A
and
  1. \Pi, A \vdash B
allows one to infer
  1. \Gamma, \Pi \vdash B
If we think of B as a theorem, then cut-elimination in this case simply says that a lemma A used to prove this theorem can be inlined. Whenever the theorem's proof mentions lemma A, we can substitute the occurrences for the proof of A. Consequently, the cut rule is admissible.


Consequences of the theorem

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 George Stephen Boolos (; 4 September 1940 – 27 May 1996) was an American philosopher and a mathematical logician who taught at the Massachusetts Institute of Technology. Life Boolos is of Greek-Jewish descent. He graduated with an A.B. i ...
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 In classical deductive logic, a consistent theory is one that does not lead to a logical contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent ...
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 Proof theory is a major branchAccording to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Barwise (1978) consists of four corresponding parts, ...
, an important property in several approaches to
proof-theoretic semantics Proof-theoretic semantics is an approach to the semantics of logic that attempts to locate the meaning of propositions and logical connectives not in terms of interpretations, as in Tarskian approaches to semantics, but in the role that the propo ...
. Cut elimination is one of the most powerful tools for proving interpolation theorems. The possibility of carrying out proof search based on
resolution Resolution(s) may refer to: Common meanings * Resolution (debate), the statement which is debated in policy debate * Resolution (law), a written motion adopted by a deliberative body * New Year's resolution, a commitment that an individual mak ...
, the essential insight leading to the
Prolog Prolog is a logic programming language associated with artificial intelligence and computational linguistics. Prolog has its roots in first-order logic, a formal logic, and unlike many other programming languages, Prolog is intended primarily ...
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 normalization property (every proof term reduces in a finite number of steps into a normal form).


See also

*
Deduction theorem In mathematical logic, a deduction theorem is a metatheorem that justifies doing conditional proofs—to prove an implication ''A'' → ''B'', assume ''A'' as an hypothesis and then proceed to derive ''B''—in systems that do not have an ...
*
Gentzen's consistency proof Gentzen's consistency proof is a result of proof theory in mathematical logic, published by Gerhard Gentzen in 1936. It shows that the Peano axioms of first-order arithmetic do not contain a contradiction (i.e. are "consistent"), as long as a cer ...
for
Peano's axioms In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly ...


Notes


References

* * *
Untersuchungen über das logische Schließen I

Untersuchungen über das logische Schließen II
* * *


External links

* * {{SpringerEOM , title=Sequent calculus , id=Sequent_calculus&oldid=11707 , author-last1=Dragalin , author-first1=A.G. Theorems in the foundations of mathematics Proof theory