论不可数性的数学与基础意义

我们研究不可数数学基本定理的逻辑与计算性质，包括 1895 年和 1903 年发表的 Cousin 引理和 Lindelöf 引理。历史上，这些引理分别是开覆盖紧致性和 Lindelöf 性质的最早表述之一。这些概念具有重大的概念重要性：前者通常被视为将不可数集（如 $[0,1]$）当作“几乎有限”来对待的一种方式，而后者允许将不可数集（如 $\mathbb{R}$）当作“几乎可数”来对待。这种将不可数归约为有限/可数的做法被证明具有相当大的逻辑与计算代价：我们证明上述引理及许多相关定理极难证明，而相关的子覆盖极难计算。事实上，就标准尺度（基于理解公理）而言，这些引理的证明至少需要二阶算术的全部范围，该系统源自 Hilbert-Bernays 的《数学基础》（Grundlagen der Mathematik）。这一观察对《数学基础》的精神继承者——逆向数学（Reverse Mathematics）程序及相关的 Gödel 层级具有深远影响。我们还证明 Cousin 引理对于规范积分的发展至关重要，规范积分是 Lebesgue 积分和广义 Riemann 积分的推广，也唯一地提供了 Feynman 路径积分的直接形式化。