Editing Cut-elimination theorem (section)

==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]]).