The weak-* topology in subsystems of Z₂

The language of second order arithmetic consists of number variables m, n, ..., set variables X, Y, ..., primitives +, $\cdot$, 0, 1, =, $\in$, and logical operations including number quantifiers and set quantifiers. By second order arithmetic (sometimes called Z₂) we mean the theory consisting of classical logic plus certain basic arithmetical axioms plus the induction scheme

$$(\varphi(0)\wedge\forall n(\varphi(n)\rightarrow\varphi(n+1)))\rightarrow\forall n\varphi(n)$$

plus the comprehension scheme

$$\exists W\, \forall n\,(n\in W\leftrightarrow\varphi(n))$$

where $\varphi(n)$ is an arbitrary formula of the language of second order arithmetic. In the comprehension scheme it is assumed that the set variable W does not occur freely in $\varphi(n)$. All of the subsystems of second order arithmetic that we shall consider employ classical logic and include the basic arithmetical axioms and the restricted induction axiom

$$(0\in W\wedge\forall n\,(n\in W\rightarrow n+1\in W))\rightarrow\forall n\,(n\in W)\,.$$

Two of the most important subsystems of second order arithmetic are $\mathsf{ACA}_0$ and $\Pi^1_1$- $\mathsf{CA}_0$. A formula of the language of second order arithmetic is said to be arithmetical if it contains no set quantifiers. The axioms of $\mathsf{ACA}_0$ consist of the basic arithmetical axioms, the restricted induction axiom, and arithmetical comprehension, i.e., the comprehension scheme for formulas $\varphi(n)$ which are arithmetical. A $\Pi^1_1$ formula is one of the form $\forall W\,\theta$ where $\theta$ is arithmetical. The axioms of $\Pi^1_1$- $\mathsf{CA}_0$ consist of the axioms of $\mathsf{ACA}_0$ plus $\Pi^1_1$ comprehension. Obviously $\Pi^1_1$- $\mathsf{CA}_0$ is much stronger than $\mathsf{ACA}_0$. Three other very important subsystems of second order arithmetic are $\mathsf{RCA}_0$ and $\mathsf{WKL}_0$, both of which are weaker than $\mathsf{ACA}_0$, and $\mathsf{ATR}_0$, which is intermediate between $\mathsf{ACA}_0$ and $\Pi^1_1$- $\mathsf{CA}_0$. 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 $\mathsf{ACA}_0$ and weaker systems. In particular, we show that a version of the Krein-Smulian theorem is provable in $\mathsf{ACA}_0$. 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].

Definition 4.1 (tex2html_wrap_inline$RCA_0$)   A (code for a) complete separable metric space $\widehat A$ is defined to be a set $A\subseteq{\mathbb{N} }$ together with a function $d:A\times A\to{\mathbb{R} }$ such that, for all $a,b,c\in A$,

1.

d(a,a)=0,

2.

d(a,b)=d(b,a), and

3.

$d(a,c)\le d(a,b)+d(b,c)$.

A (code for a) point of $\widehat A$ is defined to be a sequence $\langle{}a_n\mid n\in{\mathbb{N} }\rangle{}$ of elements of A such that $\forall m\,\forall n\,(m<n\longrightarrow d(a_m,a_n)\le1/{2^m})$. Although $\widehat A$ does not formally exist as a set within $\mathsf{RCA}_0$, we use notations such as $x\in{\widehat A}$ to mean that x is a point of $\widehat A$, etc. We then straightforwardly extend our definitions of = and d to  $\widehat A$ in such a way that $\langle{}\widehat A,d\rangle{}$ is a complete metric space, with A dense in  $\widehat A$.

Definition 4.2 (tex2html_wrap_inline$RCA_0$)   Let $\widehat A$ be a complete separable metric space as defined above. A (code for an) open set in $\widehat A$ is defined to be a sequence of ordered pairs $U=\langle{}(a_i,q_i)\mid i\in{\mathbb{N} }\rangle{}$, $a_i\in A$, $q_i\in{\mathbb{Q} }$. We write $x\in U$ to mean that $x\in{\widehat A}$ and d(x,a_i)<q_ifor some $i\in{\mathbb{N} }$. A closed set in $\widehat A$ is defined to be the complement of an open set.  

Building on the definitions above within $\mathsf{RCA}_0$, one can define corresponding notions of continuous function from one complete separable metric space into another, etc. On this basis, one can prove within $\mathsf{ACA}_0$ or $\mathsf{WKL}_0$ or $\mathsf{RCA}_0$ many fundamental results about the topology of complete separable metric spaces. For details, see [23]. In particular, one can prove within $\mathsf{WKL}_0$ (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 $\mathsf{RCA}_0$ notion of compactness:

Definition 4.3 (tex2html_wrap_inline$RCA_0$)   Let C be a closed set in a complete separable metric space $\widehat A$. We say that C is compact if there exists a countable sequence of finite sequences of points $\langle{}\langle{} x_{ni}\mid i\le k_n\rangle{}\mid n\in{\mathbb{N} }\rangle{}$ in $\widehat A$ such that for all $x\in C$ and all $n\in{\mathbb{N} }$ there exists $i\le k_n$ such that d(x,x_ni)<1/2ⁿ.

In the same setting, there is a useful version of the Tychonoff product theorem, and one can prove within $\mathsf{RCA}_0$ the compactness of the product space $\prod_{n\in{\mathbb{N} }}[a_n,b_n]$, where $\langle{}[a_n,b_n]\mid n\in{\mathbb{N} }\rangle{}$ 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 $\mathsf{RCA}_0$ and $\mathsf{ACA}_0$.

Definition 4.4 (tex2html_wrap_inline$RCA_0$)   A (code for a) separable Banach space consists of a countable set $A\subseteq{\mathbb{N} }$ together with operations $+:A\times A\to A$, $-:A\times A\to A$, and $\cdot:{\mathbb{Q} }\times A\to A$ and a distinguished element $0\in A$ such that $\langle{}A,+,-,\cdot,0\rangle{}$forms a countable vector space over the rational field ${\mathbb{Q} }$, together with a function $\Vert\,\Vert:A\to{\mathbb{R} }$ satisfying

1.

$\Vert qa\Vert=\vert q\vert\Vert a\Vert$ for all $a\in A$ and $q\in{\mathbb{Q} }$, and

2.

$\Vert a+b\Vert\le\Vert a\Vert+\Vert b\Vert$ for all $a,b\in A$.

In other words, a code for a separable Banach space $\widehat A$ is a countable pseudo-normed vector space A over ${\mathbb{Q} }$. Note that $\widehat A$ is a complete separable metric space under $d(a,b)=\Vert a-b\Vert$. Thus a point of the separable Banach space $\widehat A$ is by definition a sequence $\langle{}a_n\mid n\in{\mathbb{N} }\rangle{}$ such that $\forall m\,\forall n\,(m<n\longrightarrow\Vert a_m-a_n\Vert<1/{2^m})$.

Definition 4.5 (tex2html_wrap_inline$RCA_0$)   Let $X={\widehat A}$ and $Y={\widehat B}$ be separable Banach spaces. A (code for a) bounded linear operator $F:X\to Y$ is a linear mapping $F:A\to{\widehat B}$ such that, for some $0\le r<\infty$, $\Vert F\Vert\le r$, i.e., $\Vert F(a)\Vert\le r\Vert a\Vert$ for all $a\in A$. If $x=\langle{}a_n\mid n\in{\mathbb{N} }\rangle{}$ is a point of $X={\widehat A}$, we write $F(x)=\lim_nF(a_n)$.

It can be proved in $\mathsf{RCA}_0$ [5,7,23] that bounded linear operators $F:X\to Y$ are identifiable with continuous linear mappings from X into Y. Also within $\mathsf{RCA}_0$ one can prove a useful version of the Banach-Steinhaus theorem:

Theorem 4.6   The following is provable in $\mathsf{RCA}_0$. Given separable Banach spaces Xand Y and a sequence of bounded linear operators $F_n:X\to Y$, $n\in{\mathbb{N} }$, if $\{\Vert F_n(x)\Vert\mid n\in{\mathbb{N} }\}$ is bounded for all $x\in X$, then there exists $r<\infty$ such that $\Vert F_n\Vert\le r$ for all $n\in{\mathbb{N} }$.  

Proof. See [7,6,23].

Definition 4.7 (tex2html_wrap_inline$RCA_0$)   Let X be a separable Banach space. A bounded linear functional on X is a bounded linear operator $f:X\to{\mathbb{R} }$. We write $f\in X^*$ to mean that f is a bounded linear functional on X. For $0\le r<\infty$, we write $f\in B_r(X^*)$ to mean that $f\in X^*$ and $\Vert f\Vert\le r$.

Note that X^* and B_r(X^*) do not formally exist as sets within $\mathsf{RCA}_0$. 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 $\prod_{a\in A}[-r\Vert a\Vert,r\Vert a\Vert]$, where $X={\widehat A}$. Thus the compactness of B_r(X^*) is provable in $\mathsf{RCA}_0$. This version of the Banach-Alaoglu theorem turns out to be very useful for the development of separable Banach space theory within $\mathsf{WKL}_0$. See [5,22] and Chapter IV of [23] and Brown's discussion of the ``Alaoglu ball'' [7]. In particular we have:

Theorem 4.8   The following version of the Hahn-Banach theorem is provable in $\mathsf{WKL}_0$. Let X be a separable Banach space and let Y be a subspace of X. If $g:Y\to{\mathbb{R} }$ is a bounded linear functional with $\Vert g\Vert\le r$, then there exists a bounded linear functional $f:X\to{\mathbb{R} }$ such that $\Vert f\Vert\le r$ and f extends g, i.e., f(x)=g(x) for all $x\in Y$.  

Proof. The literature contains two proofs of this result. A direct proof is in [5]. An indirect proof via a $\mathsf{WKL}_0$ version of the Markov-Kakutani fixed point theorem is in [22] and Chapter IV of [23].

Theorem 4.9   The following extension of the Hahn-Banach Theorem is provable in $\mathsf{WKL}_0$. Let X be a separable Banach space. Let $p:X\to{\mathbb{R} }$ be a continuous function such that p(rx)=rp(x) and $p(x+y)\le p(x)+p(y)$for all $r\ge0$ and $x,y\in X$. Let Y be a subspace of X and let $g:Y\to{\mathbb{R} }$ be a bounded linear functional such that $g(x)\le p(x)$ for all $x\in Y$. Then there exists a bounded linear functional $f:X\to{\mathbb{R} }$ such that f extends g and $f(x)\le p(x)$ for all $x\in X$.  

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 $\mathsf{ACA}_0$:

Lemma 4.10   The following is provable in $\mathsf{ACA}_0$. Let X be a separable Banach space. Let Z be a countable set in X such that $\vert\vert x\vert\vert\ge1$ for all x in the convex hull of Z. Then there exists $f\in B_1(X^*)$such that $f(x)\ge1$ for all x in the convex hull of Z.  

Proof. Put

$$W=\Biggl\{\sum_{i<n}q_iz_i\Bigm\vert n\in{\mathbb{N} }\,,\;q_... ...athbb{Q} }\cap[0,1]\,,\;\sum_{i<n}q_i=1\,,\;z_i\in Z\Biggr\}\,.$$

Note that $\Vert w\Vert\ge1$ for all $w\in W$. Fix $x_0\in W$. By arithmetical comprehension, there is a continuous function $p:X\to{\mathbb{R} }$defined by

$$p(x)=\inf\{c\in{\mathbb{Q} }\mid c>0\wedge\exists w\in W\,(\Vert(x/c)+w-x_0\Vert\le1)\}\,.$$

Then p satisfies the following:

1.

$p(x_0)\ge1$.

2.

$0\le p(x)\le\Vert x\Vert$ for all $x\in X$.

3.

p(rx)=rp(x) for all $r\ge0$ and $x\in X$.

4.

$p(x+y)\le p(x)+p(y)$ for all $x,y\in X$.

Some remarks: if property 1 failed, then there would be $w\in W$ and a rational c<1 such that $\Vert(x_0/c)+w-x_0\Vert\le1$, whence $\Vert(1-c)x_0+cw\Vert\le c<1$, contrary to (1-c)x₀+cw being in W. Properties 2 and 3 are easily verified. As for property 4, given c>p(x)+p(y), write c=a+b where a>p(x) and b>p(y). Then there exist w₁ and w₂ in W such that $\Vert(x/a)+w_1-x_0\Vert\le1$ and $\Vert(y/b)+w_2-x_0\Vert\le1$. Then

$$\frac{x+y}{a+b}+\frac{a}{a+b}w_1+\frac{b}{a+b}w_2-x_0 =\left(... ...a}+w_1-x_0)+ \left(\frac{b}{a+b}\right)(\frac{y}{b}+w_2-x_0)\,,$$

so

$$\left\Vert\frac{x+y}{a+b}+\frac{a}{a+b}w_1+\frac{b}{a+b}w_2-x_0\right\Vert \le \frac{a}{a+b}+\frac{b}{a+b}=1$$

whence $p(x+y)\le a+b=c$.

Let Y be the subspace of X generated by x₀, i.e., $Y={\mathbb{R} }x_0$. Define $g:Y\to{\mathbb{R} }$ by g(rx₀)=rp(x₀). Then g is a bounded linear functional on Y. Moreover, if $r\ge0$ then g(rx₀)=rp(x₀)=p(rx₀), and if r<0 then $g(rx_0)=rp(x_0)\le0\le p(rx_0)$, so $g\le p$ on Y. Thus, by our extended Hahn-Banach theorem 4.9 in $\mathsf{WKL}_0$, we can extend g to a bounded linear functional $f:X\to{\mathbb{R} }$ such that $f\le p$ on X.

Let $w\in W$ be given, and suppose y is such that $\Vert y\Vert\le1$. Then $\Vert(y-w+x_0)+w-x_0\Vert=\Vert y\Vert\le1$, whence $f(y-w+x_0)\le p(y-w+x_0)\le1$by definition of p. But f(y-w+x₀)=f(y)-f(w)+f(x₀) and $f(x_0)\ge1$, so $f(y)\le f(w)$. Replacing f by $f/\Vert f\Vert$, we see that $f\in B_1(X^*)$ and $f(x)\ge1$ for all x in the convex hull of Z. This completes the proof.

We conjecture that this separation principle is actually provable in $\mathsf{WKL}_0$ and not only in $\mathsf{ACA}_0$.

We now begin our treatment of the weak-* topology within $\mathsf{RCA}_0$. We start by introducing an $\mathsf{RCA}_0$ version of the bounded-weak-*topology:

Definition 4.11 (tex2html_wrap_inline$RCA_0$)   A (code for a) bounded-weak-*-closed set C in X^* is defined to be a sequence of (codes for) closed sets $C_n\subseteq B_n(X^*)$, $n\in{\mathbb{N} }$, such that

$$\forall m\,\forall n\,(m<n\longrightarrow C_m=B_m(X^*)\cap C_n)\,.$$

We write $x^*\in C$to mean $\exists n\,(x^*\in C_n)$, or equivalently $\forall n(n>\Vert x^*\Vert\rightarrow x^*\in C_n)$. A bounded-weak-*-open set in X^* is defined to be the complement of a bounded-weak-*-closed set in X^*.  

The next lemma formalizes within $\mathsf{ACA}_0$ 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.

Lemma 4.12   The following is provable in $\mathsf{ACA}_0$. Let X be a separable Banach space. If $\langle{}x_n\mid n\in{\mathbb{N} }\rangle{}$ is a sequence of points in X such that $x_n\to0$, then

$$\{x^*\in X^*\mid\forall n\,\vert x^*(x_n)\vert<1\}$$

contains 0 and is bounded-weak-*-open in X^*. Conversely, if U is a bounded-weak-*-open set in X^* containing 0, then we can find a sequence of points $\langle{}x_n\mid n\in{\mathbb{N} }\rangle{}$ in X such that $x_n\to0$ and $\{x^*\in X^*\mid\forall n\,\vert x^*(x_n)\vert\le1\}\subseteq U$.  

Proof. Reasoning in $\mathsf{ACA}_0$, let $\langle{}x_n\mid n\in{\mathbb{N} }\rangle{}$ be a sequence of points in X such that $\lim_nx_n=0$. By arithmetical comprehension, there exists a sequence of integers N_m, $m\in{\mathbb{N} }$, such that $\Vert x_n\Vert<1/m$for all $m\in{\mathbb{N} }$ and $n\ge N_m$. Using the sequence $\langle{}N_m\mid m\in{\mathbb{N} }\rangle{}$ as a parameter, we can define a sequence of closed sets $C_m\subseteq B_m(X^*)$, $m\in{\mathbb{N} }$, by

$$C_m=\{x^*\in B_m(X^*)\mid\exists n<N_m(\vert x^*(x_n)\vert\ge1)\}\,.$$

It is easy to verify that

$$C_m=\{x^*\in B_m(X^*)\mid\exists n\,\vert x^*(x_n)\vert\ge1\}$$

and hence $C_k=C_m\cap B_k(X^*)$ for all k<m. Thus by Definition 4.11 we have a bounded-weak-*-closed set $C=\bigcup_{m\in{\mathbb{N} }}C_m$ and clearly

$$X^*\setminus C=\{x^*\in X^*\mid\forall n\,\vert x^*(x_n)\vert<1\}\,.$$

This shows that $\{x^*\in X^*\mid\forall n\,\vert x^*(x_n)\vert<1\}$ is bounded-weak-*-open in X^*.

The proof of the converse will be carried out in $\mathsf{WKL}_0$. Let U be a bounded-weak-*-open set in X^* containing 0. Then $C=X^*\setminus U$ is a bounded-weak-*-closed set with $0\notin C$. For any countable set $S\subseteq X$ let S^o be the polar of S, i.e.,

$$S^o=\left\{x^*\in X^*\bigm\vert\forall x\in S\,\vert x^*(x)\vert\le 1\right\}\,.$$

To complete the proof, we need to construct a sequence of points $\langle{}x_k\mid k\in{\mathbb{N} }\rangle{}$ in X such that $\lim_kx_k=0$ and $\{x_k\mid k\in{\mathbb{N} }\}^o\cap C=\emptyset$.

Let $X={\widehat A}$ where A is a countable dense set in X. Put A₀=A and, for each $n\ge1$, $A_n=\{a\in A\mid\Vert a\Vert<1/n\}$. Claim: for any $n\in{\mathbb{N} }$ and any countable set $S\subseteq X$, if $S^o\cap B_n(X^*)\cap C=\emptyset$ then there exists a finite set $F\subset A_n$ such that $(S\cup F)^o\cap B_{n+1}(X^*)\cap C=\emptyset$. If such an F does not exist, then for all finite sets $F\subset A_n$ we would have $(S\cup F)^o\cap B_{n+1}(X^*)\cap C\neq\emptyset$, so by the Heine-Borel covering property of the compact set B_n+1(X^*) it would follow that

$$(S\cup A_n)^o\cap B_{n+1}(X^*)\cap C\neq\emptyset\,.$$

But $(S\cup A_n)^o=S^o\cap A_n^o=S^o\cap B_n(X^*)$, and hence $S^o\cap B_n(X^*)\cap C\neq\emptyset$, a contradiction. This proves the claim.

Within $\mathsf{WKL}_0$, we can apply the claim above repeatedly starting with $F_0=\emptyset$ to obtain a sequence of finite sets $F_{n+1}\subseteq A_n$, $n\in{\mathbb{N} }$, such that

$$(F_0\cup\ldots\cup F_n)^o\cap B_n(X^*)\cap C=\emptyset$$

for all $n\in{\mathbb{N} }$. The construction can be carried out effectively within $\mathsf{WKL}_0$ because, by Lemma 5.8 of [3], the predicates $F\subset A_n$ and $F^o\cap B_n(X^*)\cap C=\emptyset$ are provably in $\mathsf{WKL}_0$ equivalent to $\Sigma^0_1$ formulas. Thus the existence of a sequence of finite sets $\langle{}F_n\mid n\in{\mathbb{N} }\rangle{}$ with the mentioned properties is provable in $\mathsf{WKL}_0$.

Letting $\langle{}x_k\mid k\in{\mathbb{N} }\rangle{}$ be an enumeration without repetition of $\bigcup_{n\in{\mathbb{N} }}F_n$, it is clear that $x_k\to0$ in X and that $\{x_k\mid k\in{\mathbb{N} }\}^o\cap C=\emptyset$. This completes the proof.

We now introduce our $\mathsf{RCA}_0$ version of the weak-* topology.

Definition 4.13 (tex2html_wrap_inline$RCA_0$)   A weak-*-open set in X^* is defined to be a bounded-weak-*-open set U in X^* such that for all $x_0^*\in U$there exists a finite sequence of points $x_0,\ldots,x_{n-1}\in X$such that

$$\{x^*\in X^*\mid\forall k<n\,(\vert x^*(x_k)-x_0^*(x_k)\vert\le1)\}\subseteq U\,.$$

A weak-*-closed set in X^* is defined to be the complement of a weak-*-open set in X^*.  

According to the previous definition, we have trivially in $\mathsf{RCA}_0$ that any weak-*-closed set is bounded-weak-*-closed. In $\mathsf{ACA}_0$ we have following version of the Krein-Smulian theorem:

Theorem 4.14   The following is provable in $\mathsf{ACA}_0$. Let X be a separable Banach space. Suppose that $C\subseteq X^*$ is convex and bounded-weak-*-closed. Then C is weak-*-closed.  

Proof. Let $x_0^*\notin C$ be given. Then C-x₀^* is also bounded-weak-*-closed and convex, and $0\notin C-x_0^*$. Thus $(C-x_0^*)\cap B_n(X^*)$ is a closed subset of B_n(X^*) for each $n\in{\mathbb{N} }$. Since B_n(X^*) is compact, in $\mathsf{ACA}_0$ there exists a countable dense subset $D_n\subset (C-x_0^*)\cap B_n(X^*)$ 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₀^*, as this will show that x₀^*+N is disjoint from C. Let U be a bounded-weak-*-open set containing 0 which is disjoint from C-x₀^*. By Lemma 4.12, there is a sequence $\{x_n\mid n\in{\mathbb{N} }\}$ such that $x_n\to0$ and $\{x^*\in X^*\mid\forall n\vert x^*(x_n)\vert\le 1\}\subseteq U$.

Now, for each $m\in{\mathbb{N} }$, define a function $T_m:B_m(X^*)\to c_0$ by $T_m(x^*)=\langle{}x^*(x_n)\mid n\in{\mathbb{N} }\rangle{}$. 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 $T:X^*\to c_0$ by T(x^*)=T_m(x^*) where $x^*\in B_m(X^*)$. Notice that T is linear, and $\Vert T(x^*)\Vert\le1$implies $x^*\in U$ for all $x^*\in X^*$. Let D be an enumeration of the dense sets $D_n\subset (C-x_0^*)\cap B_n(X^*)$, and let E=T(D)(which exists by arithmetical comprehension); then E is a countable subset of c₀, and $\Vert x\Vert>1$ for all x in the convex hull of E. By Lemma 4.10 there exists $f\in B_1(c_0^*)=B_1(\ell_1)$ such that $f(x)\ge1$ for all x in the convex hull of E. Write $f=\langle{}\alpha_n:n\in{\mathbb{N} }\rangle{}\in\ell_1$.

Let $x=\sum_{n\in{\mathbb{N} }}\alpha_nx_n$; note that $\{x^*\in X^*\mid \vert x^*(x)\vert<1\}$ is weak-*-open and contains 0. Also, if $y^*\in C-x_0^*$ then $y^*\in B_m(X^*)$ for some m. Thus $\vert y^*(x)\vert=\vert\sum_{n\in{\mathbb{N} }}\alpha_ny^*(x_n)\vert=\vert f(T(y^*))\vert=\vert f(T_m(y^*))\vert\ge1$since D_m is dense in B_m(X^*) and f and T_m are continuous. So let $N=\{x^*\in X^*\mid \vert x^*(2x)\vert<1\}=\{x^*\in X^*\mid \vert x^*(x)\vert<1/2\}$; then N is weak-*-open, contains 0, and is disjoint from C-x₀^*. This completes the proof.

Specializing to subspaces of X^* (see also Corollary 2.8 above), we obtain:

Corollary 4.15   The following is provable in $\mathsf{ACA}_0$. Let X be a separable Banach space. Let C be a closed set in B₁(X^*) such that $C=B_1(X^*)\cap\mbox{\rm span}(C)$ where

$$\mbox{\rm span}(C)=\left\{\sum_{i=0}^na_i\,x^*_i\Bigm\vert a_i\in{\mathbb{R} }\,,\,x^*_i\in C\,,\,n\in{\mathbb{N} }\right\}\,.$$

Then $\mbox{\rm span}(C)$ is a weak-*-closed subspace of X^*.  

Proof. This follows easily from the previous theorem. See also the proof of Corollary 2.8.