逆向数学中的“大”问题：实数集的不可数性

$\mathbb{R}$ 的不可数性是其最基本的性质之一，在数学之外也广为人知。Cantor 于 1874 年对 $\mathbb{R}$ 不可数性的证明甚至出现在第一篇集合论论文中，即一个历史里程碑。本文在 Kohlenbach 的高阶逆向数学（简称 RM）中研究 $\mathbb{R}$ 的不可数性，以如下原理形式呈现：$$\hbox{对可数集 $A\subset \mathbb{R}$，存在 $y\in \mathbb{R}\setminus A$。}$$ 一个重要的概念性观察是，通常基于到 $\mathbb{N}$ 的入射或双射的可数集定义，似乎不适合对主流数学的 RM 研究；我们还提出了一种合适的（在强系统下等价）可数集替代定义，即有限集在 $\mathbb{N}$ 上的并；后者见于文献且更贴近可数集“在野外”出现的方式。我们识别出大量基于该替代定义的与中心定理等价的定理。或许令人惊讶，我们的等价定理涉及 Riemann 积分的最基本性质、受调函数或有界变差函数、Blumberg 定理以及 Volterra 约 1881 年的早期工作。我们的等价关系也具有鲁棒性，将 $\mathbb{R}$ 的不可数性提升为 RM 中“大”系统的地位。