Cut-elimination theorem

From open-encyclopedia.com - the free encyclopedia.

The Cut-elimination theorem is the central result establishing the significance of the sequent calculus. It was originally proved by Gerhard Gentzen in his landmark paper "Investigations in Logical Deduction" 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 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 \rightarrow 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 & B & 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. Likewise the RHS may have any number of formulae--if it has none, the LHS is a contradiction--except under intuitionistic logic, in which case it may have only none or one formula. (This is on the grounds that intuitionism does not allow the proving of disjunctions. Intuitionism's rejection of the law of double negation falls out as a consequence of this with appropriate rules of derivation, so in general this change is sufficient to convert from classical to intuitionistic sequent calculi.)

"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) \rightarrow C<math>

and

(2) <math>C \rightarrow (D, E, \ldots)<math>

Lets one infer

(3) <math>(A, B, \ldots) \rightarrow (D, E, \ldots)<math>

That is, it "cuts" the occurrence 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. Consequently, the cut rule is admissible. For systems formulated in the sequent calculus, analytic proofs are those proofs that do not use cut.

As a consequence, any formula that can be proved at all can be proved without using any formulae that are not subformulae of the final one; in a manner of speaking, nothing outside the formula itself goes into the proof of it.

The theorem has many, rich consequences. 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 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.