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 judgement 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 normalization theorem, has been 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).