测度论与高阶算术

我们研究了定义在 Cantor 空间所有子集上的 Lebesgue 测度存在的命题。作为基础系统，我们采用 $\mathsf{ACA}_0^\omega + (\mu)$。系统 $\mathsf{ACA}_0^\omega$ 是 Friedman 系统 $\mathsf{ACA}_0$ 的高阶扩展，$(\mu)$ 表示 Feferman 的 $\mu$，即一个用于算术 comprehension 的一致泛函，定义为：若 $\exists n f(n)=0$ 则 $f(\mu(f))=0$，其中 $f\in \mathbb{N}^\mathbb{N}$。Feferman 的 $\mu$ 将提供实数集的可数并和交，事实上与此等价。出于这些原因，$\mathsf{ACA}_0^\omega + (\mu)$ 是可直接定义 $\sigma$-可加测度的高阶算术的最弱片段。我们得出，在 $\mathsf{ACA}_0^\omega + (\mu)$ 之上，Lebesgue 测度的存在性相对于 $\mathsf{ACA}_0^\omega$ 是 $\Pi^1_2$-保守的，因此相对于 $\mathsf{PA}$ 也是保守的。此外，我们建立了一个相应的程序提取结果。