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:

$<$ $\mathfrak N$, $+$, $\times$, = $>$

where $\mathfrak N$ = { |, ||, |||,...}, '$+$' 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$ 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....?


The 'Godel-point' in question would be, following Prof. Jech's Main Theorem

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

which leads me to my next question

>Is the structure $<$ $\mathfrak N$, $+$, $\times$, $=$ $>$ even definable in
$PA$ (in which case, if not, we seem to be back to confirming Prof. Ed Nelson's contention that one needs to assume an axiom of infinity in order to prove consistency....)?