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 Z_{2}) we mean the theory consisting of classical
logic plus certain basic arithmetical axioms plus the
induction scheme
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 [22].
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 [23]. In particular, one can prove within (see Chapter IV of [23]) 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 [23].
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:
Note that X^{*} and B_{r}(X^{*}) do not formally exist as sets within . We identify the functionals in B_{r}(X^{*}) in the obvious way with the points of a certain closed set in the compact metric space , where . Thus the compactness of B_{r}(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 [23] and Brown's discussion of the ``Alaoglu ball'' [7]. In particular we have:
Proof. The literature contains two proofs of this result. A direct proof is in [5]. An indirect proof via a version of the Markov-Kakutani fixed point theorem is in [22] and Chapter IV of [23].
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 [7].
For use later in this section, we note that the following separation principle holds in :
Proof. Put
Let Y be the subspace of X generated by x_{0}, i.e., . Define by g(rx_{0})=rp(x_{0}). Then g is a bounded linear functional on Y. Moreover, if then g(rx_{0})=rp(x_{0})=p(rx_{0}), 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+x_{0})=f(y)-f(w)+f(x_{0}) 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 [11]): 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
,
let
be a sequence of points
in X such that
.
By arithmetical comprehension, there
exists a sequence of integers N_{m},
,
such that
for all
and .
Using the sequence
as a parameter, we can define a sequence of closed sets
,
,
by
The proof of the converse will be carried out in
.
Let U be a
bounded-weak-*-open set in X^{*} containing 0. Then
is
a bounded-weak-*-closed set with .
For any countable set
let S^{o} be the polar of S, i.e.,
Let
where A is a countable dense set in X. Put
A_{0}=A and, for each ,
.
Claim:
for any
and any countable set
,
if
then there exists a finite
set
such that
.
If such an F does not exist, then for all finite sets
we would have
,
so by the Heine-Borel covering property of the
compact set
B_{n+1}(X^{*}) it would follow that
Within
,
we can apply the claim above repeatedly starting with
to obtain a sequence of finite sets
,
,
such that
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-x_{0}^{*} is also bounded-weak-*-closed and convex, and . Thus is a closed subset of B_{n}(X^{*}) for each . Since B_{n}(X^{*}) is compact, in there exists a countable dense subset for each n (see Theorem 3.2 in [4]). We want to find a weak-*-open set N containing 0 in X^{*} which is disjoint from C-x_{0}^{*}, as this will show that x_{0}^{*}+N is disjoint from C. Let U be a bounded-weak-*-open set containing 0 which is disjoint from C-x_{0}^{*}. 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 T_{n}|B_{m}(X^{*})=T_{m}. Thus we can define a function by T(x^{*})=T_{m}(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 c_{0}, 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 D_{m} is dense in B_{m}(X^{*}) and f and T_{m} are continuous. So let ; then N is weak-*-open, contains 0, and is disjoint from C-x_{0}^{*}. 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.