- Gentzen's consistency proof
**Gentzen's theorem**In 1936

Gerhard Gentzen proved the consistency offirst-order arithmetic using combinatorial methods. Gentzen's proof shows much more than merely that first-order arithmetic isconsistent . Gentzen showed that the consistency of first-order arithmetic is provable, over the weaker base theory ofprimitive recursive arithmetic with the additional principle of quantifier freetransfinite induction up to theordinal ε_{0}(epsilon nought ).The principle of quantifier free transfinite induction up to ε

_{0}says that for any formula A(x) with no bound variables transfinite induction up to ε_{0}holds. ε_{0}is the first ordinal $alpha$, such that $omega^alpha\; =\; alpha$, i.e. the limit of the sequence::$omega,\; omega^omega,\; omega^\{omega^omega\},\; ldots$To express ordinals in the language of arithmetic a notation is needed, i.e. a way to assign natural numbers to ordinals less than ε_{0}. 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 ε_{0}(in which case ε_{0}would not be well-ordered). Gentzen assigned ordinals smaller than ε_{0}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 < ε_{0}produced by aprimitive recursive operation on proofs corresponding to a quantifier free formula.Gentzen's proof also highlights one commonly missed aspect of

Gödel's second incompleteness theorem . It's 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 doesn't 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 well-ordering of natural numbers.Laurence Kirby andJeff Paris proved in 1982 thatGoodstein's theorem leads to Gentzen's theorem, i.e. it can substitute for induction up to ε_{0}.**References*** G. Gentzen, 1936. 'Die Widerspruchfreiheit der reinen Zahlentheorie'. Mathematische Annalen, 112:493–565. Translated as 'The consistency of arithmetic', in (M. E. Szabo 1969).

* G. Gentzen, 1938. 'Neue Fassung des Widerspruchsfreiheitsbeweises fuer die reine Zahlentheorie'. Translated as 'New version of the consistency proof for elementary number theory', in (M. E. Szabo 1969).

* K. Gödel, 1938. Lecture at Zilsel’s, In Feferman et al. "Kurt Gödel: Collected Works", Vol III, pp. 87–113.

* M. E. Szabo (ed.), 1969. "'The collected works of Gerhard Gentzen". North-Holland, Amsterdam.

* W. W. Tait, 2005. [*http://home.uchicago.edu/~wwtx/GoedelandNCInew1.pdf Gödel's reformulation of Gentzen's first consistency proof for arithmetic: the no-counterexample interpretation*] . The Bulletin of Symbolic Logic 11(2):225-238.

* Kirby, L. and Paris, J., "Accessible independence results for Peano arithmetic", Bull. London. Math. Soc., 14 (1982), 285-93.

*Wikimedia Foundation.
2010.*