VITALI’S THEOREM AND WWKL

DOUGLAS K. BROWN MARIAGNESE GIUSTO STEPHEN G. SIMPSON

Abstract. Continuing the investigations of X. Yu and others, we study the role of set existence axioms in classical Lebesgue measure theory. We show that pairwise disjoint countable additivity for open sets of reals is provable in RCA_{0}. We show that several well-known measure-theoretic propositions including the Vitali Covering Theorem are equivalent to WWKL over RCA_{0}.

1. Introduction

The purpose of Reverse Mathematics is to study the role of set existence axioms, with an eye to determining which axioms are needed in order to prove specific mathematical theorems. In many cases, it is shown that a specific mathematical theorem is equivalent to the set existence axiom which is needed to prove it. Such equivalences are often proved in the weak base theory RCA_{0}. RCA_{0} may be viewed as a kind of formalized constructive or recursive mathematics, with full classical logic but severely restricted comprehension and induction. The program of Reverse Mathematics has been developed in many publications; see for instance [5, 10, 11, 12, 20].

In this paper we carry out a Reverse Mathematics study of some aspects of classical Lebesgue measure theory. Historically, the subject of measure theory developed hand in hand with the nonconstructive, set-theoretic approach to mathematics. Errett Bishop has remarked that the foundations of measure theory present a special challenge to the constructive mathematician. Although our program of Reverse Mathematics is quite different from Bishop-style constructivism, we feel that Bishop’s remark implicitly raises an interesting question: Which nonconstructive set existence axioms are needed for measure theory?

Date: October 25, 1998.

1991 Mathematics Subject Classification. 03F35, 03F60, 03B30.

Giusto’s research was partially supported by Funds 40% of MURST of Italy.

Simpson’s research was partially supported by NSF grant DMS-9303478.

Accepted April 17, 1998 for Archive for Mathematical Logic.

This paper, together with earlier papers of Yu and others [21, 22, 23, 24, 25, 26], constitute an answer to that question.

The results of this paper build upon and clarify some early results of Yu and Simpson. The reader of this paper will find that familiarity with Yu–Simpson [26] is desirable but not essential. We begin in section 2 by exploring the extent to which measure theory can be developed in RCA_{0}. We show that pairwise disjoint countable additivity for open sets of reals is provable in RCA_{0}. This is in contrast to a result of Yu– Simpson [26]: countable additivity for open sets of reals is equivalent over RCA_{0} to a nonconstructive set existence axiom known as Weak Weak König’s Lemma (WWKL). We show in sections 3 and 4 that several other basic propositions of measure theory are also equivalent to WWKL over RCA_{0}. Finally in section 5 we show that the Vitali Covering Theorem is likewise equivalent to WWKL over RCA_{0}.

2. Measure Theory in RCA_{0}

Recall that RCA_{0} is the subsystem of second order arithmetic with Δ_{1}^{0} comprehension and Σ_{1}^{0} induction. The purpose of this section is to show that some measure-theoretic results can be proved in RCA_{0}.

Within RCA_{0}, let X be a compact separable metric space. We define C(X) = Â, the completion of A, where A is the vector space of rational “polynomials” over X under the sup-norm, ∥f∥ = sup_{x∈X} |f(x)|. For the precise definitions within RCA_{0}, see [26] and section III.E of Brown’s thesis [4]. The construction of C(X) within RCA_{0} is inspired by the constructive Stone–Weierstrass theorem in section 4.5 of Bishop and Bridges [2]. It is provable in RCA_{0} that there is a natural one-to-one correspondence between points of C(X) and continuous functions f : X → ℝ which are equipped with a modulus of uniform continuity, that is to say, a function h : ℕ → ℕ such that for all n ∈ ℕ and x, y ∈ X

d(x, y) < \frac{1}{2^{h(n)}} implies |f(x) − f(y)| < \frac{1}{2^{n}} .

Within RCA_{0} we define a measure (more accurately, a nonnegative Borel probability measure) on X to be a nonnegative bounded linear functional μ : C(X) → ℝ such that μ(1) = 1. (Here μ(1) denotes μ(f), f ∈ C(X), f(x) = 1 for all x ∈ X.) For example, if X = [0, 1], the unit interval, then there is an obvious measure μ_{L} : C([0, 1]) → ℝ given by μ_{L}(f) = ∫_{0}^{1} f(x) dx, the Riemann integral of f from 0 to 1. We refer to μ_{L} as Lebesgue measure on [0, 1]. There is also the obvious generalization to Lebesgue measure μ_{L} on X = [0, 1]^{n}, the n-cube.

Definition 2.1 (measure of an open set). This definition is made in RCA_{0}. Let X be any compact separable metric space, and let μ be any measure on X. If U is an open set in X, we define

μ(U) = sup { μ(f) | f ∈ C(X) , 0 ≤ f ≤ 1 , f = 0 on X \ U } .

Within RCA_{0} this supremum need not exist as a real number. (Indeed, the existence of μ(U) for all open sets U is equivalent to ACA_{0} over RCA_{0}.) Therefore, when working within RCA_{0}, we interpret assertions about μ(U) in a “virtual” or comparative sense. For example, μ(U) ≤ μ(V) is taken to mean that for all ϵ > 0 and all f ∈ C(X) with 0 ≤ f ≤ 1 and f = 0 on X \ U, there exists g ∈ C(X) with 0 ≤ g ≤ 1 and g = 0 on X \ V such that μ(f) ≤ μ(g) + ϵ. See also [26].

Some basic properties of Lebesgue measure are easily proved in RCA_{0}. For instance, it is straightforward to show that the Lebesgue measure of the union of a finite set of pairwise disjoint open intervals is equal to the sum of the lengths of the intervals.

We define L_{1}(X, μ) to be the completion of C(X) under the L_{1}- norm given by ∥f∥_{1} = μ(|f|). (For the precise definitions, see [5] and [26].) In RCA_{0} we see that L_{1}(X, μ) is a separable Banach space, but to assert within RCA_{0} that points of the Banach space L_{1}(X, μ) represent measurable functions f : X → ℝ is problematic. We shall comment further on this question in section 4 below.

Lemma 2.2. The following is provable in RCA_{0}. If U_{n}, n ∈ ℕ, is a sequence of open sets, then

μ( ⋃_{n=0}^{∞} U_{n}) ≥ lim_{k→∞} μ( ⋃_{n=0}^{k} U_{n}) .

Proof. Trivial.

Lemma 2.3. The following is provable in RCA_{0}. If U_{0}, U_{1}, …, U_{k} is a finite, pairwise disjoint sequence of open sets, then

μ( ⋃_{n=0}^{k} U_{n}) ≥ ∑_{n=0}^{k} μ(U_{n}) .

Proof. Trivial.

An open set is said to be connected if it is not the union of two disjoint nonempty open sets. Let us say that a compact separable metric space X is nice if for all sufficiently small δ > 0 and all x ∈ X, the open ball

B(x, δ) = { y ∈ X | d(x, y) < δ }

is connected. Such a δ is called a modulus of niceness for X.

For example, the unit interval [0, 1] and the n-cube [0, 1]^{n} are nice, but the Cantor space 2^{ℕ} is not nice.

Theorem 2.4 (disjoint countable additivity). The following is provable in RCA_{0}. Assume that X is nice. If U_{n}, n ∈ ℕ, is a pairwise disjoint sequence of open sets in X, then

μ( ⋃_{n=0}^{∞} U_{n}) = ∑_{n=0}^{∞} μ (U_{n}) .

Proof. Put U = ⋃_{n=0}^{∞} U_{n}. Note that U is an open set. By Lemmas 2.2 and 2.3, we have in RCA_{0} that μ(U) ≥ ∑_{n=0}^{∞} μ(U_{n}). It remains to prove in RCA_{0} that μ(U) ≤ ∑_{n=0}^{∞} μ(U_{n}). Let f ∈ C(X) be such that 0 ≤ f ≤ 1 and f = 0 on X \ U. It suffices to prove that μ(f) ≤ ∑_{n=0}^{∞} μ(U_{n}).

Claim 1: There is a sequence of continuous functions f_{n} : X → ℝ, n ∈ ℕ, defined by f_{n}(x) = f(x) for all x ∈ U_{n}, f_{n}(x) = 0 for all x ∈ X \ U_{n}.

To prove this in RCA_{0}, recall from [6] or [20] that a code for a continuous function g from X to Y is a collection G of quadruples (a, r, b, s) with certain properties, the idea being that d(a, x) < r implies d(b, g(x)) ≤ s. Also, a code for an open set U is a collection of pairs (a, r) with certain properties, the idea being that d(a, x) < r implies x ∈ U. In this case we write (a, r) < U to mean that d(a, b)+r < s for some (b, s) belonging to the code of U. Now let F be a code for f : X → ℝ. Define a sequence of codes F_{n}, n ∈ ℕ, by putting (a, r, b, s) into F_{n} if and only if

1. (a, r, b, s) belongs to F and (a, r) < U_{n}, or

2. (a, r, b, s) belongs to F and b − s ≤ 0 ≤ b + s, or

3. b − s ≤ 0 ≤ b + s and (a, r) < U_{m} for some m ≠ n.

It is straightforward to verify that F_{n} is a code for f_{n} as required by claim 1.

Claim 2: The sequence f_{n}, n ∈ ℕ, is a sequence of elements of C(X). To prove this in RCA_{0}, we must show that the sequence of f_{n}’s has

a sequence of moduli of uniform continuity. Let h : ℕ → ℕ be a modulus of uniform continuity for f, and let k be so large that 1/2^{k} is a modulus of niceness for X. We shall show that h′ : ℕ → ℕ defined by h′(m) = max(h(m), k) is a modulus of uniform continuity for all of the f_{n}’s. Let x, y ∈ X and m ∈ ℕ be such that d(x, y) < 1/2^{h′(m)}. To show that |f_{n}(x) − f_{n}(y)| < 1/2^{m}, we consider three cases. Case 1: x, y ∈ U_{n}. In this case we have

|f_{n}(x) − f_{n}(y)| = |f(x) − f(y)| < \frac{1}{2^{m}} .

Case 2: x, y ∈ X \ U_{n}. In this case we have f_{n}(x) = f_{n}(y) = 0 so |f_{n}(x) − f_{n}(x)| = 0. Case 3: x ∈ U_{n}, y ∈ X \ U_{n}. Note that f_{n}(x) = f(x), while f_{n}(y) = 0. Put B = B(x, 1/2^{h′(m)}). Then B is connected and x, y ∈ B. If B ⊆ U, then we would have

B = (B ∩ U_{n}) ∪ (B ∩ (U \ U_{n}))

and this would be a decomposition of B into two disjoint nonempty open sets, a contradiction. Thus B \ U is nonempty. Let z be a point of B \U. Then f(z) = 0 and hence |f_{n}(x)−f_{n}(y)| = |f_{n}(x)| = |f(x)| = |f(x) − f(z)| < 1/2^{m}. This proves claim 2.

Claim 3:

μ(f) = ∑_{n=0}^{∞} μ(f_{n}) . (1)

Note that by definition we already have

f(x) = ∑_{n=0}^{∞} f_{n}(x)

for all x ∈ X. Since μ : C(X) → ℝ is a bounded linear functional,

(1) will follow if we show that the series ∑_{n=0}^{∞} f_{n} converges uniformly to f. If this were not the case, then there would be an ϵ > 0 such that, for infinitely many n, f(x) > ϵ for some x ∈ U_{n}. By uniform continuity of f, let δ > 0 be such that, for all x and y ∈ X, d(x, y) < δ implies |f(x)−f(y)| < ϵ. We may safely assume that δ is a modulus of niceness for X. Now consider n and x such that x ∈ U_{n} and f(x) > ϵ. Clearly f(y) > 0 for all y ∈ B(x, δ); hence B(x, δ) ⊆ U. Since both U_{n} and U \ U_{n} are open, and since B(x, δ) is connected, it follows that B(x, δ) ⊆ U_{n}. Thus, for infinitely many n, we have ∃x B(x, δ) ⊆ U_{n}. On the other hand, by compactness of X, there exists a finite sequence of points x_{1}, …, x_{k} ∈ X such that X = ⋃_{i=1}^{k} B(x_{i}, δ). It follows that for infinitely many n we have x_{i} ∈ U_{n} for some i, 1 ≤ i ≤ k. Since the predicate x_{i} ∈ U_{n} is Σ_{1}^{0}, it follows by Σ_{1}^{0} induction and bounded Σ_{1}^{0} comprehension in RCA_{0} that there exist m, n and i such that m ≠ n and 1 ≤ i ≤ k and x_{i} ∈ U_{m} and x_{i} ∈ U_{n}. This contradicts our assumption that the sets U_{n}, n ∈ ℕ, are pairwise disjoint. Equation (1) and claim 3 are now proved.

From (1) we see that for each ϵ > 0 there exists k such that μ(f)−ϵ ≤ ∑_{n=0}^{k} μ(f_{n}). Thus we have

μ(f) − ϵ ≤ ∑_{n=0}^{k} μ(f_{n}) ≤ ∑_{n=0}^{k} μ(U_{n}) ≤ ∑_{n=0}^{∞} μ(U_{n}) .

Since this holds for all ϵ > 0, it follows that μ(f) ≤ ∑_{n=0}^{∞} μ(U_{n}). Thus μ(U) ≤ ∑_{n=0}^{∞} μ(U_{n}) and the proof of Theorem 2.4 is complete.

Corollary 2.5. The following is provable in RCA_{0}. If (a_{n}, b_{n}), n ∈ ℕ is a sequence of pairwise disjoint open intervals, then

μ_{L}( ⋃_{n=0}^{∞}(a_{n}, b_{n})) = ∑_{n=0}^{∞} |a_{n} − b_{n}| .

Proof. This is a special case of Theorem 2.4.

Remark 2.6. Theorem 2.4 fails if we drop the assumption that X is nice. Indeed, let μ_{C} be the familiar “fair coin” measure on the Cantor space X = 2^{ℕ}, given by μ_{C}({x|x(n) = i}) = 1/2 for all n ∈ ℕ and i ∈ {0, 1}. It can be shown that disjoint finite additivity for μ_{C} is equivalent to WWKL over RCA_{0}. (WWKL is defined and discussed in the next section.) In particular, disjoint finite additivity for μ_{C} is not provable in RCA_{0}.

3. Measure Theory in WWKL_{0}

Yu and Simpson [26] introduced a subsystem of second order arithmetic known as WWKL_{0}, consisting of RCA_{0} plus the following axiom: if T is a subtree of 2^{<ℕ} with no infinite path, then

(2)  lim_{n→∞} \frac{|\{ σ ∈ T | length(σ) = n\}|}{2^{n}} = 0 .

This axiom is known as Weak Weak König’s Lemma (WWKL). It is a weaker axiom than Weak König’s Lemma (WKL), which reads as follows: if T is a subtree of 2^{<ℕ} with no infinite path, then T is finite.

Remark 3.1. Yu and Simpson [26] constructed an ω-model of WWKL_{0} (namely a random real model) which is not an ω-model of WKL_{0}. In addition, Yu and Simpson [26] pointed out that the recursive sets form an ω-model of RCA_{0} which is not an ω-model of WWKL_{0}. Thus WWKL_{0} is properly weaker than WKL_{0} and properly stronger than RCA_{0}. Furthermore, the mathematical content of WKL_{0} and WWKL_{0} is known to be nonconstructive. On the other hand, WKL_{0} and therefore WWKL_{0} are known to be conservative over Primitive Recursive Arithmetic for Π_{2}^{0} sentences. This conservation result for WKL_{0} is due to Friedman [9]; see also Sieg [18]. In this sense, every mathematical theorem provable in WKL_{0} or WWKL_{0} is finitistically reducible in the sense of Hilbert’s Program; see [19, 6, 20].

Remark 3.2. The study of ω-models of WWKL_{0} is closely related to the theory of 1-random sequences, as initiated by Martin-Löf [16] and continued by Kučera [7, 13, 14, 15]. At the time of writing of [26], Yu and Simpson were unaware of this work of Martin-Löf and Kučera.

The purpose of this section and the next is to review and extend the results of [26] and [21] concerning measure theory in WWKL_{0}.

A measure μ : C(X) → ℝ on a compact separable metric space X is said to be countably additive if

μ( ⋃_{n=0}^{∞} U_{n}) = lim_{k→∞} μ( ⋃_{n=0}^{k} U_{n})

for any sequence of open sets U_{n}, n ∈ ℕ, in X. The following theorem is implicit in [26] and [21].

Theorem 3.3. The following assertions are pairwise equivalent over RCA_{0}.

1. WWKL.

2. (countable additivity) For any compact separable metric space X and any measure μ on X, μ is countably additive.

3. For any covering of the closed unit interval [0, 1] by a sequence of open intervals (a_{n}, b_{n}), n ∈ ℕ, we have ∑_{n=0}^{∞} |a_{n} − b_{n}| ≥ 1.

Proof. That WWKL implies statement 2 is proved in Theorem 1 of [26]. The implication 2 → 3 is trivial. It remains to prove that statement 3 implies WWKL.

Reasoning in RCA_{0}, let T be a subtree of 2^{<ℕ} with no infinite path. Put

T̃ = {σ^{⌢}⟨i⟩ | σ ∈ T, σ^{⌢}⟨i⟩ ∉ T, i < 2} .

For σ ∈ 2^{<ℕ} put lh(σ) = length of σ and

a_{σ} = ∑_{n=0}^{lh(σ)−1} \frac{σ(n)}{2^{n+1}} , b_{σ} = a_{σ} + \frac{1}{2^{lh(σ)}} .

Note that |a_{σ} − b_{σ}| = 1/2^{lh(σ)}. Note also that σ, τ ∈ 2^{<ℕ} are incomparable if and only if (a_{σ}, b_{σ}) ∩ (a_{τ}, b_{τ}) = ∅. In particular, the intervals (a_{τ}, b_{τ}), τ ∈ T̃, are pairwise disjoint and cover [0, 1) except for some of the points a_{σ}, σ ∈ 2^{<ℕ}. Fix ϵ > 0 and put c_{σ} = a_{σ} − ϵ/4^{lh(σ)}, d_{σ} = a_{σ} + ϵ/4^{lh(σ)}. Then the open intervals (a_{τ}, b_{τ}), τ ∈ T̃, (c_{σ}, d_{σ}), σ ∈ 2^{<ℕ} and (1 − ϵ, 1 + ϵ) form a covering of [0, 1]. Applying statement 3, we see that the sum of the lengths of these intervals is ≥ 1, i.e.

∑_{τ∈T̃} \frac{1}{2^{lh(τ)}} + 6ϵ ≥ 1 .

Since this holds for all ϵ > 0, we see that

∑_{τ∈T̃} \frac{1}{2^{lh(τ)}} = 1 .

From this, equation (2) follows easily. Thus we have proved that statement 3 implies WWKL. This completes the proof of the theorem.

It is possible to take a somewhat different approach to measure theory in RCA_{0}. Note that the definition of μ(U) that we have given (Definition 2.1) is extensional in RCA_{0}. This means that if U and V contain the same points then μ(U) = μ(V), provably in RCA_{0}. An alternative approach is the intensional one, embodied in Definition 3.4 below.

Recall that an open set U is given in RCA_{0} as a sequence of basic open sets. In the case of the real line, basic open sets are just intervals with rational endpoints.

Definition 3.4 (intensional Lebesgue measure). We make this definition in RCA_{0}. Let U = ⟨(a_{n}, b_{n})⟩_{n∈ℕ} be an open set in the real line. The intensional Lebesgue measure of U is defined by

μ_{I}(U) = lim_{k→∞} μ_{L}( ⋃_{n=0}^{k}(a_{n}, b_{n})) .

Theorem 3.5. It is provable in RCA_{0} that intensional Lebesgue measure μ_{I} is countably additive on open sets. In other words, if U_{n}, n ∈ ℕ, is a sequence of open sets, then

μ_{I}( ⋃_{n=0}^{∞} U_{n}) = lim_{k→∞} μ_{I}( ⋃_{n=0}^{k} U_{n}) .

Proof. This is immediate from the definitions, since ⋃_{n=0}^{∞} U_{n} is defined as the union of the sequences of basic open intervals in U_{n}, n ∈ ℕ.

Returning now to WWKL_{0}, we can prove that intensional Lebesgue measure concides with extensional Lebesgue measure. In fact, we have the following easy result.

Theorem 3.6. The following assertions are pairwise equivalent over RCA_{0}.

1. WWKL.

2. μ_{I}(U) = μ_{L}(U) for all open sets U ⊆ [0, 1].

3. μ_{I} is extensional on open sets. In other words, for all open sets U, V ⊆ [0, 1], if ∀x(x ∈ U ↔ x ∈ V) then μ_{I}(U) = μ_{I}(V).

4. For all open sets U ⊇ [0, 1], we have μ_{I}(U) ≥ 1.

Proof. This is immediate from Theorems 3.3 and 3.5.

4. More Measure Theory in WWKL_{0}

In this section we show that a good theory of measurable functions and measurable sets can be developed within WWKL_{0}.

We first consider pointwise values of measurable functions. Our approach is due to Yu [21, 24].

Let X be a compact separable metric space and let μ : C(X) → ℝ be a positive Borel probability measure on X. Recall that L_{1}(X, μ) is defined within RCA_{0} as the completion of C(X) under the L_{1}-norm. In what sense or to what extent can we prove that a point of the Banach space L_{1}(X, μ) gives rise to a function f : X → ℝ?

In order to answer this question, recall that f ∈ L_{1}(X, μ) is given by a sequence f_{n} ∈ C(X), n ∈ ℕ, which converges to f in the L_{1}-norm; more precisely

∥f_{n} − f_{n+1}∥_{1} ≤ \frac{1}{2^{n}}

for all n ∈ ℕ. We now observe that it is provable in WWKL_{0} that the sequence of continuous functions f_{n}, n ∈ ℕ, converges pointwise almost everywhere. This is established by the following proposition:

Proposition 4.1 (Yu [21]). Provably in WWKL_{0} we have a sequence of closed sets

C_{0}^{f} ⊆ C_{1}^{f} ⊆ ⋯ ⊆ C_{n}^{f} ⊆ …, n ∈ ℕ

such that

μ(X \ C_{n}^{f}) ≤ \frac{1}{2^{n}}

for all n, and

|f_{m}(x) − f_{m′}(x)| ≤ \frac{1}{2^{k}}

for all x ∈ C_{n}^{f} and all m, m′, k such that m, m′ ≥ n + 2k + 2.

Proof. Put

C_{n}^{f} = \{ x | ∀k ∑_{i=n+2k+2}^{∞} |f_{i}(x) − f_{i+1}(x)| ≤ \frac{1}{2^{k}} \} .

Then for x ∈ C_{n}^{f} and m′ ≥ m ≥ n + 2k + 2 we have

|f_{m}(x) − f_{m′}(x)| ≤ ∑_{i=m}^{m′−1} |f_{i}(x) − f_{i+1}(x)|

≤ ∑_{i=n+2k+2}^{∞} |f_{i}(x) − f_{i+1}(x)|

≤ \frac{1}{2^{k}} .

Moreover C_{n}^{f} is a closed set. It remains to show that μ(X \C_{n}^{f}) ≤ 1/2^{n}. To see this, note that C_{n}^{f} = ⋂_{k=0}^{∞} C_{nk}^{f} where

C_{nk}^{f} = \{ x | ∑_{i=n+2k+2}^{∞} |f_{i}(x) − f_{i+1}(x)| ≤ \frac{1}{2^{k}} \} .

We need a lemma:

Lemma 4.2. The following is provable in RCA_{0}. For f ∈ C(X) and ϵ > 0, we have μ({x | f(x) > ϵ}) ≤ ∥f∥_{1}/ϵ.

Proof. Put U = {x | f(x) > ϵ}. Note that U is an open set. If g ∈ C(X), 0 ≤ g ≤ 1, g = 0 on X \ U, then we have ϵg ≤ |f|, hence ϵμ(g) = μ(ϵg) ≤ μ(|f|) = ∥f∥_{1}, hence μ(g) ≤ ∥f∥_{1}/ϵ. Thus μ(U) ≤ ∥f∥_{1}/ϵ and the lemma is proved.

Using this lemma we have

μ(X \ C_{nk}^{f}) = μ (\{x | ∑_{i=n+2k+2}^{∞} |f_{i}(x) − f_{i+1}(x)| > \frac{1}{2^{k}} \})

≤ 2^{k} ∥ ∑_{i=n+2k+2}^{∞} |f_{i} − f_{i+1}|∥_{1}

≤ 2^{k} ∑_{i=n+2k+2}^{∞} ∥f_{i} − f_{i+1}∥_{1}

≤ 2^{k} ∑_{i=n+2k+2}^{∞} \frac{1}{2^{i}}

= \frac{1}{2^{n+k+1}} ,

hence by countable additivity

μ(X \ C_{n}^{f}) ≤ ∑_{k=0}^{∞} μ(X \ C_{nk}^{f})

≤ ∑_{k=0}^{∞} \frac{1}{2^{n+k+1}} = \frac{1}{2^{n}} .

This completes the proof of Proposition 4.1.

Remark 4.3 (Yu [21]). In accordance with Proposition 4.1, for

f = ⟨f_{n}⟩_{n∈ℕ} ∈ L_{1}(X, μ)

and x ∈ ⋃_{n=0}^{∞} C_{n}^{f}, we define f(x) = lim_{n→∞} f_{n}(x). Thus we see that f(x) is defined on an F_{σ} set of measure 1. Moreover, if f = g in L_{1}(X, μ), i.e. if ∥f − g∥_{1} = 0, then f(x) = g(x) for all x in an F_{σ} set of measure 1. These facts are provable in WWKL_{0}.

We now turn to a discussion of measurable sets within WWKL_{0}. We sketch two approaches to this topic. Our first approach is to identify measurable sets with their characteristic functions in L_{1}(X, μ), according to the following definition.

Definition 4.4. This definition is made within WWKL_{0}. We say that f ∈ L_{1}(X, μ) is a measurable characteristic function if there exists a sequence of closed sets

C_{0} ⊆ C_{1} ⊆ ⋯ ⊆ C_{n} ⊆ …, n ∈ ℕ ,

such that μ(X \ C_{n}) ≤ 1/2^{n} for all n, and f(x) ∈ {0, 1} for all x ∈ ⋃_{n=0}^{∞} C_{n}. Here f(x) is as defined in Remark 4.3.

Our second approach is more direct, but in its present form it applies only to certain specific situations. For concreteness we consider only Lebesgue measure μ_{L} on the unit interval [0, 1]. Our discussion can easily be extended to Lebesgue measure on the n-cube [0, 1]^{n}, the “fair coin” measure on the Cantor space 2^{ℕ}, etc.

Definition 4.5. The following definition is made within RCA_{0}. Let S be the Boolean algebra of finite unions of intervals in [0, 1] with rational endpoints. For E_{1}, E_{2} ∈ S we define the distance

d(E_{1}, E_{2}) = μ_{L}((E_{1} \ E_{2}) ∪ (E_{2} \ E_{1})) ,

the Lebesgue measure of the symmetric difference of E_{1} and E_{2}. Thus d is a pseudometric on S, and we define Ŝ to be the compact separable metric space which is the completion of S under d. A point E ∈ Ŝ is called a Lebesgue measurable set in [0, 1].

We shall show that these two approaches to measurable sets (Definitions 4.4 and 4.5) are equivalent in WWKL_{0}.

Begin by defining an isometry χ : S → L_{1}([0, 1], μ_{L}) as follows. For 0 ≤ a < b ≤ 1 define

χ([a, b]) = ⟨f_{n}⟩_{n∈ℕ} ∈ L_{1}([0, 1], μ_{L})

where f_{n}(0) = f_{n}(a) = f_{n}(b) = f_{n}(1) = 0 and

f_{n}(a + \frac{b − a}{2^{n+1}}) = f_{n}(b − \frac{b − a}{2^{n+1}}) = 1

and f_{n} ∈ C([0, 1]) is piecewise linear otherwise. Thus χ([a, b]) is a measurable characteristic function corresponding to the interval [a, b]. For 0 ≤ a_{1} < b_{1} < ⋯ < a_{k} < b_{k} ≤ 1 define

χ([a_{1}, b_{1}] ∪ ⋯ ∪ [a_{k}, b_{k}]) = χ([a_{1}, b_{1}]) + ⋯ + χ([a_{k}, b_{k}]) .

It is straightforward to prove in RCA_{0} that χ extends to an isometry

χ̂ : Ŝ → L_{1}([0, 1], μ_{L}) .

Proposition 4.6. The following is provable in WWKL_{0}. If E ∈ Ŝ is a Lebesgue measurable set, then χ̂(E) is a measurable characteristic function in L_{1}([0, 1], μ_{L}). Conversely, given a measurable characteristic function f ∈ L_{1}([0, 1], μ_{L}), we can find E ∈ Ŝ such that χ̂(E) = f in L_{1}([0, 1], μ_{L}).

Proof. It is straightforward to prove in RCA_{0} that for all E ∈ Ŝ, χ̂(E) is a measurable characteristic function.

For the converse, let f be a measurable characteristic function. By Definition 4.4 we have that f(x) ∈ {0, 1} for all x ∈ ⋃_{n=0}^{∞} C_{n}. By Proposition 4.1 we have |f(x) − f_{3n+3}(x)| < 1/2^{n} for all x ∈ C_{n}^{f}. Put U_{n} = {x | |f_{3n+3}(x) − 1| < 1/2^{n}} and V_{n} = {x | |f_{3n+3}(x)| < 1/2^{n}}. Then for n ≥ 1, U_{n} and V_{n} are disjoint open sets. Moreover C_{n} ∩ C_{n}^{f} ⊆ U_{n} ∪ V_{n}, hence μ_{L}(U_{n} ∪ V_{n}) ≥ 1 − 1/2^{n−1}. By countable additivity (Theorem 3.3) we can effectively find E_{n}, F_{n} ∈ S such that E_{n} ⊆ U_{n} and F_{n} ⊆ V_{n} and μ_{L}(E_{n} ∪ F_{n}) ≥ 1 − 1/2^{n−2}. Put E = ⟨E_{n+5}⟩_{n∈ℕ}. It is straightforward to show that E belongs to Ŝ and that χ̂(E) = f in L_{1}([0, 1], μ_{L}). This completes the proof.

Remark 4.7. We have presented two notions of Lebesgue measurable set and shown that they are equivalent in WWKL_{0}. Our first notion (Definition 4.4) has the advantage of generality in that it applies to any measure on a compact separable metric space. Our second notion (Definition 4.5) is advantageous in other ways, namely it is more straightforward and works well in RCA_{0}. It would be desirable to find a single definition which combines all of these advantages.

5. Vitali’s Theorem

Let S be a collection of sets. A point x is said to be Vitali covered by S if for all ϵ > 0 there exists S ∈ S such that x ∈ S and the diameter of S is less than ϵ. The Vitali Covering Theorem in its simplest form says the following: if I is a sequence of intervals which Vitali covers an interval E in the real line, then I contains a countable, pairwise disjoint set of intervals I_{n}, n ∈ ℕ, such that ⋃_{n=0}^{∞} I_{n} covers E except for a set of Lebesgue measure 0.

The purpose of this section is to show that various forms of the Vitali Covering Theorem are provable in WWKL_{0} and in fact equivalent to WWKL over RCA_{0}.

Throughout this section, we use μ to denote Lebesgue measure.

Lemma 5.1 (Baby Vitali Lemma). The following is provable in RCA_{0}. Let I_{0}, …, I_{n} be a finite sequence of intervals. Then we can find a pairwise disjoint subsequence I_{k_{0}}, …, I_{k_{m}} such that

μ(I_{k_{0}} ∪ ⋯ ∪ I_{k_{m}}) ≥ \frac{1}{3} μ(I_{0} ∪ ⋯ ∪ I_{n}) .

Proof. Put N = {0, …, n}. By bounded Σ_{1}^{0} comprehension in RCA_{0}, the finite sets

{ (i, j) ∈ N^{2} | I_{i} ∩ I_{j} = ∅ }

and

{ (i, j) ∈ N^{2} | μ(I_{i}) ≤ μ(I_{j}) }

exist. Using these finite sets as parameters, we can carry out the following primitive recursion within RCA_{0}. Begin by letting k_{0} ≤ n be such that μ(I_{k_{0}}) is as large as possible. Then let k_{1} be such that I_{k_{1}} ∩ I_{k_{0}} = ∅ and μ(I_{k_{1}}) is as large as possible. At stage j, let k_{j} be such that I_{k_{j}} ∩ I_{k_{0}} = ∅, …, I_{k_{j}} ∩ I_{k_{j−1}} = ∅ and μ(I_{k_{j}}) is as large as possible. The recursion ends with a finite, pairwise disjoint sequence of intervals I_{k_{0}}, …, I_{k_{m}} such that

∀i ≤ n ∃j ≤ m [ I_{i} ∩ I_{k_{j}} ≠ ∅] .

By construction it follows easily that

∀i ≤ n ∃j ≤ m [ I_{i} ∩ I_{k_{j}} ≠ ∅ and μ(I_{i}) ≤ μ(I_{k_{j}}) ] .

For any such i and j, we have I_{i} ⊆ I′_{k_{j}}, where I′_{k_{j}} is an interval with the same midpoint as I_{k_{j}} and 3 times as long. (If I = [a, b], then I′ = [2a − b, 2b − a].) Thus

μ(I_{0} ∪ ⋯ ∪ I_{n}) ≤ μ(I′_{k_{0}} ∪ ⋯ ∪ I′_{k_{m}})
≤ μ(I′_{k_{0}}) + ⋯ + μ(I′_{k_{m}})
= 3 μ(I_{k_{0}}) + ⋯ + 3 μ(I_{k_{m}})
= 3 μ(I_{k_{0}} ∪ ⋯ ∪ I_{k_{m}})

and the lemma is proved.

Lemma 5.2. The following is provable in WWKL_{0}. Let E be an interval, and let I_{n}, n ∈ ℕ, be a sequence of intervals. If E ⊆ ⋃_{n=0}^{∞} I_{n}, then

μ(E) ≤ lim_{k→∞} μ( ⋃_{n=0}^{k} I_{n}) .

Proof. If the intervals I_{n} are open, then the desired conclusion follows immediately from countable additivity (Theorem 3.3). Otherwise, fix ϵ > 0 and let I′_{n} be an open interval with the same midpoint as I_{n} and

μ(I′_{n}) = μ(I_{n}) + \frac{ϵ}{2^{n}} .

Then by countable additivity we have

μ(E) ≤ lim_{k→∞} μ( ⋃_{n=0}^{k} I′_{n}) ≤ lim_{k→∞} μ( ⋃_{n=0}^{k} I_{n}) + 2ϵ .

Since this holds for all ϵ > 0, the desired conclusion follows.

Lemma 5.3 (Vitali theorem for intervals). The following is provable in WWKL_{0}. Let E be an interval, and let I be a sequence of intervals which is a Vitali covering of E. Then I contains a pairwise disjoint sequence of intervals I_{n}, n ∈ ℕ, such that

μ(E \ ⋃_{n=0}^{∞} I_{n}) = 0 .

Proof. We reason in WWKL_{0}. Without loss of generality, let us assume that I consists of closed intervals. Let I^{∗} be the set of finite unions I_{1} ∪ ⋯ ∪ I_{k} where I_{1}, …, I_{k} are pairwise disjoint intervals from I.

We claim: Given A ∈ I^{∗}, if μ(E \ A) > 0 then we can find B ∈ I^{∗} such that A ∩ B = ∅ and

μ(E \ (A ∪ B)) < \frac{3}{4} μ(E \ A) . (3)

To prove the claim, use Lemma 5.2 and the Vitali property to find a finite set of intervals J_{1}, …, J_{l} ∈ I such that J_{1}, …, J_{l} ⊆ E \ A and

μ (E \ (A ∪ J_{1} ∪ ⋯ ∪ J_{l})) < \frac{1}{12} μ(E \ A) .

By the Baby Vitali Lemma 5.1, we can find a pairwise disjoint subset {I_{1}, …, I_{k}} ⊆ {J_{1}, …, J_{l}} such that

μ(I_{1} ∪ ⋯ ∪ I_{k}) ≥ \frac{1}{3} μ(J_{1} ∪ ⋯ ∪ J_{l}) .

We then have

μ(E \ (A ∪ I_{1} ∪ ⋯ ∪ I_{k}))
< \frac{2}{3} μ(J_{1} ∪ ⋯ ∪ J_{l}) + \frac{1}{12} μ(E \ A)
≤ \frac{2}{3} μ(E \ A) + \frac{1}{12} μ(E \ A)
= \frac{3}{4} μ(E \ A)

Thus we may take B = I_{1} ∪ ⋯ ∪ I_{k} and our claim is proved.

Note that the predicates A ∩ B = ∅ and (3) are Σ_{1}^{0}. Thus within RCA_{0} we can apply our claim recursively to choose a pairwise disjoint sequence A_{0} = ∅, A_{1}, A_{2}, … of sets in I^{∗} such that for all n ≥ 1,

μ(E \ (A_{1} ∪ ⋯ ∪ A_{n})) < (\frac{3}{4})^{n} μ(E) .

Then by countable additivity we have

μ(E \ ⋃_{n=1}^{∞} A_{n}) = 0

and the lemma is proved.

Remark 5.4. It is straightforward to generalize the previous lemma to the case of a Vitali covering of the n-cube [0, 1]^{n} by closed balls or n-dimensional cubes. In the case of closed balls, the constant 3 in the Baby Vitali Lemma 5.1 is replaced by 3^{n}.

Theorem 5.5. The Vitali theorem for the interval [0, 1] (as stated in Lemma 5.3) is equivalent to WWKL over RCA_{0}.

Proof. Lemma 5.3 shows that, in RCA_{0}, WWKL implies the Vitali theorem for intervals. It remains to prove within RCA_{0} that the Vitali theorem for [0, 1] implies WWKL. Instead of proving WWKL, we shall prove the equivalent statement 3.3.3. Reasoning in RCA_{0}, suppose that (a_{n}, b_{n}), n ∈ ℕ, is a sequence of open intervals which covers [0, 1]. Let I be the countable set of intervals

(a_{nki}, b_{nki}) = (a_{n} + \frac{i}{k} (b_{n} − a_{n}) , a_{n} + \frac{i + 1}{k}(b_{n} − a_{n}))

where i, k, n ∈ ℕ and 0 ≤ i < k. Then I is a Vitali covering of [0, 1]. By the Vitali theorem for intervals, I contains a sequence of pairwise disjoint intervals I_{m}, m ∈ ℕ, such that

μ( ⋃_{m=0}^{∞} I_{m}) ≥ 1 .

By disjoint countable additivity (Corollary 2.5), we have

∑_{m=0}^{∞} μ(I_{m}) ≥ 1 .

From this it follows easily that ∑_{n=0}^{∞} |a_{n} − b_{n}| ≥ 1. Thus we have 3.3.3 and our theorem is proved.

We now turn to Vitali’s theorem for measurable sets. Recall our discussion of measurable sets in section 4. A sequence of intervals I is said to almost Vitali cover a Lebesgue measurable set E ⊆ [0, 1] if for all ϵ > 0 we have μ_{L} (E \ O_{ϵ}) = 0, where

O_{ϵ} = ⋃ {I | I ∈ I , diam(I) < ϵ} .

Theorem 5.6. The following is provable in WWKL_{0}. Let E ⊆ [0, 1] be a Lebesgue measurable set with μ(E) > 0. Let I be a sequence of intervals which almost Vitali covers E. Then I contains a pairwise disjoint sequence of intervals I_{n}, n ∈ ℕ, such that

μ(E \ ⋃_{n=0}^{∞} I_{n}) = 0 .

Proof. The proof of this theorem is similar to that of Lemma 5.3. The only modification needed is in the proof of the claim. Recall from Definition 4.5 that E = lim_{n→∞} E_{n} where each E_{n} is a finite union of intervals in [0, 1]. Fix m so large that

μ((E \ E_{m}) ∪ (E_{m} \ E)) < \frac{1}{36} μ(E \ A) .

As before, find a finite set of intervals J_{1}, …, J_{l} ∈ I such that

J_{1} ∪ ⋯ ∪ J_{l} ⊆ E_{m} \ A

and

μ (E_{m} \ (A ∪ J_{1} ∪ ⋯ ∪ J_{l})) < \frac{1}{36} μ(E \ A) .

Find {I_{1}, …, I_{k}} ⊆ {J_{1}, …, J_{l}} as before. We then have

μ(E \ (A ∪ I_{1} ∪ ⋯ ∪ I_{k}))
< μ(E_{m} \ (A ∪ I_{1} ∪ ⋯ ∪ I_{k})) + \frac{1}{36} μ(E \ A)
< \frac{2}{3} μ(J_{1} ∪ ⋯ ∪ J_{l}) + \frac{2}{36} μ(E \ A)
≤ \frac{2}{3} μ(E_{m} \ A) + \frac{2}{36} μ(E \ A)
< \frac{2}{3} μ(E \ A) + \frac{3}{36} μ(E \ A)
= \frac{3}{4} μ(E \ A)

Thus we may take B = I_{1} ∪ ⋯ ∪ I_{k} and the claim is proved. The rest of the proof is as for Lemma 5.3.

Remark 5.7. Once again, the previous theorem can be generalized to the case of a Lebesgue measurable set E ⊆ [0, 1]^{n} and a Vitali covering consisting of closed balls or n-dimensional cubes. Such versions of Vitali’s theorem are also provable in WWKL_{0}.

References

1. K. Ambos-Spies, G. H. Müller, and G. E. Sacks (eds.), Recursion Theory Week, Lecture Notes in Mathematics, no. 1432, Springer-Verlag, 1990, IX + 393 pages.

2. Errett Bishop and Douglas Bridges, Constructive Analysis, Grundlehren der mathematischen Wißenschaften, no. 279, Springer-Verlag, 1985, XII + 477 pages.

3. M. Boffa, D. van Dalen, and K. McAloon (eds.), Logic Colloquium ’78, Studies in Logic and the Foundations of Mathematics, North-Holland, 1979, x + 434 pages.

4. Douglas K. Brown, Functional Analysis in Weak Subsystems of Second Order Arithmetic, Ph.D. thesis, The Pennsylvania State University, 1987, vii + 150 pages.

5. Douglas K. Brown and Stephen G. Simpson, Which set existence axioms are needed to prove the separable Hahn-Banach theorem?, Annals of Pure and Applied Logic 31 (1986), 123–144.

6. , The Baire category theorem in weak subsystems of second order arithmetic, Journal of Symbolic Logic 58 (1993), 557–578.

7. O. Demuth and A. Kučera, Remarks on constructive mathematical analysis, [3], 1979, pp. 81–129.

8. H.-D. Ebbinghaus, G.H. Müller, and G.E. Sacks (eds.), Recursion Theory Week, Lecture Notes in Mathematics, no. 1141, Springer-Verlag, 1985, IX + 418 pages.

9. Harvey Friedman, unpublished communication to Leo Harrington, 1977.

10. Harvey Friedman, Stephen G. Simpson, and Rick L. Smith, Countable algebra and set existence axioms, Annals of Pure and Applied Logic 25 (1983), 141–181.

11. , Addendum to “Countable algebra and set existence axioms”, Annals of Pure and Applied Logic 27 (1985), 319–320.

12. A. James Humphreys and Stephen G. Simpson, Separable Banach space theory needs strong set existence axioms, Transactions of the American Mathematical Society 348 (1996), 4231–4255.

13. Antonín Kučera, Measure, Π_{1}^{0} classes and complete extensions of PA, [8], 1985, pp. 245–259.

14. , Randomness and generalizations of fixed point free functions, [1], 1990, pp. 245–254.

15. , On relative randomness, Annals of Pure and Applied Logic 63 (1993), 61–67.

16. Per Martin-Löf, The definition of random sequences, Information and Control 9 (1966), 602–619.

17. W. Sieg (ed.), Logic and Computation, Contemporary Mathematics, American Mathematical Society, 1990, xiv + 297 pages.

18. Wilfried Sieg, Fragments of arithmetic, Annals of Pure and Applied Logic 28 (1985), 33–71.

19. Stephen G. Simpson, Partial realizations of Hilbert’s program, Journal of Symbolic Logic 53 (1988), 349–363.

20. , Subsystems of Second Order Arithmetic, Perspectives in Mathematical Logic, Springer-Verlag, 1998, XIV + 445 pages.

21. Xiaokang Yu, Measure Theory in Weak Subsystems of Second Order Arithmetic, Ph.D. thesis, Pennsylvania State University, 1987, vii + 73 pages.

22. , Radon-Nikodym theorem is equivalent to arithmetical comprehension, [17], 1990, pp. 289–297.

23. , Riesz representation theorem, Borel measures, and subsystems of second order arithmetic, Annals of Pure and Applied Logic 59 (1993), 65–78.

24. , Lebesgue convergence theorems and reverse mathematics, Mathematical Logic Quarterly 40 (1994), 1–13.

25. , A study of singular points and supports of measures in reverse mathematics, Annals of Pure and Applied Logic 79 (1996), 211–219.

26. Xiaokang Yu and Stephen G. Simpson, Measure theory and weak König’s lemma, Archive for Mathematical Logic 30 (1990), 171–180.

E-mail address: dkb5@psu.edu, giusto@dm.unito.it, simpson@math.psu.edu

The Pennsylvania State University