Incompleteness theorem: Peano arithmetic vs. standard model of arithmetic Context (from
https://en.wikipedia.org/wiki/Non-standard_model_of_arithmetic#From_the_incompleteness_theorems):

The incompleteness theorems show that a particular sentence G, the
Gödel sentence of Peano arithmetic, is not provable nor disprovable in
Peano arithmetic. By the completeness theorem, this means that G is
false in some model of Peano arithmetic. However, G is true in the
standard model of arithmetic, and therefore any model in which G is
false must be a non-standard model.

I roughly understand the above, but some finesses about first vs. second order logic escape me. "G is true in the standard model" is
related to the use of the second order logic, but how exactly? I am
looking for high level explanations/considerations/examples rather
than technicalities.
Question 1: The "Peano arithmetic" is a first order theory which, if
augmented with the second order axiom of induction, yields exactly the
"standard model of arithmetic". Is it correct? What are the major
differences between both theories (typical statement whose proof
requires the second order induction)?
Question 2: Why is G true in the standard model of arithmetic, whereas
it may or may not be true in the Peano arithmetic? Does the Gödel
encoding requires the standard model of arithmetic? What part of the
argument (proof of Gödel's incompleteness theorem) fails in the Peano
arithmetic?
 A: I think you may be confused about the difference between models and theories. A theory is simply a set of sentences, while a model is a set with interpretations for all relevant symbols. E.g. in this context:

*

*Our language is the language of arithmetic $\mathcal{L} = \{ 0, 1, +, \times, < \}$

*PA is a theory in this language (definition can be found on Wiki)

*The standard model $\mathbb{N}$ is a structure in this language, where we interpret all the symbols with their usual meanings.

A key difference is that models have to have an opinion on every formula, since we have a way of assigning truth values to any formula. However, theories do not - it is possible that both $\psi$ and $\lnot\psi$ could be consistent with some theory. Such a theory is called incomplete.
Now, to answer your questions:

*

*PA is indeed a first order theory. It is not categorical, meaning that it has non-isomorphic models (the so-called nonstandard models of arithmetic). If you add the second-order induction axiom, you get a categorical theory, since the only model is $\mathbb{N}$. However, PA$^+$ and $\mathbb{N}$ are not the same - the former is a theory, while the latter is the unique model of that theory.


*G is true in $\mathbb{N}$ just cause it happens to be - remember every formula has to be either true or false in a given model. However, both G and its negation are consistent with PA, i.e. there are models of PA+G (such as $\mathbb{N}$), and also models of PA+(not G) - a nonstandard model. Therefore, just from PA we can't decide if G is true or false - it's consistent either way.


*I think the Gödel encoding can be done in PA (hence in nonstandard models), so it wouldn't require the standard model $\mathbb{N}$.


*The actual proof of Gödel's theorem happens in some "metatheory" which is outside of arithmetic. So, it's wrong to ask about the proof of GIT failing in PA, since the proof is not carried out in PA. The formula G is a formula in the language of arithmetic which is not provable from PA. However, note that G is not the proof of GIT, but just an object constructed as part of this proof.
A: I read a bit more about Gödel's proof, and I think that I can
reasonably well answer my own questions now.
Question 1: PA+ (PA with the second order axiom of induction) has an
essentially unique model, namely N, the standard model of arithmetic.
Any model of PA contains N (up to isomorphism), and may contain
additional exotic elements. The difference between N and a non-standard
model is precisely the presence (in a non-standard model) resp. the
absence (in the standard model N) of exotic elements. A typical claim
which does not hold in a non-standard model is: Any number is a
descendant (by iterative application of the successor function) of
zero.
Question 2: The image of a Gödel encoded number/formula/proof is, by
construction, a natural number, such that an exotic number cannot be the
encoding of anything. It is impossible for a natural number to disprove
G, because in this case, the natural number in question would encode a
proof of G, which then would yield a plain contradiction. But it is well
possible for an exotic number to disprove G, since this exotic number is
not the Gödel encoding of anything (in particular, it does not yield a
proof of G).
Remark: Both (PA and G) and (PA and not G) are consistent first order theories, which thus have models. That is, some (non-standard) model
of PA exists where G is false.
