Gentzen's consistency proof

Remarks

Gentzen published the proof in 1936, and a second proof in 1938. In the second proof, one assigns to each derivation of a sequent in a sequent calculus for PA an ordinal below $\varepsilon_0$. One then gives a primitive recursive reduction step that turns any derivation of the empty sequent into another derivation of the empty sequent with a smaller ordinal. Transfinite induction along $\prec$ shows that no derivation of the empty sequent exists.

By Gödel's second incompleteness theorem, PA does not prove its own consistency. So PA does not prove the transfinite induction used here, although every part of the proof other than this induction is finitary. Gentzen later showed directly that PA proves transfinite induction along $\prec$ up to each ordinal below $\varepsilon_0$, but not up to $\varepsilon_0$. Thus $\varepsilon_0$ is exactly the length of induction that PA cannot reach.

Going deeper

For a student

The proof assigns ordinals to proofs and shows that reduction steps make the ordinal go down. Since the ordinals below $\varepsilon_0$ are well-ordered, the reduction must stop, and so no proof of a contradiction can exist. This is the first ordinal analysis: it shows that $\varepsilon_0$ is the proof-theoretic ordinal of PA. The method extends to stronger theories, which get larger ordinals.