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?