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

notguaranteed 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

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

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

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

Why not?

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

does not makethis claim, and for good reason: PA can't evenexpressthe 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$ – Noah Schweber Oct 6 '19 at 19:24