Measure theory and higher order arithmetic
Alexander Kreuzer · Proceedings of the American Mathematical Society · 2015
We investigate the statement that the Lebesgue measure defined on all subsets of the Cantor-space exists. As a base system we take $\textsf {ACA}_0^\omega +(\mu )$. The system $\textsf {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 {n} f(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 reason $\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 ^1_2$-conservative over $\mathsf {ACA_0}^\omega$ and with this conservative over $\mathsf {PA}$. Moreover, we establish a corresponding program extraction result.