TOPICS
Search

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  forall and  exists , and the only inference rules occurring in the derivation below the midsequent are the  forall and  exists rules and structural rules.


See also

Sequent Calculus

This entry contributed by Alex Sakharov (author's link)

Explore with Wolfram|Alpha

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.

Referenced on Wolfram|Alpha

Cut Elimination Theorem

Cite this as:

Sakharov, Alex. "Cut Elimination Theorem." From MathWorld--A Wolfram Web Resource, created by Eric W. Weisstein. https://mathworld.wolfram.com/CutEliminationTheorem.html

Subject classifications