If Goldbach's conjecture G is undecidable in PA, then can we prove $\mathbb N\models G$?

Question

Suppose Goldbach's conjecture $G$ is undecidable in first-order Peano arithmetic, $\sf{PA}$. That would mean there are models in which $G$ is true and other in which it is false. But intuitively, this would make $G$ "true" because there could not exist a counterexample proving $G$ false. Our intuition of "true arithmetic" can be formalized by fixing the model $\mathbb N$ in $\sf{ZFC}$ evaluating the truth of statements in $\mathbb N$. (Correct me if I'm wrong.)

So does this mean that $G$ is provably true in $\mathbb N$? This is where my understanding gets fuzzy. On the one hand, $\mathbb N$ is supposed to formalize our notion of "true" arithmetic, and since we can reason that undecidability $\implies$ true informally, I would expect this to translate into some formal statement about $\mathbb N$. On the other hand, I thought Gödel's incompleteness theorem carried more weight than "some statements about arithmetic are undecidable in $\sf{PA}$ and similar systems, so best to stick with $\mathbb N$ and then everything's fine."

Also, does the answer change if instead of merely assuming $G$ is undecidable, we assume it is provably undecidable (say, in $\sf{ZFC}$)?

Answer 1

If we could prove (in any given system) that $G$ is undecidable in PA, then we could prove there that it is true. But it is quite possible that $G$ happens to be undecidable (and true) but there is no proof of that fact.

Answer 2

It is a theorem of $\sf PA$ that

$\lnot\mathsf{provable}_{\sf PA}(\mathsf{negation}(\ulcorner G\urcorner))\to G.$

When we work in set theory, "$G$" means (internally) the exact same thing as "$G$ is true in $\mathbb N$", so if you want to specify that by "true" you mean "true in $\mathbb N,$" that's okay, but maybe a little pedantic depending on the context. My point is there's no real difference between the above theorem of $\sf PA$ and the same theorem of $\sf ZFC$... certainly not something imbued by the fact that in $\sf ZFC$ we can talk about models.

On the other hand, I thought Gödel's incompleteness theorem carried more weight than "some statements about arithmetic are undecidable in $\sf{PA}$ and similar systems, so best to stick with $\mathbb N$ and then everything's fine."

The canonical undecidable statement (the Gödel sentence) has the property that it is true, but not provable in $\mathsf{PA}.$ Of course, to prove this we need to use resources beyond $\sf PA$ (assuming $\sf Con(PA)$ will suffice).

I'm not sure what you mean by "stick with $\mathbb N$". But what the above suggests you should mean is "stick with stronger formal systems than the one you're studying if you want to prove statements it can't prove are true". And that's great until you're studying theories that are strong enough to formalize "all of math", like $\sf ZFC$ and we start wondering if more strengthening is justified. Is the Gödel sentence for $\sf ZFC$ true? Well, sure, but we're only justified in saying so inasmuch as we believe $\sf ZFC$ is consistent.

(And not to mention that not all the undecidability is of this simple "refutable if false" form of Goldbach / $\sf Con PA$ / Gödel sentence... but you asked about specifically what's given by Gödel's theorem, which is fair.)

Answer 3

You may be confusing theories and models. The question is not really whether Goldbach's conjecture "$G$ is provable in $\mathbb N$", rather whether $G$ is provable in ZFC. It could be that $G$ is undecidable in PA but provable in ZFC - which would imply by Shoenfield Absoluteness Theorem that $G$ is provable in ZF. But of course we don't know that; $G$ may be undecidable in ZF, as well.