Regarding Gentzen's note regarding 'Godel-points' (i.e., "Where is the Godel-point hiding?")

Question

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.

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

Answer 1

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.

Answer 2

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.

Answer 3

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