Measure Theory in $\mathsf{RCA}_0$

Recall that $\mathsf{RCA}_0$ is the subsystem of second order arithmetic with $\Delta^0_1$ comprehension and $\Sigma^0_1$ induction. The purpose of this section is to show that some measure-theoretic results can be proved in $\mathsf{RCA}_0$.

Within $\mathsf{RCA}_0$, let X be a compact separable metric space. We define $C(X)=\widehat{A}$, the completion of A, where A is the vector space of rational ``polynomials'' over X under the sup-norm, $\Vert f\Vert=\sup_{x\in X}\vert f(x)\vert$. For the precise definitions within $\mathsf{RCA}_0$, see [26] and section III.E of Brown's thesis [4]. The construction of C(X) within $\mathsf{RCA}_0$ is inspired by the constructive Stone-Weierstrass theorem in section 4.5 of Bishop and Bridges [2]. It is provable in $\mathsf{RCA}_0$ that there is a natural one-to-one correspondence between points of C(X) and continuous functions $f:X\to\mathbb{R}$ which are equipped with a modulus of uniform continuity, that is to say, a function $h:\mathbb{N}\to\mathbb{N}$ such that for all $n\in\mathbb{N}$ and x, $y\in X$

$$d(x,y)\,\,<\,\,\frac1{2^{h(n)}} \qquad\mbox{implies} \qquad\vert f(x)-f(y)\vert\,\,<\,\,\frac1{2^n}\,.$$

Within $\mathsf{RCA}_0$ we define a measure (more accurately, a nonnegative Borel probability measure) on X to be a nonnegative bounded linear functional $\mu:C(X)\to\mathbb{R}$ such that $\mu(1)=1$. (Here $\mu(1)$ denotes $\mu(f)$, $f\in C(X)$, f(x)=1 for all $x\in X$.) For example, if X=[0,1], the unit interval, then there is an obvious measure $\mu_L:C([0,1])\to\mathbb{R}$ given by $\mu_L(f)=\int_0^1 f(x)\,dx$, the Riemann integral of f from 0 to 1. We refer to $\mu_L$ as Lebesgue measure on [0,1]. There is also the obvious generalization to Lebesgue measure $\mu_L$ on X=[0,1]ⁿ, the n-cube.

Definition 2.1 (measure of an open set)   This definition is made in $\mathsf{RCA}_0$. Let X be any compact separable metric space, and let $\mu$ be any measure on X. If U is an open set in X, we define

$$\mu(U)\,=\,\sup\,\{\,\mu(f)\,\vert\,f\in C(X)\,,\, 0\le f\le1\,,\, f=0\mbox{ on }X\setminus U\,\}\,.$$

Within $\mathsf{RCA}_0$ this supremum need not exist as a real number. (Indeed, the existence of $\mu(U)$ for all open sets U is equivalent to $\mathsf{ACA}_0$ over $\mathsf{RCA}_0$.) Therefore, when working within $\mathsf{RCA}_0$, we interpret assertions about $\mu(U)$ in a ``virtual'' or comparative sense. For example, $\mu(U)\le\mu(V)$ is taken to mean that for all $\epsilon>0$ and all $f\in C(X)$ with $0\le f\le1$ and f=0 on $X\setminus U$, there exists $g\in C(X)$ with $0\le g\le 1$ and g=0 on $X\setminus V$ such that $\mu(f)\le\mu(g)+\epsilon$. See also [26].

Some basic properties of Lebesgue measure are easily proved in $\mathsf{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,\mu)$ to be the completion of C(X) under the L₁-norm given by $\Vert f\Vert _1=\mu(\vert f\vert)$. (For the precise definitions, see [5] and [26].) In $\mathsf{RCA}_0$ we see that $L_1(X,\mu)$ is a separable Banach space, but to assert within $\mathsf{RCA}_0$that points of the Banach space $L_1(X,\mu)$ represent measurable functions $f:X\to\mathbb{R}$ is problematic. We shall comment further on this question in section 4 below.

Lemma 2.2   The following is provable in $\mathsf{RCA}_0$. If U_n, $n\in\mathbb{N}$, is a sequence of open sets, then

$$\mu\!\left(\,\bigcup_{n=0}^\infty U_n\!\right)\,\,\ge\,\, \lim_{k\to\infty}\,\mu\!\left(\,\bigcup_{n=0}^k U_n\!\right)\,.$$

Proof. Trivial.

Lemma 2.3   The following is provable in $\mathsf{RCA}_0$. If $U_0,U_1,\dots,U_k$ is a finite, pairwise disjoint sequence of open sets, then

$$\mu\!\left(\,\bigcup_{n=0}^k U_n\!\right)\,\,\geq\,\, \sum_{n=0}^k\,\mu\!\left(U_n\!\right)\,.$$

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 $\delta>0$ and all $x\in X$, the open ball

$$B(x,\delta)\,\,=\,\,\{\,y\in X\,\vert\,d(x,y)<\delta\,\}$$

is connected. Such a $\delta$ is called a modulus of niceness for X.

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

Theorem 2.4 (disjoint countable additivity)   The following is provable in $\mathsf{RCA}_0$. Assume that X is nice. If U_n, $n\in\mathbb{N}$, is a pairwise disjoint sequence of open sets in X, then

$$\mu\!\left(\,\bigcup_{n=0}^\infty U_n\!\right)\,\,=\,\, \sum_{n=0}^\infty\,\mu\left(U_n\!\right)\,.$$

Proof. Put $U=\bigcup_{n=0}^\infty U_n$. Note that U is an open set. By Lemmas 2.2 and 2.3, we have in $\mathsf{RCA}_0$ that $\mu(U)\ge\sum_{n=0}^\infty\mu(U_n)$. It remains to prove in $\mathsf{RCA}_0$ that $\mu(U)\le\sum_{n=0}^\infty\mu(U_n)$. Let $f\in C(X)$ be such that $0\le f\le1$ and f=0 on $X\setminus U$. It suffices to prove that $\mu(f)\le\sum_{n=0}^\infty\mu(U_n)$.

Claim 1: There is a sequence of continuous functions $f_n:X\to\mathbb{R}$, $n\in\mathbb{N}$, defined by f_n(x)=f(x) for all $x\in U_n$, f_n(x)=0 for all $x\in X\setminus U_n$.

To prove this in $\mathsf{RCA}_0$, recall from [6] or [19] 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))\leq 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\in 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\to\mathbb{R}$. Define a sequence of codes F_n, $n\in\mathbb{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\le0\le b+s$, or

3.

$b-s\le0\le b+s$ and (a,r)<U_m for some $m\ne 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\in\mathbb{N}$, is a sequence of elements of C(X).

To prove this in $\mathsf{RCA}_0$, we must show that the sequence of f_n's has a sequence of moduli of uniform continuity. Let $h:\mathbb{N}\to\mathbb{N}$ 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':\mathbb{N}\to\mathbb{N}$ defined by $h'(m)=\max(h(m),k)$ is a modulus of uniform continuity for all of the f_n's. Let $x,y\in X$ and $m\in\mathbb{N}$ 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\in U_n$. In this case we have

$$\vert f_n(x)-f_n(y)\vert\,\,=\,\,\vert f(x)-f(y)\vert\,\,<\,\,\frac1{2^m}\,\,.$$

Case 2: $x,y\in X\setminus 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\in U_n$, $y\in X\setminus 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\in B$. If $B\subseteq U$, then we would have

$$B\,\,=\,\, (B\cap U_n)\cup(B\cap(U\setminus U_n))$$

and this would be a decomposition of B into two disjoint nonempty open sets, a contradiction. Thus $B\setminus U$ is nonempty. Let z be a point of $B\setminus 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:

$$\mu(f)\,\,=\,\,\sum_{n=0}^\infty\,\mu(f_n) \,\,.$$ (1)

Note that by definition we already have

$$f(x)\,\,=\,\,\sum_{n=0}^\infty\,f_n(x)$$

for all $x\in X$. Since $\mu:C(X)\to\mathbb{R}$ is a bounded linear functional, (1) will follow if we show that the series $\sum_{n=0}^\infty f_n$ converges uniformly to f. If this were not the case, then there would be an $\epsilon>0$ such that, for infinitely many n, $f(x)>\epsilon$ for some $x\in U_n$. By uniform continuity of f, let $\delta>0$ be such that, for all x and $y\in X$, $d(x,y)<\delta$ implies $\vert f(x)-f(y)\vert<\epsilon$. We may safely assume that $\delta$ is a modulus of niceness for X. Now consider n and x such that $x\in U_n$ and $f(x)>\epsilon$. Clearly f(y)>0 for all $y\in B(x,\delta)$; hence $B(x,\delta)\subseteq U$. Since both U_n and $U\setminus U_n$ are open, and since $B(x,\delta)$ is connected, it follows that $B(x,\delta)\subseteq U_n$. Thus, for infinitely many n, we have $\exists x\,B(x,\delta)\subseteq U_n$. On the other hand, by compactness of X, there exists a finite sequence of points $x_1,\dots,x_k\in X$ such that $X=\bigcup_{i=1}^k B(x_i,\delta)$. It follows that for infinitely many n we have $x_i\in U_n$ for some i, $1\le i\le k$. Since the predicate $x_i\in U_n$ is $\Sigma^0_1$, it follows by $\Sigma^0_1$ induction and bounded $\Sigma^0_1$ comprehension in $\mathsf{RCA}_0$ that there exist m, n and i such that $m\neq n$ and $1\le i\le k$ and $x_i\in U_m$ and $x_i\in U_n$. This contradicts our assumption that the sets U_n, $n\in\mathbb{N}$, are pairwise disjoint. Equation (1) and claim 3 are now proved.

From (1) we see that for each $\epsilon>0$ there exists k such that $\mu(f)-\epsilon\le\sum_{n=0}^k\,\mu(f_n)$. Thus we have

$$\mu(f)-\epsilon \,\,\,\le\,\,\, \sum_{n=0}^k\,\mu(f_n) \,\,\,... ...^k\,\mu(U_n) \,\,\,\le\,\,\, \sum_{n=0}^\infty\,\mu(U_n) \,\,.$$

Since this holds for all $\epsilon>0$, it follows that $\mu(f)\le\sum_{n=0}^\infty\,\mu(U_n)$. Thus $\mu(U)\le\sum_{n=0}^\infty\,\mu(U_n)$ and the proof of Theorem 2.4 is complete.

Corollary 2.5   The following is provable in $\mathsf{RCA}_0$. If (a_n,b_n), $n\in\mathbb{N}$ is a sequence of pairwise disjoint open intervals, then

$$\mu_L\!\left(\,\bigcup_{n=0}^\infty(a_n,b_n)\right) \,\,\,=\,\,\,\sum_{n=0}^\infty\,\vert a_n-b_n\vert\,\,.$$

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 $\mu_C$ be the familiar ``fair coin'' measure on the Cantor space $X=2^\mathbb{N}$, given by $\mu_C(\{x\vert x(n)=i\})=1/2$ for all $n\in\mathbb{N}$ and $i\in\{0,1\}$. It can be shown that disjoint finite additivity for $\mu_C$ is equivalent to WWKL over $\mathsf{RCA}_0$. (WWKL is defined and discussed in the next section.) In particular, disjoint finite additivity for $\mu_C$ is not provable in $\mathsf{RCA}_0$.