Editing Cut-elimination theorem (section)

{{Short description|Theorem in formal logic}}
{{use dmy dates|date=January 2025}}
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"{{sfn|Gentzen|1935a|pages=196ff|loc="Beweis des Hauptsatzes"}} for the systems [[system LJ|LJ]] and [[system LK|LK]] formalising [[intuitionistic logic|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.<ref>{{harvnb|Curry|1977|pp=208–213}}, gives a 5-page proof of the elimination theorem. See also pages 188, 250.</ref><ref>{{harvnb|Kleene|2009|pp=453}}, gives a very brief proof of the cut-elimination theorem.</ref> 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<ref>D. Prawitz, ''Natural Deduction. A proof theoretical study'', Almqvist & Wiskell, Stockholm, 1965</ref> (a similar but less general proof was given the same year by Andrès Raggio<ref> A. Raggio, ''Gentzen’s Hauptsatz for the systems NI and NK''. Logique et Analyse, 8(30), 91–100.</ref>).