In lecture notes from Lou van den Dries, page 3 here - http://www.math.uiuc.edu/~vddries/main.pdf, it is said:
"However, in our present state of knowledge, $GC$ (Goldbach conjecture) might be true in $(\mathbb{N}; 0, 1, +, ·, <)$, but not provable from those axioms (Peano axioms). (On the other hand, once you know what exactly we mean by provable from the Peano axioms, you will see that if $GC$ is provable from those axioms, then $GC$ is true in $(\mathbb{N}; 0, 1, +, ·, <)$, and that if GC is false in $(\mathbb{N}; 0, 1, +, ·, <)$, then its negation $\neg GC$ is provable from those axioms.)"
Could someone please explain me why this is true? I don't know where to start. I'm sure if I go through the whole notes I might get a better idea of why this is true, but given my understanding that's quite far away from where I am now, and this is a nice concrete example of something interesting, that I'd like to understand now. A pointer to where exactly in the notes I should look would be appreciated as well.
The key fact is:
This means that any statement using only bounded quantifiers which is true in $\mathbb{N}$ is true in every model of $PA$.
The other key fact is:
For instance, $0$ is defined as the unique $x$ such that "$\forall y<x(y\not=y)$". Note that this does not mean that the set $\mathbb{N}$ is definable in $M$, for every $M\models PA$; in fact, it never is.
Now suppose Goldbach is false. Then there is some even $n>2$ such that $n$ cannot be written as the sum of two primes. But this is a bounded statement in terms of $n$: clearly those primes must be $<n$, so the quantifier over primes is bounded; and saying that an element is prime involves quantifying over only numbers less than it. Finally, since $n$ itself is definable by a bounded formula, there is a single sentence $\varphi$, using only bounded quantifiers, which expresses "$n$ is a counterexample to Goldbach". This sentence is true in every model of $PA$, since every model of $PA$ is an end extension of $\mathbb{N}$; so by the Completeness Theorem, $PA\vdash\varphi$. But then $PA$ disproves Goldbach.
Note that this hinges on the fact that Goldbach being false would be witnessed by a single bounded statement about a single natural number (some counterexample). Goldbach being true, however, would not be. So if Goldbach is true, $PA$ might still not be able to prove it.
A statement like the Twin Prime Conjecture is even worse. What is a counterexample to TPC? Well, it's an $n$ such that there is no twin prime above $n$. So the failure of TPC would be witnessed by a single natural number. But the statement that $n$ is a counterexample to TPC involves an unbounded quantifier - " . . . above $n$"! So even if TPC is false, $PA$ might not know. And TPC being true isn't witnessed by a single example, but rather infinitely many - so even though being a twin prime is a bounded statement, TPC being true need not imply that $PA$ proves TPC.
This kind of distinction between mathematical principles leads to a natural hierarchy of sentences of arithmetic - the arithmetic hierarchy - which is intensively studied (along with its extensions and generalizations) throughout mathematical logic:
In computability theory, unbounded quantifiers roughly correspond to the Turing jump, a generalization of the halting problem. This operation is fundamental in computability theory; there is a natural extension of the arithmetic hierarchy to transfinite iterates of the Turing jump, called the hyperarithmetic hierarchy, which in turn is connected with quantifiers in infinitary logic.
In model theory, the structure of quantifiers in a sentence can determine the kinds of algebraic operations on its models which preserve its truth; see e.g. this. This is essentially the arithmetic hierarchy generalized to arbitrary structures.
In set theory, the Levy hierarchy is the generalization of the arithmetic hierarchy; quantifiers of the form "$\forall x\in a$" take the place of quantifiers of the form "$\forall n<k$". Additionally, a second-order analogue of the arithmetical hierarchy plays a fundamental role in descriptive set theory, and in the analysis of forcing extensions.
In proof theory, theories of arithmetic are fruitfully studied by stratifying them into hierarchies of weaker theories via the arithmetic hierarchy.