Editing Cut-elimination theorem

{{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>).

==The cut rule==
A [[sequent]] is a logical expression relating multiple formulas, in the form {{nowrap|"<math>A_1, A_2, A_3, \ldots \vdash B_1, B_2, B_3, \ldots</math>"}}, which is to be read as "If all of {{nowrap|<math>A_1, A_2, A_3, \ldots</math>}} hold, then at least one of {{nowrap|<math>B_1, B_2, B_3, \ldots</math>}} must hold", or (as Gentzen glossed): "If (<math>A_1</math> and <math>A_2</math> and <math>A_3</math> …) then (<math>B_1</math> or <math>B_2</math> or <math>B_3</math> …)."<ref>Wilfried Buchholz, [http://www.mathematik.uni-muenchen.de/~buchholz/articles/beweisth.ps Beweistheorie] (university lecture notes about cut-elimination, German, 2002-2003)</ref> Note that the left-hand side (LHS) is a conjunction (and) and the right-hand side (RHS)  is a disjunction (or).  

The LHS may have arbitrarily many or few formulae; when the LHS is empty, the RHS is a [[tautology (logic)|tautology]].  In LK, the RHS may also have any number of formulae—if it has none, the LHS is a [[contradiction]], whereas in LJ the RHS may only have one formula or none: here we see that allowing more than one formula in the RHS is equivalent, in the presence of the right contraction rule, to the admissibility of the [[law of the excluded middle]].  However, the sequent calculus is a fairly expressive framework, and there have been sequent calculi for intuitionistic logic proposed that allow many formulae in the RHS. From [[Jean-Yves Girard]]'s logic LC it is easy to obtain a rather natural formalisation of classical logic where the RHS contains at most one formula; it is the interplay of the logical and [[structural rule]]s that is the key here.

"Cut" is a [[rule of inference]] in the normal statement of the [[sequent calculus]], and equivalent to a variety of rules in other [[proof theory|proof theories]], which, given

<ol><li><math> \Gamma \vdash A,\Delta</math></li></ol>

and 

<ol start="2"><li><math> \Pi, A \vdash \Lambda</math></li></ol>

allows one to infer

<ol start="3"><li><math>\Gamma, \Pi \vdash \Delta,\Lambda</math></li></ol>

That is, it "cuts" the occurrences of the formula <math>A</math> out of the inferential relation. 
==Cut elimination==
The cut-elimination theorem states that (for a given system) any sequent provable using the rule Cut can be proved without use of this rule.

For sequent calculi that have only one formula in the RHS, the "Cut" rule reads, given

<ol><li><math> \Gamma \vdash A</math></li></ol>

and 

<ol start="2"><li><math> \Pi, A \vdash B</math></li></ol>

allows one to infer

<ol start="3"><li><math>\Gamma, \Pi \vdash B</math></li></ol>

If we think of <math>B</math> as a theorem, then cut-elimination in this case simply says that a lemma <math>A</math> used to prove this theorem can be inlined. Whenever the theorem's proof mentions [[lemma (mathematics)|lemma]] <math>A</math>, we can substitute the occurrences for the proof of <math>A</math>. Consequently, the cut rule is [[admissible rule|admissible]].

==Consequences of the theorem==

For systems formulated in the sequent calculus, [[Analytic proof#Structural proof theory|analytic proofs]] are those proofs that do not use Cut. Typically such a proof will be longer, of course, and not necessarily trivially so. In his essay "Don't Eliminate Cut!"<ref>{{harvnb|Boolos|1984|pp=373-378}}</ref> [[George Boolos]] demonstrated that there was a derivation that could be completed in a page using cut, but whose analytic proof could not be completed in the lifespan of the universe.

The theorem has many, rich consequences:
* A system is [[consistency proof|inconsistent]] if it admits a proof of the absurd. If the system has a cut elimination theorem, then if it has a proof of the absurd, or of the empty sequent,  it should also have a proof of the absurd (or   the empty sequent), without cuts. It is typically very easy  to check that there are no such proofs. Thus, once a system is shown to have a cut elimination theorem, it is normally immediate that the system is consistent.
* Normally also the system has, at least in first-order logic,  the [[subformula property]], an important property in several approaches to [[proof-theoretic semantics]].

Cut elimination is one of the most powerful tools for proving [[Craig interpolation|interpolation theorem]]s.  The possibility of carrying out proof search based on [[First-order resolution|resolution]], the essential insight leading to the [[Prolog]] programming language, depends upon the admissibility of Cut in the appropriate system.

For proof systems based on higher-order [[typed lambda calculus]] through a [[Curry&ndash;Howard isomorphism]], cut elimination algorithms correspond to the [[normalization property (abstract rewriting)|strong normalization property]] (every proof term reduces in a finite number of steps into a [[normal form (term rewriting)|normal form]]).

== See also ==
* [[Deduction theorem]]
* [[Gentzen's consistency proof]] for [[Peano's axioms]]

==Notes==
{{Reflist|2}}

== References ==
* {{Cite journal|last=Gentzen|first=Gerhard|author-link=Gerhard Gentzen|year=1935a|title=Untersuchungen über das logische Schließen. I|journal=[[Mathematische Zeitschrift]]|volume=39 | issue = 2 |pages=176–210|doi=10.1007/bf01201353 |s2cid=121546341|url=http://gdz.sub.uni-goettingen.de/dms/resolveppn/?PPN=GDZPPN002375508|archive-url=https://web.archive.org/web/20151224194624/http://gdz.sub.uni-goettingen.de/dms/load/img/?IDDOC=17178|archive-date=2015-12-24|url-status=live|url-access=subscription}}
:{{cite journal | first=Gerhard | last=Gentzen | author-mask=1| year=1964|orig-year=1935| title=Investigations into logical deduction | journal=[[American Philosophical Quarterly]] | volume=1 | number=4 | pages=249–287}}
* {{Cite journal|last=Gentzen|first=Gerhard|author-link=Gerhard Gentzen|year=1935b|title=Untersuchungen über das logische Schließen. II|journal=[[Mathematische Zeitschrift]]|volume=39 | issue = 3 |pages=405–431|doi=10.1007/bf01201363 |s2cid=186239837|url=http://gdz.sub.uni-goettingen.de/dms/resolveppn/?PPN=GDZPPN002375605|archive-url=https://archive.today/20120709063902/http://gdz.sub.uni-goettingen.de/dms/load/img/?IDDOC=17188|archive-date=2012-07-09|url-status=live|url-access=subscription}}
:{{cite journal | first=Gerhard | last=Gentzen | author-mask=1| year=1965|orig-year=1935| title=Investigations into logical deduction | journal=American Philosophical Quarterly | volume=2 | number=3 | pages=204–218}}
* {{cite book|last1=Curry|first1=Haskell Brooks|author1-link=Haskell Curry|title=Foundations of mathematical logic|orig-year=1963|year=1977|publisher=Dover Publications Inc.|location=New York|isbn=978-0-486-63462-3}}
* {{cite book|last1=Kleene|first1=Stephen Cole|author1-link=Stephen Cole Kleene|title=Introduction to metamathematics|orig-year=1952|year=2009|publisher=Ishi Press International|isbn=978-0-923891-57-2}} 
* {{cite journal | first=George | last=Boolos | author-link=George Boolos | title=Don't eliminate cut | journal=[[Journal of Philosophical Logic]] | volume=13 | number=4 | pages=373–378 | year=1984| doi=10.1007/BF00247711 }}

== External links ==
* {{MathWorld | urlname=CutEliminationTheorem | title=Cut Elimination Theorem | author=Alex Sakharov}}
* {{SpringerEOM
 |title=Sequent calculus
 |id=Sequent_calculus&oldid=11707
 |author-last1=Dragalin
 |author-first1=A.G.
}}

[[Category:Theorems in the foundations of mathematics]]
[[Category:Proof theory]]