If I understand correctly, the real numbers can be formalised in a first-order, like in ZF. However, such a formalisation is not strong enough to ensure that all models of the reals are isomorphic.
Why is being able to ensure isomorphism between models interesting? What's significant about that? In terms of the first-order formalisation of the reals, when does it fall short compared to a second-order theory?