柯西序列，戴德金分割和实数

实数的直观概念

我们中学学到的实数定义"似乎"是：

$$ \mathbb{R} = \mathbb{Q} \cup \text{无理数} $$

其中无理数的定义是：

• 无理数是无限不循环小数

或者

• 无理数是不能被表示为分数的数

然而，我们很快会发现要说明一个数是"无限不循环小数"需要观察无限多位，即使你在有限位上没有观察到循环，也不能说明在更多位上就没有循环了， 实际上，"小数"这个表示形式就是很不适合用来证明东西的¹。

另一个方面，我们将无理数定义成不能被表示为分数的数，那么之后引入虚数之后，这个定义就不对了。

此外，这两种定义没有揭示任何无理数的内部结构，或者一个通用的构造出（任意一个）无理数的方式²，而利用有理数和无理数的并定义出的 实数也继承了这两种定义的缺点。

因此，一个更好用的实数的定义是必要的。³

实数的定义

实数有非常之多的定义方式。 我们将介绍其中最常用的两种方式，戴德金分割和柯西序列。

戴德金分割

较为容易理解的定义方式是使用戴德金分割来定义实数。

我们将有理数 $\mathbb{Q}$ 分成两个不相交的非空集合 $L$ 和 $R$，要求

• $q ∈ L ⇔ ∃(r ∈ Q). q < r ∧ r ∈ L$，更直观的说法是，对 $L$ 中的任何一个元素，都能在 $L$ 中找到一个大于它的元素， 反之如果对于某一个有理数，在 $L$ 中能找到一个大于它的有理数，那么它就在 $L$ 中。
• $r ∈ U ⇔ ∃(q ∈ Q). q < r ∧ q ∈ U$, 更直观的说法是，对 $R$ 中的任何一个元素，都能在 $R$ 中找到一个小于它的元素， 反之如果对于某一个有理数，在 $R$ 中能找到一个小于它的有理数，那么它就在 $R$ 中。
• 若对有理数 $a$ 和 $b$， $a < b$，则 $a ∈ L$ 或 $b ∈ R$

通过这种方式取得的集合 $A$ 和 $B$ 就是对 $\mathbb{Q}$ 的戴德金分割，每一个这样的分割表示了一个实数，$L$ 和 $R$ 中 最大/最小的元素都无限接近它所代表的这个实数。

例子

取 $L= \{x | x \in \mathbb{Q}, x^2 < 2\}$，$R = \{x | x \in \mathbb{Q}, x^2 > 2\}$，则 $L$ 和 $R$ 是对 $\mathbb{Q}$ 的戴德金分割。

这个分割对应的实数就是 $\sqrt{2}$。

Formalization

Agda 的 unimath 库中的实数使用戴德金分割来定义。

当然，由于 unimath 使用的 foundation 不是集合论而是 HoTT，定义有些许细微的差别（例如使用 subtype 而非子集），但大体思想还是一样的。

柯西序列

一个需要更多前置知识的定义方式是通过柯西序列来定义实数。

对于一个度量空间（简单理解就是定义了“距离”这个概念的空间），我们定义有理数一个序列

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

为一个（有理数上的）柯西序列，如果对于任意正数 $\epsilon$，有自然数 $N$，使得对所有 $i,j \geq N$ 有 $|x_i - x_j| < \epsilon$。

取 $\mathbb{Q}$ 这个度量空间，存在一些柯西序列，其收敛到的值不在 $\mathbb{Q}$ 中，例如：

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

我们可以看出来这个序列是收敛到 $\sqrt{2}$ 的，但这个数并不在 $\mathbb{Q}$ 中。

通过往 $\mathbb{Q}$ 中添加这些序列收敛到的数，我们将 $\mathbb{Q}$ 完备化 了，得到的这个新的集合就是实数集合。

每一个实数都能对应到至少一个柯西序列。

柯西序列的等价

我们定义两个柯西序列的等价为如果两个序列收敛到同一个值，则这两个序列等价。

比如，$a_n = 1$ 和 $a_n​=1−10^{−n}$ 是等价的，因为它们收敛到同一个值，这两个序列对应的都是实数 $1$。

这也是 $1 = 0.\dot{9}$ 从定义上就可以得到的证明。

Formalization

Lean4 Mathlib 中的实数使用柯西序列来定义。

相关的重要那个定义还有柯西完备化。

两个定义的等价性

$A=\{r∈Q | \exists n, r<q_n\}$ 为柯西序列 $q_n$ 对应的戴德金分割（中的比较小的那部分）。

显然 $A$ 符合戴德金分割的条件。

反之，如果有一个戴德金分割 $A$，其上确界（即其代表的实数）为 $s$， 我们一定能⁴构造出一个序列 $q_n$，其中 $s - q_n < \frac{1} n$， 且 $q_n$ 是一个趋向于 $s$ 的柯西序列。