Measure theory and higher order arithmetic

Abstract

We investigate the statement that the Lebesgue measure defined on all subsets of the Cantor space exists. As base system we take ${\mathsf{ACA}}_0^{\omega }+(\mu )$. The system ${\mathsf{ACA}}_0^{\omega }$ is the higher order extension of Friedman's system ${\mathsf{ACA}}_0$, and $(\mu )$ denotes Feferman's $\mu$, that is a uniform functional for arithmetical comprehension defined by $f(\mu (f))=0$ if $\exists nf(n)=0$ for $f\in {\mathbb{N}}^{\mathbb{N}}$. Feferman's $\mu$ will provide countable unions and intersections of sets of reals and is, in fact, equivalent to this. For this reasons ${\mathsf{ACA}}_0^{\omega }+(\mu )$ is the weakest fragment of higher order arithmetic where $\sigma$-additive measures are directly definable. We obtain that over ${\mathsf{ACA}}_0^{\omega }+(\mu )$ the existence of the Lebesgue measure is ${\Pi }_2^1$-conservative over ${\mathsf{ACA}}_0^{\omega }$ and with this conservative over $\mathsf{PA}$. Moreover, we establish a corresponding program extraction result.

References in corpus (2)

• Local stability of ergodic averages
• Algorithmic randomness, reverse mathematics, and the dominated convergence theorem