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^ω+ (μ)$. The system $\mathsf{ACA}_0^ω$ is the higher order extension of Friedman's system $\mathsf{ACA}_0$, and $(μ)$ denotes Feferman's $μ$, that is a uniform functional for arithmetical comprehension defined by $f(μ(f))=0$ if $\exists n f(n)=0$ for $f\in \mathbb{N}^\mathbb{N}$. Feferman's $μ$ will provide countable unions and intersections of sets of reals and is, in fact, equivalent to this. For this reasons $\mathsf{ACA}_0^ω+ (μ)$ is the weakest fragment of higher order arithmetic where $σ$-additive measures are directly definable. We obtain that over $\mathsf{ACA}_0^ω+ (μ)$ the existence of the Lebesgue measure is $Π^1_2$-conservative over $\mathsf{ACA}_0^ω$ and with this conservative over $\mathsf{PA}$. Moreover, we establish a corresponding program extraction result.