[cevi]

Unfortunately no, ZFC isn't good enough to capture arithmetical truth. The problem is that there are nonstandard models of ZFC where every single model of second-order PA within is itself nonstandard. There are even models of ZFC where a certain specific computer program, known as the "universal algorithm" [1], solves the halting problem for all standard Turing machines.

https://jdh.hamkins.org/the-universal-algorithm-a-new-simple...

[czbot]

ZFC allows models of second order PA and proves that those models are all isomorphic. Within each model of ZFC there is no such thing as a nonstandard model of second order PA. One can only think it is nonstandard by looking from outside the model, no? What theorem of second order PA is ZFC unable to prove?

This is similar to how there are countable models of ZFC but those models think of themselves as uncountable. They are countable externally and not internally.

[cevi]

The consistency of ZFC is (presumably) a theorem of second order PA, and ZFC is unable to prove it (unless ZFC is inconsistent).

[czbot]

Indeed yes. But in a sense within ZFC one can say what N is given the categorical nature of second order PA. Each model of ZFC will have, up to isomorphism, one model of N.