next up previous
Next: More Measure Theory in Up: Vitali's Theorem and WWKL Previous: Measure Theory in

   
Measure Theory in $\mathsf{WWKL}_0$

Yu and Simpson [26] introduced a subsystem of second order arithmetic known as $\mathsf{WWKL}_0$, consisting of $\mathsf{RCA}_0$ plus the following axiom: if T is a subtree of $2^{<\mathbb{N} }$ with no infinite path, then

 \begin{displaymath}
\lim_{n\to\infty}\frac{\vert\{\,\sigma\in
T\,\vert\,\,\mbox{length}(\sigma)=n\}\vert}{2^n} \,\,=\,\, 0\,.
\end{displaymath} (2)

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^{<\mathbb{N} }$ with no infinite path, then T is finite.

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

Remark 3.2   The study of $\omega$-models of $\mathsf{WWKL}_0$ is closely related to the theory of 1-random sequences, as initiated by Martin-Löf [16] and continued by Kucera [7,13,14,15]. At the time of writing of [26], Yu and Simpson were unaware of this work of Martin-Löf and Kucera.

The purpose of this section and the next is to review and extend the results of [26] and [21] concerning measure theory in $\mathsf{WWKL}_0$.

A measure $\mu:C(X)\to\mathbb{R} $ on a compact separable metric space X is said to be countably additive if

\begin{displaymath}\mu\!\left(\,\bigcup_{n=0}^\infty
U_n\!\right)\,\,\,=\,\,\,\lim_{k\to\infty}\,\mu\!\left(\,\bigcup_{n=0}^k
U_n\!\right) \end{displaymath}

for any sequence of open sets Un, $n\in\mathbb{N} $, in X. The following theorem is implicit in [26] and [21].

Theorem 3.3   The following assertions are pairwise equivalent over $\mathsf{RCA}_0$.
1.
WWKL.
2.
(countable additivity) For any compact separable metric space X and any measure $\mu$ on X, $\mu$ is countably additive.  
3.
For any covering of the closed unit interval [0,1] by a sequence of open intervals (an,bn), $n\in\mathbb{N} $, we have $\sum_{n=0}^\infty\vert a_n-b_n\vert\ge1$.  

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

Reasoning in $\mathsf{RCA}_0$, let T be a subtree of $2^{<\mathbb{N} }$ with no infinite path. Put

\begin{displaymath}\widetilde{T} \,\,=\,\,
\{\sigma^{\smallfrown}\!\left\langle...
...smallfrown}\!\left\langle i\right\rangle\notin T,\, i<2\}\,\,. \end{displaymath}

For $\sigma\in2^{<\mathbb{N} }$ put $\mbox{lh}(\sigma)=$ length of $\sigma$ and

\begin{displaymath}a_\sigma \,\,=\,\,
\sum_{n=0}^{\mbox{lh}(\sigma)-1}\frac{\si...
...
b_\sigma\,\,=\,\,a_\sigma+\frac1{2^{\mbox{lh}(\sigma)}}\,\,. \end{displaymath}

Note that $\vert a_\sigma-b_\sigma\vert=1/2^{\mbox{lh}(\sigma)}$. Note also that $\sigma,\tau\in 2^{<\mathbb{N} }$ are incomparable if and only if $(a_\sigma,b_\sigma)\cap(a_\tau,b_\tau)=\emptyset$. In particular, the intervals $(a_\tau,b_\tau)$, $\tau\in\widetilde{T}$, are pairwise disjoint and cover [0,1) except for some of the points $a_\sigma$, $\sigma\in2^{<\mathbb{N} }$. Fix $\epsilon>0$ and put $c_\sigma=a_\sigma -\epsilon/4^{\mbox{lh}(\sigma)}$, $d_\sigma=
a_\sigma +\epsilon/4^{\mbox{lh}(\sigma)}$. Then the open intervals $(a_\tau,b_\tau)$, $\tau\in\widetilde{T}$, $(c_\sigma,d_\sigma)$, $\sigma\in2^{<\mathbb{N} }$ and $(1-\epsilon,1+\epsilon)$ form a covering of [0,1]. Applying statement 3, we see that the sum of the lengths of these intervals is $\geq1$, i.e.

\begin{displaymath}\sum_{\tau\in\widetilde{T}}\,\,\frac1{2^{\mbox{lh}(\tau)}}\,+\,6\epsilon
\,\,\geq\,\, 1 \,\,.\end{displaymath}

Since this holds for all $\epsilon>0$, we see that

\begin{displaymath}\sum_{\tau\in\widetilde{T}}\,\,\frac1{2^{\mbox{lh}(\tau)}}
\,\,=\,\, 1 \,\,.\end{displaymath}

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 $\mathsf{RCA}_0$. Note that the definition of $\mu(U)$ that we have given (Definition 2.1) is extensional in $\mathsf{RCA}_0$. This means that if U and V contain the same points then $\mu(U)=\mu(V)$, provably in $\mathsf{RCA}_0$. An alternative approach is the intensional one, embodied in Definition 3.4 below.

Recall that an open set U is given in $\mathsf{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 $\mathsf{RCA}_0$. Let $U=\left\langle(a_n,b_n)\right\rangle_{n\in\mathbb{N} }$ be an open set in the real line. The intensional Lebesgue measure of U is defined by

\begin{displaymath}\mu_I(U) \,\,=\,\, \lim_{k\to\infty}\,
\mu_L\!\left(\,\bigcup_{n=0}^k(a_n,b_n)\right) \,\,. \end{displaymath}

Theorem 3.5   It is provable in $\mathsf{RCA}_0$ that intensional Lebesgue measure $\mu_I$ is countably additive on open sets. In other words, if Un, $n\in\mathbb{N} $, is a sequence of open sets, then

\begin{displaymath}\mu_I\!\left(\,\bigcup_{n=0}^\infty U_n\!\right) \,\,=\,\,
\...
...{k\to\infty}\mu_I\!\left(\,\bigcup_{n=0}^k U_n\!\right) \,\,.
\end{displaymath}

Proof. This is immediate from the definitions, since $\bigcup_{n=0}^\infty
U_n$ is defined as the union of the sequences of basic open intervals in Un, $n\in\mathbb{N} $.

Returning now to $\mathsf{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 $\mathsf{RCA}_0$.
1.
WWKL.
2.
$\mu_I(U)=\mu_L(U)$ for all open sets $U\subseteq[0,1]$.
3.
$\mu_I$ is extensional on open sets. In other words, for all open sets $U,V\subseteq[0,1]$, if $\,\forall x(x\in
U\leftrightarrow x\in V)$ then $\mu_I(U)=\mu_I(V)$.
4.
For all open sets $U\supseteq[0,1]$, we have $\mu_I(U)\geq1$.

Proof. This is immediate from Theorems 3.3 and 3.5.


next up previous
Next: More Measure Theory in Up: Vitali's Theorem and WWKL Previous: Measure Theory in
Stephen G Simpson
1998-10-25