The language of second order arithmetic consists of number variables
m, n, ..., set variables X, Y, ..., primitives +,
0, 1, =, ,
and logical operations including number
quantifiers and set quantifiers. By second order arithmetic
(sometimes called Z2) we mean the theory consisting of classical
logic plus certain basic arithmetical axioms plus the
Two of the most important subsystems of second order arithmetic are and - . A formula of the language of second order arithmetic is said to be arithmetical if it contains no set quantifiers. The axioms of consist of the basic arithmetical axioms, the restricted induction axiom, and arithmetical comprehension, i.e., the comprehension scheme for formulas which are arithmetical. A formula is one of the form where is arithmetical. The axioms of - consist of the axioms of plus comprehension. Obviously - is much stronger than . Three other very important subsystems of second order arithmetic are and , both of which are weaker than , and , which is intermediate between and - . For background material on subsystems of second order arithmetic, we refer the reader to [12,5,6,23].
The purpose of this section is to show how some fundamental results concerning separable Banach spaces and the weak-* topology can be developed formally within and weaker systems. In particular, we show that a version of the Krein-Smulian theorem is provable in . Our approach for the development of separable Banach space theory within subsystems of second order arithmetic follows that of Brown and Simpson [5,7,4,6,23]; see also the paper of Shioji and Tanaka .
Building on the definitions above within , one can define corresponding notions of continuous function from one complete separable metric space into another, etc. On this basis, one can prove within or or many fundamental results about the topology of complete separable metric spaces. For details, see . In particular, one can prove within (see Chapter IV of ) the Heine-Borel covering lemma (``if Cis compact then any covering of C by a sequence of open sets has a finite subcovering''), using the following notion of compactness:
In the same setting, there is a useful version of the Tychonoff product theorem, and one can prove within the compactness of the product space , where is any sequence of closed bounded intervals. For details, see Chapter IV of .
We now turn to our development of separable Banach space theory within and .
It can be proved in [5,7,23] that bounded linear operators are identifiable with continuous linear mappings from X into Y. Also within one can prove a useful version of the Banach-Steinhaus theorem:
Proof. See [7,6,23].
Note that X* and Br(X*) do not formally exist as sets within . We identify the functionals in Br(X*) in the obvious way with the points of a certain closed set in the compact metric space , where . Thus the compactness of Br(X*) is provable in . This version of the Banach-Alaoglu theorem turns out to be very useful for the development of separable Banach space theory within . See [5,22] and Chapter IV of  and Brown's discussion of the ``Alaoglu ball'' . In particular we have:
Proof. The literature contains two proofs of this result. A direct proof is in . An indirect proof via a version of the Markov-Kakutani fixed point theorem is in  and Chapter IV of .
Proof. Either of the cited proofs of Theorem 4.8 can be straightforwardly adapted to prove this more general result. See also Theorem 4.2 of .
For use later in this section, we note that the following separation principle holds in :
Let Y be the subspace of X generated by x0, i.e., . Define by g(rx0)=rp(x0). Then g is a bounded linear functional on Y. Moreover, if then g(rx0)=rp(x0)=p(rx0), and if r<0 then , so on Y. Thus, by our extended Hahn-Banach theorem 4.9 in , we can extend g to a bounded linear functional such that on X.
Let be given, and suppose y is such that . Then , whence by definition of p. But f(y-w+x0)=f(y)-f(w)+f(x0) and , so . Replacing f by , we see that and for all x in the convex hull of Z. This completes the proof.
We conjecture that this separation principle is actually provable in and not only in .
We now begin our treatment of the weak-* topology within . We start by introducing an version of the bounded-weak-*topology:
The next lemma formalizes within a well-known fact (see Lemma V.5.4 in ): there is a bounded-weak-*neighborhood basis of 0 in X* consisting of the polars of sequences converging to 0 in X.
Proof. Reasoning in
be a sequence of points
in X such that
By arithmetical comprehension, there
exists a sequence of integers Nm,
Using the sequence
as a parameter, we can define a sequence of closed sets
The proof of the converse will be carried out in
Let U be a
bounded-weak-*-open set in X* containing 0. Then
a bounded-weak-*-closed set with .
For any countable set
let So be the polar of S, i.e.,
where A is a countable dense set in X. Put
A0=A and, for each ,
and any countable set
then there exists a finite
If such an F does not exist, then for all finite sets
we would have
so by the Heine-Borel covering property of the
Bn+1(X*) it would follow that
we can apply the claim above repeatedly starting with
to obtain a sequence of finite sets
Letting be an enumeration without repetition of , it is clear that in X and that . This completes the proof.
We now introduce our version of the weak-* topology.
According to the previous definition, we have trivially in that any weak-*-closed set is bounded-weak-*-closed. In we have following version of the Krein-Smulian theorem:
Proof. Let be given. Then C-x0* is also bounded-weak-*-closed and convex, and . Thus is a closed subset of Bn(X*) for each . Since Bn(X*) is compact, in there exists a countable dense subset for each n (see Theorem 3.2 in ). We want to find a weak-*-open set N containing 0 in X* which is disjoint from C-x0*, as this will show that x0*+N is disjoint from C. Let U be a bounded-weak-*-open set containing 0 which is disjoint from C-x0*. By Lemma 4.12, there is a sequence such that and .
Now, for each , define a function by . These form a sequence of compatible functions, i.e., if m<n then Tn|Bm(X*)=Tm. Thus we can define a function by T(x*)=Tm(x*) where . Notice that T is linear, and implies for all . Let D be an enumeration of the dense sets , and let E=T(D)(which exists by arithmetical comprehension); then E is a countable subset of c0, and for all x in the convex hull of E. By Lemma 4.10 there exists such that for all x in the convex hull of E. Write .
Let ; note that is weak-*-open and contains 0. Also, if then for some m. Thus since Dm is dense in Bm(X*) and f and Tm are continuous. So let ; then N is weak-*-open, contains 0, and is disjoint from C-x0*. This completes the proof.
Specializing to subspaces of X* (see also Corollary 2.8 above), we obtain:
Proof. This follows easily from the previous theorem. See also the proof of Corollary 2.8.