  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 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 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^1_2$-conservative over $\mathsf{ACA}_0^\omega$ and
with this conservative over $\mathsf{PA}$. Moreover, we establish a
corresponding program extraction result.
