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

At very least, Gentzen's theorem is an interesting result:

PA is consistent $\iff$ PRA+TI$_{\varepsilon_0}$ is consistent,

where PRA is primitive recursive arithmetic and where for an ordinal $\alpha$, TI$_{\alpha}$ is the set of all open formulas that are instances of transfinite induction along a well-ordering of length $\le \alpha$.

Gentzen also showed that $\varepsilon_0$ is the least ordinal $\alpha$ such that PA does not prove all instances of TI$_{\alpha}$: a transfinite induction up to $\varepsilon_0$ proves Con(PA) in Gentzen's system. This provides useful information: in a sense that is now precise, the "ordinal strength" of PA is $\varepsilon_0$, and one can now ask about the ordinal strengths of other theories, and consider more powerful systems PRA + TI$_{\beta}$ for (suitable) larger $\beta$.

It's another question, however, whether the equi-consistency result really increases anyone's confidence in the consistency of PA. After all, $\omega$ is a simpler object than $\varepsilon_0$; however, PA is more complex than PRA. So perhaps it's squeezing a bag of water, and it's interesting to see that complexity of one sort can be traded for complexity of another.

According to this bio of Gentzen, Tarski wrote:

"Gentzen's proof of the consistency of arithmetic is undoubtedly a very interesting metamathematical result, which may prove very stimulating and fruitful. I cannot say, however, that the consistency of arithmetic is now much more evident to me ... than it was before the proof was given.