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

m a t h s f {A C A}_{0}^{o} m e g a + (m u)

. The system

m a t h s f {A C A}_{0}^{o} m e g a

is the higher order extension of Friedman's system

m a t h s f {A C A}_{0}

, and

(m u)

denotes Feferman's

m u

, that is a uniform functional for arithmetical comprehension defined by

f (m u (f)) = 0

if

e x i s t s n f (n) = 0

for

f i n m a t h b b N^{m} a t h b b N

. Feferman's

m u

will provide countable unions and intersections of sets of reals and is, in fact, equivalent to this. For this reasons

m a t h s f {A C A}_{0}^{o} m e g a + (m u)

is the weakest fragment of higher order arithmetic where

s i g m a

-additive measures are directly definable. We obtain that over

m a t h s f {A C A}_{0}^{o} m e g a + (m u)

the existence of the Lebesgue measure is

P i_{2}^{1}

-conservative over

m a t h s f {A C A}_{0}^{o} m e g a

and with this conservative over

m a t h s f P A

. Moreover, we establish a corresponding program extraction result.

Recommendations

Cites work

Cited in

(9)

This page was built for publication: Measure theory and higher order arithmetic