In this section we show that a rather strong set existence axiom,
comprehension, is needed to prove a very elementary (indeed
trivial-sounding) fact of separable Banach space theory. Namely,
is equivalent over
to the following statement (S):
The forward direction is the assertion that (S) is provable in - . This will be obtained as a special case of:
Proof. We reason in -
and each finite set
there is a weak-*-open set
For the reversal, we must show that (S) implies - . The standard method of proving that a mathematical statement implies - is to apply the following lemma [12,23]:
Proof. The assertion that Tn is well-founded is (using the sequence as a parameter). The implication from (1) to (2) is therefore obvious. For the converse, reasoning in , first we show that (2) implies . It is well-known (see ) that is equivalent over to the statement that, for any one-to-one function , the range of f exists. Accordingly, let be one-to-one. By recursive comprehension (using f as a parameter), we define a sequence by if and only if . Note that Tn is well-founded if and only if n is in the range of f. By (2), there is a set Wsuch that if and only if Tn is well-founded, and so if and only if n is in the range of f, i.e., the range of f exists, as desired. This proves .
Now, reasoning in
By the Normal Form Theorem formalized within
we can write
Use recursive comprehension to form a
sequence of trees
In showing that the implication from (S) to - is provable in , we shall want to know that some of our results from Section 3 are provable in . Our version of part of Lemma 3.14 is:
Proof. We reason in . If T* is well-founded then obviously T is well-founded, since . Suppose now that T* is not well-founded. Let f be a path through T*. By recursive comprehension form the tree . Since f is a path through T*, we have that for each n there exists such that , and hence , so Tfis infinite. Thus Tf is a bounded infinite tree. By Bounded König's Lemma, Tf has a path. Here we are using the fact that Bounded König's Lemma is provable in (see  and Lemma IV.1.4 of ). Since , it follows that T has a path. This completes the proof.
Recall that a tree T is said to be smooth if T*=T. The previous lemma implies the following refinement of Lemma 5.2.
Proof. The equivalence of (1) and (2) is Lemma 5.2. Given a sequence of trees , we can use recursive comprehension to form a sequence of smooth trees . By the previous lemma we have in that for all n, Tn is well-founded if and only if Tn* is well-founded. The equivalence of (2) and (3) follows.
Our version of Corollary 3.12 is:
Proof. To simplify notation, let us write , so that . Clearly ZS is a subspace of X*. In order to show that ZS is weak-*-closed, we shall first show that is weak-*-closed.
By arithmetical comprehension, there exists a sequence
where Ms is the least M such that
for all .
as a parameter,
formula asserting for the existence of
We claim that
To see this, let
be given. If
then for some
The claim implies that is weak-*-closed. By Corollary 4.15, it follows in that ZS is weak-*-closed. This completes the proof.
We are now ready to prove our main result:
Proof. The implication from (1) to (2) is just
Lemma 5.1. The implications from (2) to
(3) and (5) to
(6) are straightforward by considering the countable set
It remains to prove in that (7) implies - . First we show in that (7) implies . Toward that end, let be one-to-one; we want to show that the range of f exists. Using f as a parameter, let . By (7), let C be the smallest weak-*-closed subspace of containing Y. Claim: for all , if and only if n is in the range of f. To see this, first suppose n=f(k) for some k. Then for all , and, since weak-* as , we have . Conversely, suppose n is not in the range of f. Then for all , and hence, for all , . Let C' be the set of all such that . Then C' is a weak-*-closed subspace of which contains Y (and hence contains C), but . This proves the claim. Now, ` ' is (as C is a code for a weak-*-closed set), whereas `n is in the range of f' is , so by recursive comprehension, the range of f exists, as desired. Thus (7) implies .
So, reasoning within , assume (7). Instead of proving - directly, we shall prove the equivalent statement given by Lemma 5.4.
be a sequence of smooth trees. By
recursive comprehension, form the set
To prove the claim, let n be such that Tn is well-founded. We shall argue by arithmetical transfinite induction on the well-founded tree Tn that for all . (Note that arithmetical transfinite induction is available in ; see Lemma V.2.1 of .) The base step consists of observing that implies which implies . For the inductive step, let be given such that for all . Clearly converges weak-* to as . Since C is weak-*-closed, it follows that . This gives the inductive step. Thus for all . In particular , i.e., . This proves half of the claim.
For the other half, let n be such that Tn is not well-founded.
We shall show that .
Let f be a path through Tn. By
recursive comprehension form the set
From our assumption (7) we have shown that for all sequences of smooth trees , there exists a set W consisting of all n such that Tn is well-founded. Hence by Lemma 5.4 we see that (7) implies comprehension, i.e., (1). This completes the proof of Theorem 5.6.
Of course, in light of Theorem 3.21, with enough comprehension the equivalences (2) (3) and (4) (5) are trivial; however, we do not know the status of Theorem 3.21 in .
Proof. Let X be a separable Banach space, with a norm closed subspace. In - , since Z is norm closed there is a countable set such that Z is the norm closure of S(see , ). By Theorem 5.6, there is a smallest weak-* closed subspace of X* containing S, which must also be the smallest weak-* closed subspace of X*containing Z. Thus (1) implies (2). The implications (2) (4) and (3) (5) are trivial, and the implications (2) (3) and (4) (5) follow from the norm topology being stronger than the weak topology.
It remains only to prove in
(1). As in the proof
of Theorem 5.6, we first show that (5)
So assume (5) and let
be one-to-one; we want to show in
that the range of fexists. By recursive comprehension (using f as a parameter), define
a tree T by
Conversely, suppose n is not in the range of f; we want to show
It suffices therefore to show that ZS is
weak-* closed, because then
In fact, we'll show that
clearly weak-* closed. Obviously, if z(t)=0 for all ,
follows from the definition of ZS that .
On the other
be given. Since
it follows that
which in turn equals
To prove that (5) implies - , we observe that the subspace in the proof of Theorem 5.6 is weakly closed, so we need only repeat the part of that argument. This completes the proof of Theorem 5.7.