Cauchy Sequences, Dedekind Cuts and Real Numbers

Intuitive Concept of Real Numbers

The definition of real numbers that we learned in high school "seems" to be:

$$ \mathbb{R} = \mathbb{Q} \cup \text{irrational numbers} $$

where irrational numbers are defined as:

• Irrational numbers are non-repeating infinite decimals

or

• Irrational numbers are numbers that cannot be expressed as fractions

However, we quickly find that to show a number is a "non-repeating infinite decimal" requires observing infinitely many digits. Even if you don't observe any repetition in a finite number of digits, you can't conclude there won't be repetition in more digits. In fact, the "decimal" representation is not very suitable for proving things¹.

On another side, if we define irrational numbers as numbers that cannot be expressed as fractions, this definition becomes incorrect after introducing imaginary numbers.

Furthermore, these two definitions don't reveal any internal structure of irrational numbers, or a universal way to construct (any) irrational number², and real numbers defined as the union of rational and irrational numbers inherit the drawbacks of these two definitions.

Therefore, a better definition of real numbers is necessary.³

Definition of Real Numbers

Real numbers have many different ways of definition. We will introduce the two most commonly used methods, Dedekind cuts and Cauchy sequences.

Dedekind Cuts

An easier to understand definition is using Dedekind cuts to define real numbers.

We divide rational numbers $\mathbb{Q}$ into two disjoint non-empty sets $L$ and $R$, requiring:

• $q ∈ L ⇔ ∃(r ∈ Q). q < r ∧ r ∈ L$, more intuitively, for any element in $L$, we can find an element in $L$ that is greater than it, conversely if for a rational number, we can find a rational number in $L$ that is greater than it, then it is in $L$.
• $r ∈ U ⇔ ∃(q ∈ Q). q < r ∧ q ∈ U$, more intuitively, for any element in $R$, we can find an element in $R$ that is less than it, conversely if for a rational number, we can find a rational number in $R$ that is less than it, then it is in $R$.
• For rational numbers $a$ and $b$, if $a < b$, then $a ∈ L$ or $b ∈ R$

The sets $A$ and $B$ obtained in this way are Dedekind cuts of $\mathbb{Q}$, each such cut represents a real number, and the maximum/minimum elements in $L$ and $R$ are infinitely close to the real number it represents.

Example

Take $L= \{x | x \in \mathbb{Q}, x^2 < 2\}$, $R = \{x | x \in \mathbb{Q}, x^2 > 2\}$, then $L$ and $R$ form a Dedekind cut of $\mathbb{Q}$.

The real number corresponding to this cut is $\sqrt{2}$.

Formalization

The real numbers in Agda's unimath library are defined using Dedekind cuts.

Of course, since unimath uses HoTT rather than set theory as its foundation, there are some subtle differences in the definition (like using subtype instead of subset), but the main idea is the same.

Cauchy Sequences

A definition requiring more prerequisite knowledge is defining real numbers through Cauchy sequences.

For a metric space (simply understood as a space that defines the concept of "distance"), we define a sequence of rational numbers

$$ x_0, x_1, \cdots, x_n, \cdots $$

as a (rational) Cauchy sequence if for any positive number $\epsilon$, there exists a natural number $N$, such that for all $i,j \geq N$, we have $|x_i - x_j| < \epsilon$.

Taking $\mathbb{Q}$ as the metric space, there exist some Cauchy sequences that converge to values not in $\mathbb{Q}$, for example:

$$ x_0 = 0 $$ $$ x_{n+1} = \frac{x_n + \frac{2} {x_n}} {2} $$

We can see that this sequence converges to $\sqrt{2}$, but this number is not in $\mathbb{Q}$.

By adding these numbers that sequences converge to into $\mathbb{Q}$, we have completed $\mathbb{Q}$, and the new set obtained is the set of real numbers.

Every real number corresponds to at least one Cauchy sequence.

Equivalence of Cauchy Sequences

We define two Cauchy sequences to be equivalent if they converge to the same value.

For example, $a_n = 1$ and $a_n​=1−10^{−n}$ are equivalent because they converge to the same value, both sequences correspond to the real number $1$.

This also provides a definition-level proof that $1 = 0.\dot{9}$.

Formalization

The real numbers in Lean4 Mathlib are defined using Cauchy sequences.

Another important related definition is Cauchy completion.

Equivalence of the Two Definitions

$A=\{r∈Q | \exists n, r<q_n\}$ is the Dedekind cut (the smaller part) corresponding to the Cauchy sequence $q_n$.

Obviously, $A$ satisfies the conditions of a Dedekind cut.

Conversely, if we have a Dedekind cut $A$ with supremum (i.e., the real number it represents) $s$, we can definitely⁴ construct a sequence $q_n$ where $s - q_n < \frac{1} n$, and $q_n$ is a Cauchy sequence converging to $s$.