Cut Elimination Theorem

The cut elimination theorem, also called the "Hauptsatz" (Gentzen 1969), states that every sequent calculus derivation can be transformed into another derivation with the same endsequent (bottom sequent) and in which the cut rule does not occur.

All derivations without cuts posses the sub-formula property that all formulas occurring in a derivation are sub-formulas of the formulas from the endsequent.

A sharpened form of theorem applies to the classical variant of sequent calculus. This form states that any derivation can be transformed to another derivation with the same endsequent and having the following properties.

1. It has no cuts.

2. It contains a so-called midsequent whose derivation contains no  and , and the only inference rules occurring in the derivation below the midsequent are the  and  rules and structural rules.

REFERENCES

Gentzen, G. The Collected Papers of Gerhard Gentzen (Ed. M. E. Szabo). Amsterdam, Netherlands: North-Holland, 1969.

Kleene, S. C. Introduction to Metamathematics. Princeton, NJ: Van Nostrand, 1964.