Related questions: Difference between undecidable statements in set-theory and number theory? Is the arithmetic most mathematicans use a modelled within first or a second order logic?
Peano's axioms (in second-order logic) are categorical - they characterize the natural numbers completely, with every one of their models being isomorphic to "the standard model" of the natural numbers. Unfortunately, they are second-order - which means they are not complete, and so not every true statement about the natural numbers will be provable from Peano's axioms.
To overcome this problem, we use set theory, which allows us to place the natural numbers in a first-order set theory such as ZFC, and restate Peano's axioms as first-order statements in the universe of sets. We therefore acquire a theory much bigger than Peano's axioms, which however includes a specific set $\mathbb{N}$ for which all the Peano axioms (including the second-order induction axiom, which is now a first-order statement in the universe of sets) apply. We are now working in a first-order theory, and so every true statement here should be provable.
My question is therefore, is every true statement about the natural numbers provable in ZFC? As far as I understand, every true statement about $\mathbb{N}$ should be provable in ZFC, because ZFC is a first-order theory. You will, of course, have statements in ZFC (like the continuum hypothesis) which are undecidable in ZFC; that's okay, because ZFC has many models. However the natural numbers in ZFC are not so much a formal system anymore as they are simply a specific set which exists in all models of ZFC and satisfies Peno's axioms, sort of like how analytic geometry is not a formal system anymore but a specific model of euclidean geometry. So as much as I understand, you should be able to prove any true statement about $\mathbb{N}$ in ZFC.
I ask whether that is actually true, because everywhere I read about undecidable statements, people mention that statements like Goldbach's conjecture or the $3n+1$ problem might turn out to be undecidable. However those are statements about $\mathbb{N}$, about the specific set $\mathbb{N}$ that is formalizable as the unique model of a first-order set of axioms in the language of ZFC, and so I don't understand how is it possible that ZFC won't be able to prove all true statements about it (even though it will surely have undecidable statements in it). Another way to phrase my question is, are all undecidable statements in ZFC unrelated to number theory? If this is not the case, please explain to me where is the problem with my logic.