The cut-elimination theorem (or Gentzen's Hauptsatz) is the central result establishing the significance of the sequent calculus.
It was originally proved by Gerhard Gentzen in part I of his landmark 1935 paper "Investigations in Logical Deduction"[1] for the systems LJ and LK formalising intuitionistic 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.
[2][3] A sequent is a logical expression relating multiple formulas, in the form "
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 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 in the normal statement of the sequent calculus, and equivalent to a variety of rules in other proof theories, which, given and allows one to infer That is, it "cuts" the occurrences of the formula
For sequent calculi that have only one formula in the RHS, the "Cut" rule reads, given and allows one to infer If we think of
as a theorem, then cut-elimination in this case simply says that a lemma
Typically such a proof will be longer, of course, and not necessarily trivially so.
"[5] 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: 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 normalization property (every proof term reduces in a finite number of steps into a normal form).