Gentzen's Consistency Proof - Gentzen's Theorem

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 ε₀ (epsilon nought). 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 ε₀ says that for any formula A(x) with no bound variables transfinite induction up to ε₀ holds. ε₀ is the first ordinal, such that, i.e. the limit of the sequence:

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