[yequalsx]

You're welcome. I think your understanding is correct.

I will add one more thing for completeness sake. There are statements that are true of the natural numbers, the natural numbers that you and I think of when see this term, that can't be proven in the first order theory. This means that there is a non-standard model in which there is a non-standard integer that is a counterexample to the statement. The second order axioms are categorical so there is a proof of such a statement using the second order axioms. One may not be able to find such a proof but there is one.