Gentzen's consistency proof

Gentzen's theorem

In 1936 Gerhard Gentzen proved the consistency of first order arithmetic using combinatorial methods. In itself, the result is rather trivial, since the consistency of first order arithmetic has a very easy proof: the axioms are true—in a mathematically defined sense—the rules of predicate calculus preserve truth and no contradiction is true, hence no contradiction follows from the axioms of first order arithmetic. What makes Gentzen's proof interesting is that it shows much more than merely that first order arithmetic is consistent. Gentzen showed that the consistency of first order arithmetic is provable, over a very weak base theory, using the principle of quantifier free transfinite induction up to the ordinal ε₀.

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 ε₀ holds. ε₀ is the first ordinal $\alpha$ , such that $\alpha^\omega = \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 ε₀. 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 ε₀ (in which case ε₀ would not be well-ordered). Gentzen assigned ordinals smaller than ε₀ 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 < ε₀ 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 can't. 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 (constructive) ordinals they can prove to be well-ordered, or equivalently for how large (constructive) ordinals is transfinite induction provable. A constructive ordinal is the order type of a recursive well-ordering of natural numbers.

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

Proof theory

Gourt Home::Gourt :: Gentzen's consistency proof

Gentzen's theorem

References