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?

3$\begingroup$ 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.) $\endgroup$– Steven LandsburgDec 3, 2015 at 5:54

1$\begingroup$ I think it's reasonable to take, say, "the unique model of secondorder Peano arithmetic" as a definition of the natural numbers; hence they satisfy the firstorder Peano arithmetic axioms by definition. The problem is then: how do you know the natural numbers exist? $\endgroup$– Qiaochu YuanDec 3, 2015 at 6:31

3$\begingroup$ 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). $\endgroup$– Mauro ALLEGRANZADec 3, 2015 at 8:01

2$\begingroup$ @StevenLandsburg: "...but some people have doubts..." Who, exactly? $\endgroup$– Thomas BenjaminDec 3, 2015 at 9:52

1$\begingroup$ @ThomasBenjamin: I believe Voevodsky is an example of someone who both has doubts and is much smarter than me. (Though, per Qiaochu's comment, it would be clearer to say that his doubts concern the consistency of Peano arithmetic and hence the existence of the natural numbers). $\endgroup$– Steven LandsburgDec 3, 2015 at 16:06
2 Answers
The axioms of firstorder 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 wellknown 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 firstorder formula. For anyone who (1) understands the natural numbers well enough to grasp the general induction principle and (2) believes that (firstorder) quantifiers over the natural numbers are meaningful so that firstorder formulas $A(x)$ really define properties, it is clear that the natural number system satisfies all of the firstorder 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 firstorder 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 wellordering of the natural numbers but for the considerably longer wellordering $\varepsilon_0$.
Thus, Gentzen uses a much longer wellordering, but his induction principle is only about primitive recursive properties, not about arbitrary firstorder definable properties. There is a tradeoff: Length of wellordering versus quantification.
I believe the tradeoff 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 tradeoff is that an additional quantifier in the induction formulas costs an additional exponential in the ordinal.

$\begingroup$ Very well explained. Definitely not $2n$; I don't remember exactly either, but it's $n$ or $n\pm1$. $\endgroup$ Dec 3, 2015 at 11:45

$\begingroup$ so to most mathematicians  those without constructivist or finitist leanings  gentzen's proof isn't necessary? $\endgroup$ Dec 3, 2015 at 13:22

$\begingroup$ Yes, from the viewpoint of most mathematicians, firstorder Peano arithmetic is obviously consistent because all its axioms are true under the standard interpretation (natural numbers with the usual addition and multiplication). $\endgroup$ Dec 3, 2015 at 15:55

$\begingroup$ @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 $\endgroup$ Dec 4, 2015 at 7:10

$\begingroup$ (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' $\endgroup$ Dec 4, 2015 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).