Existence and uniqueness up to isomorphism of the real numbers from axioms Pretty much what the title says: how does one prove the existence and uniqueness of the real number system from the ordered field axioms together with the least-upper-bound property (or maybe some equivalent), instead of using some construction process?
Thanks in advance.
 A: I don't know how to write a formal proof in ZF and even if I did, I would still write an informal proof here because it's easier to understand and it will be easy for an expert to figure out how to write a complete formal proof that there is a complete ordered field which is unique up to isomorphism from reading this answer.
First, we can define a natural number as a finite ordinal number. Let's define 0 to be the empty set. For each natrual number $x$, let's define its the successor function $S$ to be a function from the set of all finite ordinals to itself such that for every finite ordinal $x$, $S(x) = x \bigcup {\text{{x}}}$. Now we can see that the function $S$ satisfies closure on the set of all natural numbers and every natrual number can be gotten by starting from 0 and applying the successor function. Now we can define addition recursively as


*

*$\forall x \in \mathbb{N}, x + 0 = x$

*$\forall x \in \mathbb{N}\forall y \in \mathbb{N}, x + S(y) = S(x + y)$
Now we can define multiplication in terms of addition as


*

*$\forall x \in \mathbb{N}, x \times 0 = 0$

*$\forall x \in \mathbb{N}\forall y \in \mathbb{N}, x \times S(y) = (x \times y) + x$
Now it's easy to prove the following statements using this definition but I won't bother writing the proof


*

*$\forall x \in \mathbb{N}\forall y \in \mathbb{N}\forall z \in \mathbb{N}, (x + y) + z = x + (y + z)$

*$\forall x \in \mathbb{N}\forall y \in \mathbb{N}, x + y = y + x$

*$\forall x \in \mathbb{N}\forall y \in \mathbb{N}, x \times y = y \times x$

*$\forall x \in \mathbb{N}\forall y \in \mathbb{N}\forall z \in \mathbb{N}, x \times (y + z) = (x \times y) + (x \times z)$

*$\forall x \in \mathbb{N}\forall y \in \mathbb{N}\forall z \in \mathbb{N}, (x \times y) \times z = x \times (y \times z)$
Now we can construct the set of all integers as follows. 0 is not a solution to $x + 1 = 0$ so we can invent the solution -1. We can again invent a solution to the equation $x + 1 = -1$, -2 and keep going for ever and call the result the set of all integers $\mathbb{Z}$. We can also invent an intuitive definition of + and \times and show that it still has those properties and agrees with those operations on $\mathbb{N}$.
Now we can construct the dyadic rationals as follows. For each odd number $x$, we can invent a solution to the equation $2 \times y = x$. Each newly invented solution $y$ is still not a solution to the equation $2 \times z = y$ so we can also invent a solution to that and keep going and call the result the set of all dyadic rationals. We can also create an intuitive definition for those operations on that set and show that it still satisfies those 5 laws and agrees with those operations on $\mathbb{Z}$. We can also create an intuitive definition of the relation $\leq$ on that set. Now that we invented that relation, take any subset of that set such that that set and its complement are nonempty and for any member of the subset, all smaller members of the set are in the subset. When the set has no maximal element and its complement has no minimal element, we will invent a number that's larger than all members of the subset and smaller than all members of the complement. Let's call those the real numbers. Now we can also invent an intuitive definition +, $\times$ and $\leq$ and show that $\exists x\exists y$ such that $(\mathbb{R}, x, y, +, \times, \leq)$ is a complete ordered field where some of the defining criteria are that $x$ is a multiplicative identity and $y$ is an additive identity and those 5 laws still hold. We can also show that +, $\times$, and $\leq$ on this set agree with the way they were defined on the previous set and that 0 is the additive identity and $S(0)$ is the multiplicative identity.
Now take any complete ordered field. Either it has infinitesimal numbers or it doesn't. If it does, then it's not complete. Therefore, no complete ordered field has infinitesimal numbers. Also, every complete ordered field without infinitesimal numbers is isomorphic to that complete ordered field. Therefore, all complete ordered fields are isomorphic to that one.
