Is the 'copy' of the naturals in ZF a unique way to represent the second-order arithmetic in first-order logic? The following line of thought came into me while studying introductory logic and set theory. I feel like there is an error in it somewhere, but I can't point it. It might even be correct.


*

*We have the copy of naturals in ZF as $\omega$

*$\omega$ is unique and with functions we can define in ZF, it satisfies the axioms of PA

*This gives a model of PA in a first-order language in a unique way

*We can prove that the structure in ZF satisfies the properties of PA, and even we can formulate the stronger second-order induction on this structure as in ZF subsets are just elements

*This gives that we can capture the second order arithmetic, the intended model of the naturals.


Is there something wrong with this line of thought? If we consider different models of ZF, do we get different $\omega$?
If this indeed captures the second order arithmetic, then can't we deal with second order problems in this first order representation? Maybe inherit first order properties like a deductive system?
 A: Different models of ZF(C) can have different $\omega.$ For instance, any model of ZFC plus “ZFC is inconsistent” will necessarily have a nonstandard $\omega$ (assuming ZFC is consistent, the proof of inconsistency must be coded by a nonstandard number or it would be an actual proof of inconsistency).
The reason this doesn’t conflict with categoricity of second order arithmetic that the nonstandardness can’t be seen internally. For instance, any infinite descending sequence won’t be in the model. So internally, the model’s $\omega$ is a model of second order arithmetic (after all, being the model’s natural numbers, it is isomorphic to the model’s natural numbers), but not externally.
So while ZFC interprets second order arithmetic, this doesn’t solve incompleteness since ZFC is arithmetically incomplete. We do inherent a strong deductive system for arithmetic, but there are still arithmetic statements that are undecidable, most notably the consistency of ZFC.
(Here it is also good to remember that while second order arithmetic is as strong as possible semantically, any effective deductive system for it must still be constrained by the incompleteness theorem (which shows why the completeness theorem must fail for second order logic). This of course includes the deductive system we get from ZFC, although from the perspective of ZFC it manifests as regular old first order incompleteness, where a statement is true in some models and false in others if and only if it is undecidable, etc.)
