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?
Thanks!
To take a stab at the other question, ensuring isomorphism between models amounts to having a characterization of the object in question and so demonstrating that it makes sense to talk about the object in question. For example, up to isomorphism there is only one countable dense linear order without endpoints: any such order is order-isomorphic to $\langle\mathbb{Q},\le\rangle$. Thus, we can reasonably talk about the dense linear order without endpoints, and we can resolve questions about it by looking specifically at $\langle\mathbb{Q},\le\rangle$. Whether this is interesting is perhaps a matter of taste, but it pretty clearly is significant, in that it facilitates understanding and further investigation of the object. It also makes it easier to recognize the object when it appears in an unfamiliar guise.