Consider the following note written by Gerhard Gentzen in early 1932, on the onset of his work on a consistency proof for arithmetic:

The axioms of arithmetic are obviously correct, and the principles of proof obviously preserve correctness. Why cannot one simply conclude consistency, i.e., what is the meaning of the second incompleteness theorem, the one by which consistency of arithmetic cannot be proved by arithmetic means? Where is the Godel-point hiding?

The first question one might ask when reading this statement (plus three questions) is, how is it that Gentzen concludes that, "The axioms of arithmetic [read 'arithmetic' as meaning, $PA$--my comment] are obviously correct."? Well, one might infer that Gentzen infers that "The axioms of arithmetic are obviously correct" by virtue of the fact that the axioms of $PA$ satisfy the following structure:

$$\langle \mathfrak N, +, \times, = \rangle$$

where $\mathfrak N = \{ |, ||, |||,\ldots\},$ '$+$' as meaning concatenation, '$\times$' as meaning the Hilbert-Bernays definition of multiplication (e.g., || $\times$ ||| means replacing each | in || by |||, i.e., ||||||), and '=' as simply meaning equality as defined by the axioms of equality, i.e. for the axiom of equality 'a=a' one has, for the elements of $\mathfrak N$, the following equalities:

{ |=|, ||=||, |||=|||,...} [given this, and the closure of $\mathfrak N$ under $+$ and $\times$, how is it possible that $PA$, satisfying this structure, could ever derive, say, '||=|||'?]

In his answer to Noah Schweber's mathoverflow question, "What are some proofs of Godel's Theorem which are essentially different from the original proof?", Ron Maimon mentions the "Jech/Woodin Set theory model proof". In regards to Gentzen's point of view (at least in early 1932), it might behoove one to take a close look at Prof. Jech's three-page paper (Proceedings of the American Mathematical Society, Volume 121, Number 1, May 1994, pp. 311-313).

Why? Because of "Remark 2" on pg. 312 which states:

Even though our proof of Godel's Theorem [Second Incompleteness Theorem--my comment] uses the Completeness Theorem, it can be modified to apply to weaker theories such as Peano Arithmetic ($PA$). To prove that $PA$ does not prove its own consistency, (unless it is inconsistent), we argue as follows:

Assume that $PA$ is consistent and that "$PA$ is consistent" is provable in $PA$. There is a conservative extension $\Gamma$ [let it be $ACA_0$ as in Noah Schweber's answer--my comment] of $PA$ in which the Completeness Theorem is provable [Theorem 5.5, p. 443, of Takeuti's Proof Theory, 2nd ed.--my expansion of his comment by his reference], and moreover, $PA$ $\vdash$ ($\Gamma$ is a conservative extension of $PA$). Therefore, $\Gamma$ $\vdash$ ($\Gamma$ is a conservative extension of a consistent theory) and thus proves its own consistency. Consequently, $\Gamma$ proves that $\Gamma$ has a model.

Now let $\Sigma$ be a sufficiently strong finite subset of of $\Gamma$ that proves that $\Sigma$ has a model; the proof above leads to a contradiction.

Is this where the Godel-point is hiding with regards to Gentzen's statement and first question?

The axioms of arithmetic are obviously correct, and the principles of proof obviously prove correctness. Why cannot one simply conclude consistency....?

Would the 'Godel-point' in question be, following Prof. Jech's Main Theorem,

It is unprovable in $ACA_0$ (unless $ACA_0$ is inconsistent) that there exists a model of $PA$. ?

Now as regards Noah Schweber's very nice answer, I have two questions regarding the following passage

...However, we are not guaranteed that our model $\mathfrak M$ [of $ACA_0$-- my comment] thinks that its first-order part actually satisfies $PA$. That is, the "obvious truth" of the $PA$ axioms is not actually that obvious.

This is an example of a failure on an $\omega$-rule: while for each axiom $\varphi$ of $PA$ we do in fact have "$Num$($\mathfrak M$) $\vDash$ $\varphi$" (appropriately phrased) is true in $\mathfrak M$, we do not get from this that "$Num$($\mathfrak M$) $\vDash$ each $PA$ axiom" is true in $\mathfrak M$. And this is just like how being able to check each individual derivation in $PA$ doesn't give us a way to check all derivations at once, so it really shouldn't be suprising.

  1. How does the above passage relate to Gentzen's note, especially the phrase

That is, the "obvious truth" of the $PA$ axioms is not actually that obvious.

  1. What perspective is Gentzen taking in his note (external or internal) and why does it matter what $\mathfrak M$ 'thinks' (so to speak) as regards Gentzen's note?

Now two questions for Panu Raatikainen: as regards your statement

In general, we just cannot see that they [the theories "which include elementary arithmetic and happen to be consistent"--my paraphrase of your earlier comment] are consistent.

  1. Why not?

  2. What was Gentzen 'seeing' when he made his statement ("The axioms of arithmetic are obviously correct, and the principles of proof obviously preserve correctness"), and why was his 'seeing' incorrect (i.e., leading to inconsistency)?

  • 1
    $\begingroup$ What does it mean to talk about a structure being definable in a theory? Certainly there are models of PA which do not interpret the standard model (indeed, no nonstandard model of PA can interpret the standard model). $\endgroup$ Oct 6, 2019 at 19:17
  • 1
    $\begingroup$ Also, you attribute to Jech the claim "It is unprovable in PA (unless PA is inconsistent) that there exists a model of PA." But Jech does not make this claim, and for good reason: PA can't even express the existence of a model of PA! This is the whole point of passing to the conservative extension $\Gamma$, which is capable of talking about models. $\endgroup$ Oct 6, 2019 at 19:24
  • $\begingroup$ @NoahSchweber: Thanks for your helpful comments. Sorry I didn't respond sooner. Would this fix the error: 'It is unprovable in $ACA_0$ (unless it is inconsistent) that there exists a model of $PA$'? Pleas let me know and I will appropriately edit. $\endgroup$ Oct 7, 2019 at 21:25
  • $\begingroup$ Yes, that's right (per my answer). $\endgroup$ Oct 7, 2019 at 22:19
  • 1
    $\begingroup$ You shouldn't edit your question with continuing questions for specific answerers - comment on their answers instead. $\endgroup$ Oct 9, 2019 at 21:06

3 Answers 3


Your question seems to boil down to (after fixing an error) the following:

Any model $\mathfrak{M}$ of ACA$_0$ has a first-order part $Num(\mathfrak{M})$, which satisfies PA; why doesn't this mean that ACA$_0$ proves "PA has a model" (indeed, the a priori stronger "PA is sound") and hence its own consistency?

Here ACA$_0$ is a conservative extension of the type Jech mentions (what he calls "$\Gamma$"): it can talk about models and prove basic model-theoretic results (e.g. the soundness and completeness theorems), and is PA-provably a conservative extension of PA.

The issue is the following. Fix a model $\mathfrak{M}$ of ACA$_0$. We can indeed talk about $Num(\mathfrak{M})$ as a structure in $\mathfrak{M}$, and have the following:

$(*)\quad$ Any set of sentences true in $Num(\mathfrak{M})$ is consistent.

However, we are not guaranteed that our model $\mathfrak{M}$ thinks that its first-order part actually satisfies PA. That is, the "obvious truth" of the PA axioms is not actually that obvious. From the existence of such models we conclude

PA $\not\vdash Sound($PA),

and so in particular the obvious argument for PA$\vdash$ "PA has a model" breaks down.

This is an example of a failure of the $\omega$-rule: while for each axiom $\varphi$ of PA we do in fact have that "$Num(\mathfrak{M})\models \varphi$" (appropriately formalized) is true in $\mathfrak{M}$, we do not get from this that "$Num(\mathfrak{M})\models$ each PA axiom" is true in $\mathfrak{M}$. That is:

ACA$_0$ doesn't prove that PA is sound; indeed, no conservative extension of PA can (since then it would prove that PA is consistent, which is in the language of PA and not PA-provable).

This is just like how being able to check each individual derivation in PA doesn't give us a way to check all derivations at once, so it really shouldn't be surprising.

Re: your edits, the point is that knowing that ACA$_0$ doesn't prove the soundness of PA indicates that we can be "smart enough" to know each specific axiom of PA, yet still not know that PA as a whole is true. So when Gentzen says that that PA is "obviously correct," that's a slightly weaker level of obviousness than any of the individual PA axioms.

This saves us from the circle Gentzen is gesturing at. While focusing on PA, Gentzen is more generally describing a hypothetical situation where - in a sufficiently rich language (e.g. that of second-order arithmetic) - we have some notion of "obviousness" with the following properties:

  • The set of obvious sentences is consistent,

  • Every axiom of PA is obvious,

  • The set of obvious sentences is c.e., and

  • It's obvious that every obvious arithmetic sentence is true.

Godel's theorem implies that no such property exists; the fact that ACA$_0\not\vdash Sound($PA) is a particular example of this phenomenon, showing that PA doesn't correspond to the first-order part of such a notion of obviousness and hopefully making it more intuitively clear why the above situation can't happen despite its face-value-plausibility.

  • $\begingroup$ Thanks-- this is heipful. A couple of questions by way of clarification: First, is the property you refer to that Godel's theorem proves does not exist the property of being 'obvious'? Second, does the $\omega$-rule you refer to fail because "for each axiom $\varphi$ of $PA$ we do in fact have that '$Num$($\mathfrak M$) $\vDash$ $\varphi$' (appropriately formalized) is true in $\mathfrak M$", internal to $ACA_0$, while " '$Num$($\mathfrak M$) $\vDash$ each $PA$ axiom' is true in $\mathfrak M$", external to $ACA_0$? If so, would the $\omega$-rule succeed if it was treated as a rule of $\endgroup$ Oct 9, 2019 at 20:46
  • $\begingroup$ (cont.) inference in some informal metatheory? $\endgroup$ Oct 9, 2019 at 20:48
  • $\begingroup$ GIT says that no notion of obviousness fitting the criteria I give exists. You're right about the failure of the $\omega$-rule I'm referring to. I'm not sure what your last question means; certainly it's true that once we add the $\omega$-rule to our system, what I've written is no longer applicable, nor is GIT (indeed, PA + $\omega$-rule yields true arithmetic). $\endgroup$ Oct 9, 2019 at 20:50
  • $\begingroup$ Well, $\omega^2$ applications of the $\omega-rule$.... $\endgroup$ Oct 9, 2019 at 21:04
  • $\begingroup$ @ThomasBenjamin So what? (If you want to restrict to limited applications, that needs to be specified.) Besides, this is getting a bit far afield from your specific question. $\endgroup$ Oct 9, 2019 at 21:05

Gentzen's remark has some bite in the case the standard first-order arithmetic PA, because we plausibly know a bit more arithmetically. But he apparently did not understand the generality of the incompleteness theorems: they hold for any theory which includes elementary arithmetic and happens to be consistent. In general, we just cannot see that they are consistent (even if they happen to be.) And as soon as Gentzen would define what exactly he means by "arithmetic means", we can prove that the consistency of the theory of those arithmetic means cannot be proved by those arithmetic means.

  • $\begingroup$ Thanks for your helpful answer--it is somewhat closer to the mark (so to speak) especially considering that you note (in your 'Stanford' entry) that transfinite induction up to $\epsilon_0$ in an early example on an unprovable mathematical statement on a par (so you wrote in your entry) with Paris-Harrington (and others). If one assumes $\epsilon_0$ exists (and if one assumes $\omega$ exists, why not....) then transfinite induction up to $\epsilon_0$ is 'true' but unprovable. If one uses Gentzen's (or Hilbert-Bernays', or Ackermann's) ordinal notations, one can even make $\endgroup$ Oct 7, 2019 at 21:43
  • $\begingroup$ (cont.) the case (as does (Zach) of such transfinite induction's 'finitariness'. Take a look (for the umpteenth time, no doubt) at the Peano Axioms--they seem to be 'obvious' statements derived from the definition of the operations and relations. Why doen Gentzen's not 'draw blood'? $\endgroup$ Oct 7, 2019 at 21:47
  • $\begingroup$ the last sentence should read: Why doesn't Gentzen's note 'draw blood'? $\endgroup$ Oct 8, 2019 at 21:46

In his answer to David Roberts' mathoverflow question, "$Z_2$ versus second-order $PA$" (question 97077), Prof. Ali Enayat writes (Under the subheading, "Regarding the second question)":

One way to see this is based on an old result (noticed by a number of people, including Takeuti and Feferman) that $ACA$ is equiconsistent with an extension $PA$($T$) of $PA$ with a distinguished predicate $T$ that codes up the full truth predicate for the ambient model of arithmetic [which I will assume (for want of a better assumption) is the intended model for $PA$--my comment]. Note that $PA$($T$) includes induction in the extended language of arithmetic augmented by the predicate $T$ [footnote 1 on pg. 2 of Enayat and Pakhomov's arXiv preprint, "Truth, Disjunction, and Induction" (arXiv:1805.09890v1 [math.LO] 24 May 2018) seems to be a restatement of this-- my comment].

If somehow Gentzen was implicitly working in $PA$($T$)(without realizing it, of course), it would explain the viewpoint expressed in the aforementioned note.

The question now remains as to whether in fact he was, which is a question to ask a historian of Gentzen's work (von Plato, perhaps)?


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.