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 tautolog ...

. It was originally proved by Gerhard Gentzen in part I of his landmark 1935 paper "Investigations in Logical Deduction" for the systems LJ and LK formalising intuitionistic and

classical logic Classical logic (or standard logic) or Frege–Russell logic is the intensively studied and most widely used class of deductive logic. Classical logic has had much influence on analytic philosophy. Characteristics Each logical system in this c ...

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 Natural Deduction version of cut-elimination, known as ''normalization theorem'', has been first proved for a variety of logics by

Dag Prawitz Dag Prawitz (born 1936, Stockholm) is a Swedish philosopher and logician. He is best known for his work on proof theory and the foundations of natural deduction, and for his contributions to proof-theoretic semantics. Prawitz is a member of the ...

in 1965 (a similar but less general proof was given the same year by Andrès Raggio).

The cut rule

A sequent is a logical expression relating multiple formulas, in the form , which is to be read as "If all of hold, then at least one of must hold", or (as Gentzen glossed): "If (

A_1

and

A_2

and

A_3

…) then (

B_1

B_2

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 involves a proposition conflicting 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. 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 of inference Rules of inference are ways of deriving conclusions from premises. They are integral parts of formal logic, serving as norms of the Logical form, logical structure of Validity (logic), valid arguments. If an argument with true premises follows a ...

in the normal statement of the

, and equivalent to a variety of rules in other proof theories, which, given

$\Gamma \vdash A,\Delta$

and

$\Pi, A \vdash \Lambda$

allows one to infer

$\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

$\Gamma \vdash A$

and

$\Pi, A \vdash B$

allows one to infer

$\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 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 Prolog is a logic programming language that has its origins in artificial intelligence, automated theorem proving, and computational linguistics. Prolog has its roots in first-order logic, a formal logic. Unlike many other programming language ...

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).

Notes

References

* * * * : * : * * *

External links