Next: More Measure Theory in
Up: Vitali's Theorem and WWKL
Previous: Measure Theory in
Measure Theory in
Yu and Simpson [26] introduced a subsystem of second
order arithmetic known as
,
consisting of
plus the
following axiom: if T is a subtree of
with no
infinite path, then
 |
(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
with no infinite path, then
T is finite.
Remark 3.1
Yu and Simpson [
26] constructed an

-model of

(namely a random real model) which is not an

-model
of

.
In addition, Yu and Simpson [
26] pointed
out that the recursive sets form an

-model of

which
is not an

-model of

.
Thus

is properly
weaker than

and properly stronger than

.
Furthermore, the mathematical content of

and

is
known to be nonconstructive. On the other hand,

and
therefore

are known to be conservative over Primitive
Recursive Arithmetic for

sentences. This conservation
result for

is due to Friedman [
9]; see also Sieg
[
18]. In this sense, every mathematical theorem provable in

or

is finitistically reducible in the sense of
Hilbert's Program; see [
20,
6,
19].
Remark 3.2
The study of

-models of

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
.
A measure
on a compact separable metric space X is
said to be countably additive if
for any sequence of open sets Un,
,
in
X. The following theorem is implicit in [26] and
[21].
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
,
let T be a subtree of
with no
infinite path. Put
For
put
length of
and
Note
that
.
Note also that
are incomparable if and only if
.
In particular,
the intervals
,
,
are
pairwise disjoint and cover [0,1) except for some of the points
,
.
Fix
and put
,
.
Then the open intervals
,
,
,
and
form a covering of
[0,1]. Applying statement 3, we see that the sum of
the lengths of these intervals is
,
i.e.
Since this holds for all
,
we see
that
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
.
Note that the definition of
that we have given
(Definition 2.1) is extensional in
.
This
means that if U and V contain the same points then
,
provably in
.
An alternative approach is the
intensional one, embodied in Definition 3.4 below.
Recall that an open set U is given in
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

.
Let

be an open set in the real line. The
intensional Lebesgue measure of
U is defined by
Theorem 3.5
It is provable in

that intensional Lebesgue measure

is countably additive on open sets. In other words, if
Un,

,
is a sequence of open sets, then
Proof. This is immediate from the definitions, since
is defined as the union of the sequences of basic open
intervals in Un,
.
Returning now to
,
we can prove that intensional Lebesgue
measure concides with extensional Lebesgue measure. In fact, we have
the following easy result.
Proof. This is immediate from Theorems 3.3 and 3.5.
Next: More Measure Theory in
Up: Vitali's Theorem and WWKL
Previous: Measure Theory in
Stephen G Simpson
1998-10-25