Q:

Is every true statement about the natural numbers provable in ZFC?

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.

A:

Not really. The statement "$\sf ZFC$ is consistent" can be translated into a statement about the natural numbers in the standard coding way, it's even a $\Pi_1$ statement as far as $\sf PA$ is concerned.
Now, if $\sf ZFC$ is truly consistent, then it cannot prove this fact, so this is a true statement which is not provable. But if $\sf ZFC$ is inconsistent, well, then this question is moot, isn't it?

Let me add a small and fine point. Most "standard" set theoretic independence come from one of two things:

Forcing and inner models related results, like the Continuum Hypothesis or Martin's Axiom. These are not related to number theoretic results, not directly, and since these methods cannot change the truth about first-order statements on the natural numbers (second-order is a different thing, since different models can have more or less subsets of natural numbers), the proofs obtained by these methods indicate that the statements in question are not really related to number theoretic ones.
Stronger theories, like inaccessible cardinals or the consistency of $\sf ZF$ and extensions thereof. These are number theoretic statements, for the most part $\Pi_1$ or $\Sigma_1$ results about the consistency or inconsistency of certain things. For example, $\sf ZFC$ and "There is a nontrivial elementary embedding $j\colon V\to V$" is inconsistent. While formalizing this might be a bit awkward, we can still turn this into a number theoretic statement, and this would be a $\Sigma_1$ statement. Then not only that this statement is true, $\sf PA$ itself would prove it!

Now you might argue that neither is a number theoretic problem. And these would be something like Diophantine equations, or Goldbach's conjecture. And to this I would retort, that the second type of statements are Diophantine equations, or rather could be translated to them. And that Goldbach's conjecture, and things like that, by the first type of statements, cannot be proved to be independent just using forcing or inner model arguments. Thus a proof that Goldbach is independent of $\sf ZFC$ would have to be of an entirely new style.

A:

The categoricity of the second-order Peano axioms simply means (in the context of ZFC set theory) that every model of ZFC contains exactly one thing (up to internal isomorphism) that it thinks is a model of those axioms.
However, different models of ZFC can have different $\mathbb N$s. Each model will think its $\mathbb N$ satisfies the second-order Peano axioms, but that is not generally true (in standard semantics) when viewed "from the outside". Oftentimes it will simply be the case that the collection that would be a counterexample to the induction axiom does not exist as a set in the model.

A:

If ZFC is inconsistent, then yes: everything can be proven in an inconsistent theory.
If it is consistent, then no, by the Godel results.

