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.
