Why is there a need for ordinal analysis?

Question

Consider the Peano axioms. There exists a model for them (namely, the natural numbers with a ordering relation $<$, binary function $+$, and constant term $0$). Therefore, by the model existence theorem, shouldn't this suffice to prove the consistency of first order arithmetic? Why is Gentzen's proof necessary?

Answer 1

The axioms of first-order arithmetic include the induction schema, which says that, for every formula $A(x)$ with free variable $x$, the conjunction of $A(0)$ and $\forall x\,(A(x)\rightarrow A(x+1))$ implies $\forall x\,A(x)$. This is, of course, a special case of the well-known and basic induction property of the natural numbers that says the same thing for any property $A(x)$ whatsoever, whether or not it's defined by a first-order formula. For anyone who (1) understands the natural numbers well enough to grasp the general induction principle and (2) believes that (first-order) quantifiers over the natural numbers are meaningful so that first-order formulas $A(x)$ really define properties, it is clear that the natural number system satisfies all of the first-order Peano axioms, and therefore those axioms are consistent.

A difficulty arises if one adopts a very strong constructivist or finitist viewpoint, doubting item (2) above, i.e., questioning the meaning of first-order quantifiers $\forall z$ and $\exists z$ when $z$ ranges over an infinite set (like $\mathbb N$) so that one can't actually check each individual $z$. From such a viewpoint, the formulas $A(x)$ occurring in the induction schema are gibberish (or close to gibberish, or at least not clear enough to be used in mathematical reasoning), and then the proposed consistency proof collapses.

The chief virtue of Gentzen's consistency proof is that it essentially avoids any explicit quantification over infinite sets. It can be formulated in terms of very basic, explicit, computational constructions (technically, in terms of primitive recursive functions and relations). There is, however, a cost for this virtue, namely that one needs an induction principle not just for the usual well-ordering of the natural numbers but for the considerably longer well-ordering $\varepsilon_0$.

Thus, Gentzen uses a much longer well-ordering, but his induction principle is only about primitive recursive properties, not about arbitrary first-order definable properties. There is a trade-off: Length of well-ordering versus quantification.

I believe the trade-off can be made rather precise, but I don't remember the details. Recall that $\varepsilon_0$ is the limit of the sequence of iterated exponentials $\omega(0)=\omega$ and $\omega(n+1)=\omega^{\omega(n)}$. If we weaken PA by limiting the induction principle to formulas $A(x)$ that can be defined with a fixed number $n$ of quantifiers, then the consistency of this weakened theory can be proved using primitive recursive induction up to $\omega(n)$, as proved by Carnielli and Rathjen in "Hydrae and subsystems of arithmetic". In other words, the trade-off is that an additional quantifier in the induction formulas costs an additional exponential in the ordinal.

Answer 2

In addition to the reasons Andreas gives, Gentzen's theorem gives additional information that's interesting even if you don't have any qualms about consistency.

In particular, ordinal analysis gives a fairly precise characterization of the provably total computable functions of a theory (and, along with it, a lot of information about the structure of proofs in PA).