The real numbers can be constructed in a number of different ways. Most people who've taken a real analysis course are familiar with either the Dedekind cut or Cauchy sequence constructions. However, there is a third option, which we might call the Leibniz monad construction. It relies on nonstandard analysis, and involves in an essential way some of the more technical and confusing aspects of nonstandard analysis, so it's not the most suitable construction for beginners. However, it is quite simple and elegant, provided the machinery of nonstandard analysis is set up and you are comfortable with using it. Since I couldn't find a exposition of it online or in any textbooks that I found wholly satisfactory, I have tried to provide one in this post.
For convenience, I shall work in Mauro Di Nasso's *ZFC, rather than in ZFC. This makes it easy to use nonstandard analysis without having to do a lot of preliminary setup.
*ZFC is a set theory whose signature contains two primitive symbols: the membership symbol $\in$ from ZFC (which is a binary relation symbol), and a unary partial function symbol $\st$ called the internalizer. Every axiom of ZFC is an axiom of *ZFC, except for the axiom of foundation, and every axiom scheme of ZFC is an axiom scheme of *ZFC, with no restrictions on the formulas with which the scheme may be instantiated (so that they may contain the $\st$ symbol). *ZFC also has a number of extra axioms describing the properties of the internalizer, the most important one being the transfer axiom. Before I state these axioms, some preliminary definitions are required:
Axiom 1 (Transfer). An $\in$-formula $\varphi$ with E-standard parameters holds in $\Vni$ if and only if $\st \varphi$ holds in $\Ini$.
The process of passing from $\varphi^\Vni$ to $\st \varphi^\Ini$ or vice versa, which this axiom asserts preserves truth, is called applying transfer.
Although transfer applies only to $\in$-formulas, strictly speaking, we will often apply it implicitly to formulas containing relation and function symbols defined in terms of $\in$, by replacing references to those symbols by equivalent subformulas containing only $\in$.
Here are two simple examples of how transfer can be used in a proof.
Theorem 1. Every I-standard set is internal.
Proof. Suppose $A \in \Vni$. Then $\{A\}$ is also E-standard and contains $A$. Applying transfer to the formula $A \in \{A\}$ yields $\st A \in \st \{A\}$. It follows that $\st A$ is internal. $\blacksquare$
Theorem 2. For every E-standard set $X$, the image of $X$ under the internalizer is a subset of $\st X$.
Proof. Suppose $X \in \Vni$ and $A \in X$. Then $A$ is also E-standard. Applying transfer to the formula $A \in X$ yields $\st A \in \st X$. $\blacksquare$
Many applications of transfer make some use of the axiom below, as well as transfer proper.
Axiom 2. Members of internal sets are internal.
The point of Axiom 2 is this. Suppose $\varphi$ is an $\in$-formula with E-standard parameters and $A$ is one of those parameters. If $\varphi$ contains a quantifier ranging over the members of $A$, then applying transfer to $\varphi^\Vni$ makes the quantifier range only over the internal members of $A$. But because $A$ is standard, and hence internal, each of its members is internal by Axiom 2; so the quantifier still has the same effective range as in $\varphi$.
In particular, if every quantifier in $\varphi$ ranges only over the members of one of the parameters of $\varphi$, then by transfer, we have $\varphi^\Vni$ if and only if $\st \varphi$.
We can now prove that the internalizer behaves nicely with respect to the familiar set operations.
To prove that for every pair of standard sets $A$ and $B$, we have $\st \{A, B\} = \{\st A, \st B\}$, apply transfer to the formula \begin{equation*} (\forall^\Vni C)(C \in \{A, B\} \Leftrightarrow C = A \vee C = B). \end{equation*} Using the consequence of Axiom 2 described above, this yields \begin{equation*} (\forall C)(C \in \st \{A, B\} \Leftrightarrow C = \st A \vee C = \st B), \end{equation*} so the members of $\st \{A, B\}$ are $\st A$ and $\st B$. The other proofs are similar. I'm not proving them here because it gets tedious.
Another important thing to note, which is tedious but not difficult to prove, is that Theorem 2 can be generalized to arbitrary algebraic structures: for every algebraic structure $X$ whose underlying set, relations and functions are all E-standard, the restriction of the internalizer to $X$ is a monomorphism from the $X$ to the $\st X$ (the structure resulting from internalizing the underlying set and all the relations and functions of $X$). This means that $X$ can be identified with the range of this restriction.
Now, let's forget about nonstandard analysis for a moment. For this section, suppose $X$ is an ordered field.
Definition 1. An $x \in X$ is finite if it is between two integers, and infinite otherwise.
Proposition 1. An $x \in X$ is finite if and only if it is smaller in magnitude than some integer, and infinite if and only if it is larger in magnitude than every integer.
Proposition 2. Every rational number is finite.
Theorem 1. The set of the finite members of $X$ is a subring of $X$.
Proof. Let $A$ be the set of the finite members of $X$. Then $\QQ \subseteq A$, so $A$ is nonempty. Suppose $x$ and $y$ are members of $A$. Then there are integers $m$ and $n$ such that $|x| < m$ and $|y| < n$. Adding the inequalities, we have $|x + y| \le |x| + |y| < m + n$, so $x + y \in A$. Multiplying the inequalities, we have $|xy| = |x||y| < mn$, so $xy \in A$. $\blacksquare$
Theorem 2. The set of the finite members of $X$ is an interval.
Proof. Suppose $x$, $y$, $z$ are members of $X$, $x$ and $z$ are finite and $x < y < z$. Then there are integers $m$ and $n$ such that $m < x$ and $z < n$. By transitivity, it follows that $m < y < n$ and hence $y$ is finite. $\blacksquare$
Definition 2. For every $x \in X$, the galaxy $\gal x$ (or $\gal_X(x)$, if we want to specify the ordered field) of $x$ is the additive coset with respect to $x$ of the set of the finite members of $X$, and finite closeness $\sim$ is the equivalence relation associated with these cosets.
Proposition 3. The galaxy of 0 is the set of the finite members of $X$, and an $x \in X$ is finite if and only if $x \sim 0$. Also, every galaxy is an interval (because every galaxy is a translate of $\gal 0$).
Definition 3. An $x \in X$ is (an) infinitesimal if it is smaller in magnitude than every positive rational number.
Proposition 4. Zero is infinitesimal, and a nonzero $x \in X$ is infinitesimal if and only if its reciprocal is infinite.
Proposition 5. No nonzero rational number is infinitesimal.
Theorem 3. The set of the infinitesimals in $X$ is an ideal of $\gal 0$.
Proof. Let $A$ be the set of the infinitesimals in $X$. Then $0 \in A$, so $A$ is nonempty. Suppose $\varepsilon$ is a positive rational number. For every pair of members $x$ and $y$ of $A$, both $|x|$ and $|y|$ are less than $\varepsilon/2$ and hence $|x + y| \le |x| + |y| < \varepsilon$, so $x + y \in A$. And for every $x \in A$ and every finite $a \in X$, there is a positive integer $n$ such that $|a| < n$; because $x$ is infinitesimal, we have $|x| < \varepsilon/n$ and hence $|ax| = |a||x| < n|x| < \varepsilon$, so $ax \in A$. $\blacksquare$
Theorem 2. The set of the infinitesimals in $X$ is an interval.
Proof. Suppose $x$, $y$, $z$ are members of $X$, $x$ and $z$ are infinite, $x < y < z$ and $\varepsilon$ is a positive rational number. Then $-\varepsilon < x$ and $z < \varepsilon$. By transitivity, it follows that $-\varepsilon < y < \varepsilon$, i.e. $|y| < \varepsilon$, and hence $y$ is infinitesimal. $\blacksquare$
Definition 4. For every $x \in X$, the monad $\mon x$ (or $\mon_X(x)$, if we want to specify the ordered field) of $x$ is the additive coset with respect to $x$ of the set of the infinitesimals in $X$, and infinite closeness $\approx$ is the equivalence relation associated with these cosets.
Proposition 6. The monad of 0 is the set of the infinitesimals in $X$, and an $x \in X$ is infinitesimal if and only if $x \approx 0$. Also, every monad is an interval (because every monad is a translate of $\mon 0$).
For finite members of $X$, there is a useful alternative characterization of infinite closeness.
Theorem 5. Every finite member of $X$ can be approximated to arbitrarily small rational error on both sides by rational numbers.
Proof. Suppose $x \in \gal 0$ and $\varepsilon$ is a positive rational number. Then there are integers $a$ and $b$ such that $a < x < b$. Let $n$ be an integer greater than $(b - a)/\varepsilon$, let $h = (b - a)/n$ and for every $k \in \{0, \dotsc, n\}$, let $c_k = a + kh$. Note that $h < \varepsilon$, \begin{equation*} a = c_0 < c_1 < \dotso < c_{n - 1} < c_n = b, \end{equation*} and every term in the inequality above is rational. Let $i$ be the largest member of $\{0, \dotsc, n\}$ possible such that $c_i < x$ and let $j$ be the smallest member of $\{0, \dotsc, n\}$ possible such that $x < c_j$. Then $i \ne n$ (otherwise $b < x$) and $j \ne 0$ (otherwise $x < a$), so $x \le c_{i + 1}$ and $c_{j - 1} \le x$. Therefore \begin{equation*} x - \varepsilon < c_{i + 1} - h = c_i < x < c_j < c_{j - 1} + h < x + \varepsilon. \end{equation*} $\blacksquare$
Theorem 6. A finite $x \in X$ is infinitely close to a $y \in X$ if and only if for every pair of rational numbers $a$ and $b$ not infinitely close to $x$ such that $a < x < b$, we have $a < y < b$.
Proof. Suppose $x$ and $y$ are members of $X$ and $x$ is finite.
First, suppose $x \approx y$, $a$ and $b$ are rational numbers not infinitely close to $x$, and $a < x < b$. Then $x - a$ and $b - x$ are not infinitesimal, so there are positive rational numbers $r$ and $s$ such that $\varepsilon < x - a$ and $\delta < b - x$. Because $x - y$ is infinitesimal, it is smaller in magnitude than both $\varepsilon$ and $\delta$, and hence \begin{equation*} a = x - (x - a) < x - \varepsilon < y < x + \delta < x + (b - x) = b. \end{equation*}
Second, suppose that for every pair of rational numbers $a$ and $b$ not infinitely close to $x$ such that $a < x < b$, we have $a < y < b$; and suppose $\varepsilon$ is a positive rational number. By Theorem 5, there are rational numbers $r$ and $s$ such that \begin{equation*} x - \varepsilon < r < x < s < x + \varepsilon. \end{equation*} Neither $x - \varepsilon$ nor $x + \varepsilon$ is infinitely close to $x$ (because $\varepsilon$ is not infinitesimal); therefore we have $x - \varepsilon < y < x + \varepsilon$, i.e. $|x - y| < \varepsilon$. $\blacksquare$
Definition 4. An ordered field $X$ is Archimedean if each of its members is finite.
Proposition 7. For every ordered field $X$, the statements below are equivalent.
Definition 5. For every Archimedean ordered field $X$ and every $x \in X$, the integer part $[x]$ of $x$ is the greatest integer less than or equal to $x$.
Proposition 8. The ordered field $\QQ$ is Archimedean.
Axiom 1. The ordered field $\st \QQ$ is non-Archimedean.
Remark 1. This does not contradict the transfer principle because the assertion “$\QQ$ is Archimedean” unpacks to “every member of $\QQ$ is between two integers”, and applying transfer to this yields “every member of $\st \QQ$ is between two hyperintegers”, not “every member of $\st \QQ$ is between two integers”.
Definition 5. For every ordered field $X$, the monad field of $X$ is the quotient ordered field of $\mon_X(0)$ in $\gal_X(0)$, and $\mon_X$ is the associated field epimorphism (i.e. the function $f$ on $\gal_X(0)$ such that for every $x \in \gal_X(0)$, we have $f(x) = \mon_X(x)$).
Remark 1. The quotient has a field structure because $\mon_X(0)$ is an ideal of $\gal_X(0)$, and it can be ordered because $\mon_X(0)$ is an interval.
Proposition 9. For every ordered field $X$:
Theorem 7. Monad fields are Archimedean.
Proof. Suppose $X$ is an ordered field, let $Y$ be its monad field and suppose $A \in Y$. Then there is an $x \in \gal_X(0)$ such that $A = \mon_X(x)$. Because $x$ is finite in $X$, there are rational numbers $a$ and $b$ such that $a < x < b$. If $a \approx x$, replace $a$ with $a - 1$; if $x \approx b$, replace $b$ with $b + 1$. Then $a < x < b$ still holds, but $a \not \approx x \not \approx b$ and hence $\mon_X(a) < A < \mon_X(b)$ holds in $Y$. Because we can identify $\mon_X(a)$ and $\mon_X(b)$ with $a$ and $b$ respectively, it follows that $Y$ is Archimedean. $\blacksquare$
Definition 5. The ordered field $\RR$ is the monad field of $\st \QQ$, the real numbers are the members of $\RR$, and the hyperreal numbers are the members of $\st \RR$.
Let $f$ be the internalization of $\mon_{\st \QQ} \tril \QQ$. By transfer, this function is an ordered field monomorphism from $\st \QQ$ to $\st \RR$, so we can identify $\st \QQ$ with the range of $f$.
Given this identification, for every $x \in \QQ$, we can identify $f(x)$ with $\mon_{\st \QQ}(x)$. However, $f$ does not coincide with $\mon_{\st \QQ}$ on $\st \QQ$ as a whole! Theorem 8 describes the relationship between the two functions.
Theorem 8. For every finite hyperrational number $x$, we have $\mon_X(x) \approx x$ (given the identification made in Proposition 10).
Proof. Suppose $x$ is a finite hyperrational number, let $a = \mon_{\st \QQ}(x)$ and suppose $r$ and $s$ are rational numbers not infinitely close to $x$ and $r < x < s$. Let $f = \st (\mon_{\st \QQ} \tril \QQ)$. Then $f(r) = \mon_{\st \QQ}(r)$ and $f(s) = \mon_{\st \QQ}(s)$, so by Proposition 9, we can identify $r$ and $s$ with their values under $f$. Because $f$ is order-preserving, it follows that $r < a < s$. Therefore, by Theorem 6, we have $x \approx a$. $\blacksquare$
Theorem 9. Every hyperreal number is infinitely close to a hyperrational number.
Proof. Suppose $x \in \st \RR$ and let $n$ be an infinite hypernatural number. Then \begin{equation*} \frac {\lfloor nx \rfloor} n - x = \frac {\lfloor nx \rfloor - nx} n < \frac 1 n \approx 0, \end{equation*} and $\lfloor nx \rfloor/n$ is rational.
Remark 3. The floor function on $\st \RR$ referred to in this proof is the natural extension of the floor function on $\RR$ (which is well-defined because $\RR$ is Archimedean). It has the same properties as the floor function on $\RR$, by transfer.
Theorem 10 (Leibniz Completeness). Every finite hyperreal number is infinitely close to a real number.
Proof. Suppose $x \in \gal_{\st \RR}(0)$. By Theorem 9, there is an $r \in \st \QQ$ infinitely close to $x$. Therefore, by Theorem 8, we have $x \approx r \approx \mon_{\st \QQ}(r)$.
Remark 4. Because $\RR$ is Archimedean, every finite hyperreal number is infinitely close to exactly one real number.
Definition 6. For every $x \in \gal_{\st \RR}(0)$, the shadow $\sh x$ of $x$ is the unique real number infinitely close to $x$.
In order to convince you that the real numbers as constructed here are isomorphic to the real numbers as constructed normally, I shall prove the Cauchy completeness of the real numbers as constructed here.
Definition 7. A real-valued sequence $x$ is Cauchy if all the hyperreal numbers of the form $\st x(n)$, where $n$ is an infinite hypernatural number, are infinitely close.
Theorem 11. A real-valued sequence $x$ is Cauchy if and only if for every positive $\varepsilon \in \RR$, there is a positive integer $m$ such that for every pair of integers $p$ and $q$ greater than $m$, we have $|x(p) - x(q)| < \varepsilon$. $\blacksquare$
Proof. Suppose $x$ is a real-valued sequence.
First, suppose $x$ is Cauchy and $\varepsilon$ is a positive real number. Let $m$ be an infinite hypernatural number. Then for every pair of hyperintegers $p$ and $q$ greater than $m$, we have $\st x(p) \approx \st x(q)$ and hence $|\st x(p) - \st x(q)| < \varepsilon$. By transfer, it follows that there is a positive integer $m$ such that for every pair of integers $p$ and $q$ greater than $m$, we have $|x(p) - x(q)| < \varepsilon$. $\blacksquare$
Second, suppose that for every positive $\varepsilon \in \RR$, there is a positive integer $m$ such that for every pair of integers $p$ and $q$ greater than $m$, we have $|x(p) - x(q)| < \varepsilon$; and suppose $p$ and $q$ are infinite hypernatural numbers. For every positive $\varepsilon \in \RR$, we have by transfer that there is a positive hyperinteger $m$ such that for every pair of hyperintegers $P$ and $Q$ greater than $m$, we have $|x(P) - x(Q)| < \varepsilon$. In particular, $|x(p) - x(q)| < \varepsilon$. This holds whatever $\varepsilon$ is, so it follows that $x(p) \approx x(q)$. $\blacksquare$
Definition 8. A real-valued sequence $x$ is bounded if for every infinite hypernatural number $n$, we have $\st x(n) \sim 0$.
Theorem 12. Every Cauchy real-valued sequence is bounded.
Proof. Suppose $x$ is a Cauchy real-valued sequence. Then there is a positive integer $m$ such that for every pair of integers $p$ and $q$ greater than $m$, we have $|x(p) - x(q)| < 1$. In particular, for every integer $n > m$, we have $|x(n) - x(m + 1)| < 1$. By transfer, it follows that for every hyperinteger $n > m$, we have $|\st x(n) - x(m + 1)| < 1$ and hence $\st x(n) \sim x(m + 1) \sim 0$. $\blacksquare$
Definition 9. For every real-valued sequence $x$, the limit of $x$ is the common shadow of the hyperreal numbers of the form $\st x(n)$, where $n$ is an infinite hypernatural number, if this common shadow exists.
Theorem 14 (Cauchy Completeness). A real-valued sequence has a limit if and only if it is Cauchy.
Proof. Suppose $x$ is a real-valued sequence.
If $x$ has a limit $a$, then for every pair of infinite hypernatural numbers $m$ and $n$, we have $\st x(m) \approx a \approx \st x(n)$. Therefore $x$ is Cauchy.
If $x$ is Cauchy, then all the hyperreal numbers of the form $\st x(n)$, where $n$ is an infinite hypernatural number, are infinitely close. Because $x$ is bounded, they are also finite. It follows that they have a common shadow. $\blacksquare$
Theorem 13. For every real-valued sequence $x$, an $a \in \RR$ is a limit of $x$ if and only if for every positive $\varepsilon \in \RR$, there is a positive integer $m$ such that for every integer $n > m$, we have $|x(n) - a| < \varepsilon$.
Proof. Suppose $x$ is a real-valued sequence.
First, suppose $a$ is a limit of $x$ and $\varepsilon$ is a positive real number. Let $m$ be an infinite hypernatural number. Then for every hyperinteger $n > m$, we have $\st x(n) \approx a$ and hence $|\st x(n) - a| < \varepsilon$. By transfer, it follows that there is a positive integer $m$ such that for every integer $n > m$, we have $|x(n) - a| < \varepsilon$.
Second, suppose that for every positive $\varepsilon \in \RR$, there is a positive integer $m$ such that for every integer $n > m$, we have $|x(n) - a| < \varepsilon$; and suppose $n$ is an infinite hypernatural number. For every positive $\varepsilon \in \RR$, we have by transfer that there is a positive hyperinteger $m$ such that for every hyperinteger $N > m$, we have $|\st x(N) - a| < \varepsilon$. In particular, $|\st x(n) - a| < \varepsilon$. This holds whatever $\varepsilon$ is, so it follows that $\st x(n) \approx a$. $\blacksquare$