Gentzen's consistency proof

From Wikipedia, the free encyclopedia
Jump to: navigation, search

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[edit]

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 ε0. Informally, this additional principle means that there is a well-ordering on the set of finite rooted trees.

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 an ordinal 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 a primitive recursive operation on proofs corresponding to a quantifier-free formula.[1]

Relation to Gödel's theorem[edit]

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

Hermann Weyl made the following comment in 1946 regarding the significance of Gentzen's consistency result following the devastating impact of Gödel's 1931 incompleteness result on Hilbert's plan to prove the consistency of mathematics.[2]

It is likely that all mathematicians ultimately would have accepted Hilbert's approach had he been able to carry it out successfully. The first steps were inspiring and promising. But then Gödel dealt it a terrific blow (1931), from which it has not yet recovered. Gödel enumerated the symbols, formulas, and sequences of formulas in Hilbert's formalism in a certain way, and thus transformed the assertion of consistency into an arithmetic proposition. He could show that this proposition can neither be proved nor disproved within the formalism. This can mean only two things: either the reasoning by which a proof of consistency is given must contain some argument that has no formal counterpart within the system, i.e., we have not succeeded in completely formalizing the procedure of mathematical induction; or hope for a strictly "finitistic" proof of consistency must be given up altogether. When G. Gentzen finally succeeded in proving the consistency of arithmetic he trespassed those limits indeed by claiming as evident a type of reasoning that penetrates into Cantor's "second class of ordinal numbers."

Kleene (2009, p. 479) made the following comment in 1952 on the significance of Gentzen's result, particularly in the context of the formalist program which was initiated by Hilbert.

The original proposals of the formalists to make classical mathematics secure by a consistency proof did not contemplate that such a method as transfinite induction up to ε0 would have to be used. To what extent the Gentzen proof can be accepted as securing classical number theory in the sense of that problem formulation is in the present state of affairs a matter for individual judgement, depending on how ready one is to accept induction up to ε0 as a finitary method.


  1. ^ See Kleene (2009, pp. 476–499) for a full presentation of Gentzen's proof and various comments on the historic and philosophical significance of the result.
  2. ^ Weyl (2012, p. 144).