Cut-elimination theorem

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" for the systems LJ and LK formalising intuitionistic and classical logic respectively. The cut-elimination theorem states that any sequent 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. The natural deduction version of cut-elimination, known as the normalization theorem, was first proved for a variety of logics by Dag Prawitz in 1965 (a similar but less general proof was given the same year by Andrès Raggio).

There are many different possible sequent calculuses for many logics, and consequently there are many different cut-elimination theorems. Indeed, cut-elimination is such an important genre of theorems in logic, that logicians speak of "this logic has cut-elimination" as a way to say that this logic has a desirable property. Conversely, if a formalism or a logic does not have cut-elimination, that is usually considered a point against it, and would motivate research into finding a new formalism, or a modification of the logic, such that cut-elimination is true, or an analog of cut-elimination is true.