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.