Gentzen's consistency proof

Gentzen's consistency proof

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 weaker base theory of primitive recursive arithmetic with the additional principle of quantifier free transfinite induction up to the ordinal ε0 (epsilon nought).

The principle of quantifier free transfinite induction up to &epsilon;0 says that for any formula A(x) with no bound variables transfinite induction up to &epsilon;0 holds. &epsilon;0 is the first ordinal alpha, such that omega^alpha = alpha, i.e. the limit of the sequence::omega, omega^omega, omega^{omega^omega}, ldotsTo express ordinals in the language of arithmetic a notation is needed, i.e. a way to assign natural numbers to ordinals less than &epsilon;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 &epsilon;0 (in which case &epsilon;0 would not be well-ordered). Gentzen assigned ordinals smaller than &epsilon;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 < &epsilon;0 produced by a primitive 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 and Jeff Paris proved in 1982 that Goodstein's theorem leads to Gentzen's theorem, i.e. it can substitute for induction up to &epsilon;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.

Look at other dictionaries:

  • Consistency — For other uses, see Consistency (disambiguation). In logic, a consistent theory is one that does not contain a contradiction.[1] The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a …   Wikipedia

  • Proof theory — is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively defined data structures such as plain lists, boxed… …   Wikipedia

  • Gerhard Gentzen — Gerhard Karl Erich Gentzen (November 24, 1909, Greifswald, Germany ndash; August 4, 1945, Prague, Czechoslovakia) was a German mathematician and logician.He was one of Hermann Weyl s students at the University of Göttingen from 1929 to 1933.… …   Wikipedia

  • Gerhard Karl Erich Gentzen — (* 24. November 1909 in Greifswald; † 4. August 1945 in Prag) war ein deutscher Mathematiker und Logiker. Inhaltsverzeichnis 1 Mathematische Leistungen 2 Leben 3 Zitat …   Deutsch Wikipedia

  • Gerhard Gentzen — Gerhard Karl Erich Gentzen (* 24. November 1909 in Greifswald; † 4. August 1945 in Prag) war ein deutscher Mathematiker und Logiker. Inhaltsverzeichnis …   Deutsch Wikipedia

  • Gödel–Gentzen negative translation — In proof theory, the Gödel–Gentzen negative translation is a method for embedding classical first order logic into intuitionistic first order logic. It is one of a number of double negation translations that are of importance to the metatheory of …   Wikipedia

  • Mathematical proof — In mathematics, a proof is a convincing demonstration (within the accepted standards of the field) that some mathematical statement is necessarily true.[1][2] Proofs are obtained from deductive reasoning, rather than from inductive or empirical… …   Wikipedia

  • Formal proof — See also: mathematical proof, proof theory, and axiomatic system A formal proof or derivation is a finite sequence of sentences (called well formed formulas in the case of a formal language) each of which is an axiom or follows from the… …   Wikipedia

  • Hilbert's second problem — In mathematics, Hilbert s second problem was posed by David Hilbert in 1900 as one of his 23 problems. It asks for a proof that arithmetic of real numbers is consistent.In the 1930s, Kurt Gödel and Gerhard Gentzen proved results that cast new… …   Wikipedia

  • Peano axioms — In mathematical logic, the Peano axioms, also known as the Dedekind Peano axioms or the Peano postulates, are a set of axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”