View source for Criterion-referenced test

{{Expert-subject|Mathematics|date=November 2008}}

'''Gentzen's consistency proof''' is a result of [[proof theory]] in [[mathematical logic]]. It "reduces" the consistency of a simplified part of mathematics, not to something that could be proved in that same simplified part of mathematics (which would contradict the basic results of [[Kurt Gödel]]), but rather to a simpler logical principle.

==Gentzen's theorem==
In 1936 [[Gerhard Gentzen]] proved the consistency of [[first-order arithmetic]] using combinatorial methods.  Gentzen's proof shows much more than merely that first-order arithmetic is [[consistent]]. Gentzen showed that the consistency of first-order arithmetic is provable, over the base theory of [[primitive recursive arithmetic]] with the additional principle of quantifier-free [[transfinite induction]] up to the [[ordinal number|ordinal]] [[epsilon zero|ε<sub>0</sub>]].  Informally, this additional principle means that there is a [[well-ordering]] on the set of finite rooted [[tree (mathematics)|tree]]s.

The principle of quantifier-free transfinite induction up to ε<sub>0</sub> says that for any formula A(x) with no bound variables transfinite induction up to ε<sub>0</sub> holds. ε<sub>0</sub> is the first ordinal <math>\alpha</math>, such that <math>\omega^\alpha = \alpha</math>, i.e. the limit of the sequence:
:<math>\omega,\ \omega^\omega,\ \omega^{\omega^\omega},\ \ldots</math>
To express ordinals in the language of arithmetic an [[ordinal notation]] is needed, i.e. a way to assign natural numbers to ordinals less than ε<sub>0</sub>. This can be done in various ways, one example provided by Cantor's normal form theorem. That transfinite induction holds for a formula A(x) means that A does not define an infinite descending sequence of ordinals smaller than ε<sub>0</sub> (in which case ε<sub>0</sub> would not be well-ordered). Gentzen assigned ordinals smaller than ε<sub>0</sub> to proofs in first-order arithmetic and showed that if there is a proof of contradiction, then there is an infinite descending sequence of ordinals < ε<sub>0</sub> produced by a [[primitive recursive]] operation on proofs corresponding to a quantifier-free formula.

==Relation to Gödel's theorem==
Gentzen's proof also highlights one commonly missed aspect of [[Gödel's second incompleteness theorem]]. It is sometimes claimed that the consistency of a theory can only be proved in a stronger theory. The theory obtained by adding quantifier-free transfinite induction to primitive recursive arithmetic proves the consistency of first-order arithmetic but is not stronger than first-order arithmetic. For example, it does not prove ordinary mathematical induction for all formulae, while first-order arithmetic does (it has this as an axiom schema). The resulting theory is not weaker than first-order arithmetic either, since it can prove a number-theoretical fact - the consistency of first-order arithmetic - that first-order arithmetic cannot. The two theories are simply incomparable.

Gentzen's proof is the first example of what is called proof-theoretical [[ordinal analysis]]. In ordinal analysis one gauges the strength of theories by measuring how large the (constructive) ordinals are that can be proven to be well-ordered, or equivalently for how large a (constructive) ordinal can transfinite induction be proven. A constructive ordinal is the order type of a [[recursive set|recursive]] well-ordering of natural numbers.

[[Laurence Kirby]] and [[Jeff Paris]] proved in 1982 that [[Goodstein's theorem]] cannot be proven in Peano arithmetic based on Gentzen's theorem.

==References==
*{{Citation|last1=Gentzen|doi=10.1007/BF01565428|first1=Gerhard|author-link=Gerhard Gentzen|title=Die Widerspruchsfreiheit der reinen Zahlentheorie|journal=Mathematische Annalen|volume=112|year=1936|publisher=|pages=493–565|url=http://gdz.sub.uni-goettingen.de/dms/resolveppn/?PPN=GDZPPN002278391}} - Translated as 'The consistency of arithmetic', in {{Harv|Gentzen|Szabo|1969}}.
*{{Citation|last1=Gentzen|first1=Gerhard|author-link=Gerhard Gentzen|title=Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie|journal=Forschungen zur Logik und zur Grundlegung der exakten Wissenschaften|volume=4|year=1938|publisher=|pages=19–44}} - Translated as 'New version of the consistency proof for elementary number theory', in {{Harv|Gentzen|Szabo|1969}}.
*{{Citation|last=Gentzen|first=Gerhard|editor-last=M. E.|editor-first=Szabo|editor-link=M. E. Szabo|year=1969|title=Collected Papers of Gerhard Gentzen|publisher=North-Holland|location=Amsterdam|edition=Hardcover|series=Studies in logic and the foundations of mathematics|isbn=0-7204-2254-X|ref={{Harvid|Gentzen|Szabo|1969}}}} - an English translation of papers.
*{{Citation|last=Gödel|first=K.|author-link=Kurt Gödel|editor1-last=Feferman|editor1-first=Solomon|editor1-link=Solomon Feferman|origyear=1938|year=2001|title=Kurt Gödel: Collected Works|chapter=Lecture at Zilsel’s|publisher=Oxford University Press Inc.|pages=87–113|edition=Paperback|volume=vol.III Unpublished Essays and Lectures|isbn=0-19-514722-7|ref={{Harvid|Gödel|Feferman et al.|2001}}}}
*{{Citation|last=Jervell|first=Herman Ruge|author-link=Herman Ruge Jervell|year=1999|title=A course in proof theory|edition=textbook draft|url=http://folk.uio.no/herman/bevisteori.ps}}
*{{Citation|last1=Kirby|first1=L.|author1-link=Laurie Kirby|last2=Paris|first2=J.|author2-link=Jeff Paris|year=1982|title=Accessible independence results for Peano arithmetic|journal=[[Bull. London Math. Soc.]]|publisher=[[London Mathematical Society|LMS]]|pages=285–293|volume=14|url=http://blms.oxfordjournals.org/content/14/4/285.full.pdf|format=PDF}}
*{{Citation|last=Tait|first=W. W.|author-link=William W. Tait|year=2005|title=Gödel's reformulation of Gentzen's first consistency proof for arithmetic: the no-counterexample interpretation|journal=The Bulletin of Symbolic Logic|volume=11|issue=2|publisher=[[Association for Symbolic Logic|ASL]]|pages=225–238|url=http://home.uchicago.edu/~wwtx/GoedelandNCInew1.pdf|format=PDF|issn=1079-8986}}

[[Category:Metatheorems]]
[[Category:Proof theory]]