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$ Dec 3, 2015 at 5:54
  • 1
    $\begingroup$ 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? $\endgroup$ Dec 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$ Dec 3, 2015 at 8:01
  • 2
    $\begingroup$ @StevenLandsburg: "...but some people have doubts..." Who, exactly? $\endgroup$ Dec 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$ Dec 3, 2015 at 16:06

2 Answers 2


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.

  • $\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, 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). $\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).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.