In this section we show that a rather strong set existence axiom,
comprehension, is needed to prove a very elementary (indeed
trivialsounding) 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 
.
For each
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 T_{n} is wellfounded 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 wellknown (see [23]) that is equivalent over to the statement that, for any onetoone function , the range of f exists. Accordingly, let be onetoone. By recursive comprehension (using f as a parameter), we define a sequence by if and only if . Note that T_{n} is wellfounded if and only if n is in the range of f. By (2), there is a set Wsuch that if and only if T_{n} is wellfounded, 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
,
let
be a
formula.
By the Normal Form Theorem formalized within
(see [23]),
we can write
,
where
is
.
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 wellfounded then obviously T is wellfounded, since . Suppose now that T^{*} is not wellfounded. 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 T_{f}is infinite. Thus T_{f} is a bounded infinite tree. By Bounded König's Lemma, T_{f} has a path. Here we are using the fact that Bounded König's Lemma is provable in (see [12] and Lemma IV.1.4 of [23]). 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, T_{n} is wellfounded if and only if T_{n}^{*} is wellfounded. The equivalence of (2) and (3) follows.
Our version of Corollary 3.12 is:
Proof. To simplify notation, let us write , so that . Clearly Z_{S} is a subspace of X^{*}. In order to show that Z_{S} is weak*closed, we shall first show that is weak*closed.
By arithmetical comprehension, there exists a sequence
where M_{s} is the least M such that
for all .
Using
as a parameter,
let
be a
formula asserting for the existence of
and
such that
We claim that
.
To see this, let
be given. If
,
then for some
we have
The claim implies that is weak*closed. By Corollary 4.15, it follows in that Z_{S} 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 onetoone; 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.
Let
be a sequence of smooth trees. By
recursive comprehension, form the set
To prove the claim, let n be such that T_{n} is wellfounded. We shall argue by arithmetical transfinite induction on the wellfounded tree T_{n} that for all . (Note that arithmetical transfinite induction is available in ; see Lemma V.2.1 of [23].) 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 T_{n} is not wellfounded.
We shall show that .
Let f be a path through T_{n}. 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 T_{n} is wellfounded. 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 [4], [7]). 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
that
(5)
(1). As in the proof
of Theorem 5.6, we first show that (5)
implies
.
So assume (5) and let
be onetoone; 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
that
.
Let
.
Then
,
whence
.
It suffices therefore to show that Z_{S} is
weak* closed, because then
,
and
since
.
In fact, we'll show that
,
which is
clearly weak* closed. Obviously, if z(t)=0 for all ,
it
follows from the definition of Z_{S} that .
On the other
hand, suppose
and let
be given. Since
for all
,
it follows that
,
which in turn equals
,
which 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.