Why is there a need for ordinal analysis?

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?

• How do you know the natural numbers satisfy the Peano axioms? (Personally I have no doubt about this, but some people do have doubts, and some of those are much smarter than I am.) – Steven Landsburg Dec 3 '15 at 5:54
• I think it's reasonable to take, say, "the unique model of second-order Peano arithmetic" as a definition of the natural numbers; hence they satisfy the first-order Peano arithmetic axioms by definition. The problem is then: how do you know the natural numbers exist? – Qiaochu Yuan Dec 3 '15 at 6:31
• It may help if you locate Gentzen's proof in the context of "foundational debate" : see Hilbert's program and The consistency of arithmetic and analysis. If you are interested to the question : "how may I prove that there exists a "structure" satisfying Peano's axioms", then you cannot invoke the model existence theorem, because it presuppose the consistency of the theory, and this is "hard" to prove (if we do not assume the existence of the sought structure). – Mauro ALLEGRANZA Dec 3 '15 at 8:01
• @StevenLandsburg: "...but some people have doubts..." Who, exactly? – Thomas Benjamin Dec 3 '15 at 9:52
• @ThomasBenjamin Also Edward Nelson, if I understand his views correctly. – Noah Schweber Dec 3 '15 at 20:32

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)\to 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 the language of primitive recursive arithmetic). 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)$. [I don't guarantee that the last $n$ here is correct; you might need something like $2n$; I hope an expert will come along and edit this answer to fix any error I've made.] In other words, the trade-off is that an additional quantifier in the induction formulas costs an additional exponential [or two?] in the ordinal.

• Very well explained. Definitely not $2n$; I don't remember exactly either, but it's $n$ or $n\pm1$. – Emil Jeřábek Dec 3 '15 at 11:45
• so to most mathematicians -- those without constructivist or finitist leanings -- gentzen's proof isn't necessary? – user3730940 Dec 3 '15 at 13:22
• Yes, from the viewpoint of most mathematicians, first-order Peano arithmetic is obviously consistent because all its axioms are true under the standard interpretation (natural numbers with the usual addition and multiplication). – Andreas Blass Dec 3 '15 at 15:55
• @AndreasBlass: Just to get my facts straight: i) did the "Hilbert School" have what they deemed a 'finitary' proof of the consistency of $PRA$ before the Goedel and Gentzen results; ii) did Gentzen prove the consistency of $PRA$+"Induction principle for $\epsilon_{0}$"? If so then the following principle of Hilbert seems to be relevant (this from "On the Infinite"): "For there is a condition, a single but absolutely necessary one, to which the use of the method of ideal elements [in this case, the induction principle for $\epsilon_{0}$ --my comment] is subject, and that is the proof of – Thomas Benjamin Dec 4 '15 at 7:10
• (cont.) consistency; for, extension by the additions of ideals is legitimate by only if no contradiction is thereby brought about in the old, narrower domain [$PRA$--my comment], that is, if the relations that result for the old objects whenever the ideal objects are eliminated are valid in the old domain [relative consistency result?--my question and comment ] ." Note also that $PRA$ can be recast in terms of concatenation and operations and relations on the strings $e$ (the 'empty' string), |, ||, |||,.., etc., so one can dispense with questions regarding the 'existence' or 'nonexistence' – Thomas Benjamin Dec 4 '15 at 7:45

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