Can ZFC decide number theory?

Gödel's proof gives an explicit construction for a statement in a given (sufficiently strong, and recursively axiomatizable) theory that cannot be proved or disproved in the theory.

It so happens that when the theory is ZFC the independent statement turns out to be one that is the set-theoretic representation of a purely number-theoretic statement. At least this is the case when you use the most natural way to establish that ZFC meets the condition of being "sufficiently strong".

Basically, "sufficiently strong" boils down to being able to represent certain basic number-theoretic constructions, and the Gödel sentence is then constructed as the representation of a particular number-theoretic property.

The formal statement "Con(ZFC)" is a number theoretic statement, in the same way that "Con(PA)" is, and (assuming the consistency of ZFC) it is independent of ZFC.

One can construct a proof by a small variant of the proof that a recursively axiomatized complete theory is decidable.

$1$. It is well-known that there is no algorithm that, given any sentence $\varphi$ of Number Theory, will determine whether that sentence is true in the natural numbers. More precisely, if the set of sentences of Number Theory is indexed as $(\varphi_n)$ in any one of the usual ways, then the set of $n$ such that $\varphi_n$ is true in $\mathbb{N}$ is not recursive. Indeed, the situation is much worse than that: the set is not even arithmetical.

$2.$ Suppose that $T$ is a recursively axiomatized extension of Peano Arithmetic. Then there is a sentence $\varphi$ of Number Theory such that $\varphi$ is neither provable nor refutable in $T$. The idea is that we can write a program that list the proofs in $T$, since the set of (indices of) proofs is recursively enumerable.

If for every sentence $\varphi$ of Number Theory, one of $\varphi$ or $\lnot\varphi$ is a theorem of $T$, then sooner or later one of $\varphi$ or $\lnot\varphi$ will show up as the final sentence of a proof in the list. This procedure would give an algorithm for determining truth of sentences in $\mathbb{N}$, contradicting ($1$).

There is a minor technicality that one needs to deal with, since ZFC is not an extension of Peano Arithmetic. To deal with that, for any sentence $\psi$ of Number Theory, we can mechanically produce a sentence $\psi'$ of Set Theory such that if $\psi'$ is a theorem of ZFC, then $\psi$ is true in $\mathbb{N}$. The sentence $\psi'$ is obtained from the usual construction of $\mathbb{N}$, and its addition and multiplication, in ZFC.