SEPARABLE BANACH SPACE THEORY NEEDS STRONG SET EXISTENCE AXIOMS

A. JAMES HUMPHREYS AND STEPHEN G. SIMPSON

Abstract. We investigate the strength of set existence axioms needed for separable Banach space theory. We show that a very strong axiom, Π_{1}^{1} comprehension, is needed to prove such basic facts as the existence of the weak-∗ closure of any norm-closed subspace of ℓ_{1} = c_{0}^{∗}. This is in contrast to earlier work [5, 7, 6, 25, 22] in which theorems of separable Banach space theory were proved in very weak subsystems of second order arithmetic, subsystems which are conservative over Primitive Recursive Arithmetic for Π_{2}^{0} sentences. En route to our main results, we prove the Krein-Šmulian theorem in ACA_{0}, and we give a new, elementary proof of a result of McGehee on weak-∗ sequential closure ordinals.

1. Introduction

This paper is part of an ongoing study of the role of set existence axioms in the foundations of mathematics. The ongoing study has been carried out in the context of subsystems of second order arithmetic, under the slogan Reverse Mathematics [12, 3, 25]. We continue this program here by examining the role of strong set existence axioms in separable Banach space theory. We show that a very strong set existence axiom is needed in order to prove basic results concerning the weak-∗ topology on the dual of a separable Banach space.

The results in this paper are related to earlier work of Brown and Simpson [5, 7, 6, 25] and Shioji and Tanaka [22]. The earlier work shows that the basic notions of separable Banach space theory can be developed in very weak subsystems of second order arithmetic, and that many basic results can be proved in such systems. Specifically, the Hahn-Banach theorem and a version of the Schauder fixed point theorem are provable in WKL_{0}; the Banach-Steinhaus theorem is provable in RCA_{0}; and versions of the Open Mapping and Closed Graph theorems are provable in RCA_{0}^{+}. The set existence axioms of these three subsystems of second order arithmetic are very weak, in the sense that the systems themselves are conservative over Primitive Recursive Arithmetic for Π_{2}^{0} sentences (see Chapter IX of [25]). In particular, the mentioned systems are considerably weaker than first order arithmetic.

Date: May 17, 1995 Published in Transactions of the American Mathematical Society, 348, 1996, pp. 4231-4255.

1991 Mathematics Subject Classification. Primary 03F35; Secondary 46B10, 46B45.

Key words and phrases. Reverse mathematics, separable Banach space theory, weak-∗ topology, closure ordinals, Krein-Šmulian theorem.

This research was partially supported by NSF grant DMS-9303478. We would also like to thank our colleague Robert E. Huff for showing us his unpublished notes on the Krein-Šmulian theorem, and the referee for helpful comments which improved the exposition of this paper.

Thus the results of Brown and Simpson [5, 7, 6] may have tended to support the opinion that only very weak set existence axioms are needed for separable Banach space theory. Our main results here, Theorems 5.6 and 5.7 below, provide a counterexample to that opinion and a departure from Brown-Simpson-Shioji-Tanaka. Namely, Theorems 5.6 and 5.7 show that a very strong set existence axiom, Π_{1}^{1} comprehension, is needed in order to prove basic facts such as the existence of the weak-∗ closure of any norm-closed subspace of ℓ_{1} = c_{0}^{∗}. Thus Π_{1}^{1} comprehension is in a sense indispensable for separable Banach space theory. This is significant because Π_{1}^{1} comprehension is, of course, much stronger than first order arithmetic.

As a byproduct, we show that the Krein-Šmulian theorem for the dual of a separable Banach space (Theorem 2.7 below) is provable in ACA_{0} (Theorem 4.14 below). We conjecture that the Krein-Šmulian theorem for the dual of a separable Banach space is actually provable in the weaker system WKL_{0}.

Some of our results here may be of interest to readers who are familiar with Banach spaces but do not share our concern with Reverse Mathematics and other foundational issues. Namely, the following Banach space phenomenon may be of independent interest. Let Z be a subspace of the dual of a separable Banach space. Banach and Mazurkiewicz observed that, although the weak-∗ closure of Z is the same as the weak-∗ sequential closure of Z, it is not necessarily the case that every point of the weak-∗ closure of Z is the weak-∗ limit of a sequence of points of Z. Indeed, the process of taking weak-∗ limits of sequences may need to be iterated transfinitely many times in order to obtain the weak-∗ closure. In a self-contained part of this paper, we obtain a sharp result along these lines. Namely, for each countable ordinal α, we obtain an explicit example of a norm-closed, weak-∗ dense subspace of ℓ_{1} = c_{0}^{∗} whose weak-∗ sequential closure ordinal is exactly α + 1. This result is originally due to McGehee [18], but our examples are different and more elementary.

On the other hand, it is perhaps worth noting that our original motivation for the work here had nothing to do with Banach space theory. Rather, our starting point was another aspect of Reverse Mathematics, specifically the search for necessary uses of strong set existence axioms in classical (“hard”) analysis. We began with the thought that, in searching for necessary uses of strong set existence axioms, it would be natural to consider how Cantor was led to the invention or discovery of set theory in the first place. We were struck by the well known historical fact [9, 10] that Cantor introduced ordinal numbers in tandem with his study of trigonometric series and the structure of sets of uniqueness; see also Jourdain’s essay [8]. Indeed, Cantor’s proof that every countable closed set is a set of uniqueness uses transfinite induction on the Cantor-Bendixson rank of such sets. Therefore, from our Reverse Mathematics viewpoint, it is very natural to reexamine these results of Cantor. Although we postpone such reexamination to a future paper, we want to point out that our work here was inspired by a discussion of Kechris and Louveau [14, 13] culminating in a result attributed to Solovay: the Piatetski-Shapiro rank is a Π_{1}^{1}-rank on the set of closed sets of uniqueness. Since the Piatetski-Shapiro rank is the weak-∗ sequential closure ordinal of a certain weak-∗ dense subspace of ℓ_{1}, our foundational motivation for studying such ordinals is apparent.

We end this introductory section with a brief outline of the rest of the paper. Section 2 reviews the concepts and results of Banach space theory that are important for us here. In particular we review the weak-∗ topology and define the notion of the weak-∗ sequential closure ordinal of an arbitrary set in the dual of a separable Banach space. In Section 3 we exhibit the previously mentioned examples concerning weak-∗ sequential closure ordinals, using the concept of a smooth tree. These two sections, Sections 2 and 3, are intended to form a self-contained unit which should be accessible to anyone who is familiar with the notion of a Banach space. Our discussion of subsystems of second order arithmetic does not get under way until Section 4. We begin that section by reviewing the definitions and results from Brown-Simpson [5, 7, 6, 25] that we shall need. We then discuss the weak-∗ topology and related notions in the Brown-Simpson context. We end Section 4 by proving our version of the Krein-Šmulian theorem within ACA_{0}. Finally, in Section 5, we state and prove our main theorem, concerning the need for Π_{1}^{1} comprehension. The ideas of Section 3 are used in the proof of the main theorem in Section 5.

2. Banach space preliminaries

The purpose of this section is to review some well-known concepts and results from separable Banach space theory. Our focus is the weak-∗ topology on the dual of a separable Banach space. A reference for most of this material is Chapter V of Dunford and Schwartz [11].

Let X be a Banach space. The weak topology on X is the weakest topology such that every bounded linear functional on X is continuous. The dual space of X is the space X^{∗} of all bounded linear functionals on X. The norm of x^{∗} ∈ X^{∗} is defined by

∥x^{∗}∥ = sup{|x^{∗}(x)| | ∥x∥ ≤ 1} .

The weak-∗ topology on X^{∗} is the weakest topology such that for all x ∈ X the functional x^{∗} ↦ x^{∗}(x) is continuous. The weak-∗ closure of a set Z ⊆ X^{∗} is denoted cl*(Z). Note that about any point x_{0}^{∗} ∈ X^{∗} there is a weak-∗ neighborhood basis consisting of all sets of the form

{x^{∗} ∈ X^{∗} | |x^{∗}(x_{1}) − x_{0}^{∗}(x_{1})| < 1, …, |x^{∗}(x_{n}) − x_{0}^{∗}(x_{n})| < 1}

for some finite set x_{1}, …, x_{n} ∈ X.

A key theorem concerning the weak-∗ topology is:

Theorem 2.1 (Banach-Alaoglu). For any r > 0, the closed ball

B_{r}(X^{∗}) = {x^{∗} ∈ X^{∗} | ∥x^{∗}∥ ≤ r}

is weak-∗ closed and weak-∗ compact. Furthermore, if X is separable then B_{r}(X^{∗}) is weak-∗ metrizable.

Proof. See [11], page 424.

In considering weak-∗ sequential convergence, an important fact to keep in mind is the following consequence of the Banach-Steinhaus theorem:

Theorem 2.2. Let {x_{n}^{∗} | n ∈ ℕ} be a countable set of points in X^{∗}. If sup_{n} |x_{n}^{∗}(x)| < ∞ for all x ∈ X, then sup_{n} ∥x_{n}^{∗}∥ < ∞.

Proof. See [11], page 66.

Corollary 2.3. If x_{n}^{∗} → x^{∗} in the weak-∗ topology in X^{∗}, then {x_{n}^{∗} | n ∈ ℕ} is bounded, i.e., {x_{n}^{∗} | n ∈ ℕ} ⊆ B_{r}(X^{∗}) for some 0 < r < ∞.

A set Z ⊆ X^{∗} is said to be weak-∗ sequentially closed if it is closed under weak-∗ limits of sequences, i.e., x_{n}^{∗} → x^{∗} weak-∗ and x_{n}^{∗} ∈ Z for all n ∈ ℕ imply x^{∗} ∈ Z.

Corollary 2.4. A set Z ⊆ X^{∗} is weak-∗ sequentially closed if and only if Z ∩ B_{r}(X^{∗}) is weak-∗ sequentially closed for all r > 0.

For an arbitrary set Z ⊆ X^{∗}, being weak-∗ sequentially closed is not in general equivalent to being weak-∗ closed. In particular, the weak-∗ topology is not in general metrizable, even when X is separable. This is shown by the following theorem.

Theorem 2.5. Let X be an infinite-dimensional separable Banach space. Then we can find a countable set Z ⊂ X^{∗} such that Z is weak-∗ sequentially closed yet weak-∗ dense in X^{∗}.

Proof. We first prove the following lemma.

Lemma 2.6. Let X be an infinite-dimensional Banach space. Then we can find a sequence of points ⟨x_{k} | k ∈ ℕ⟩ in X such that lim_{k} ∥x_{k}∥ = ∞ and ∥x_{k}∥ > 1 for all k ∈ ℕ, yet 0 belongs to the weak closure of {x_{k} | k ∈ ℕ}.

Proof. For any finite set F ⊂ X^{∗}, {x ∈ X | y^{∗}(x) = 0 for all y^{∗} ∈ F } is a subspace of X of codimension at most the cardinality of F, and hence in particular it intersects {x ∈ X | ∥x∥ > n} for each n ∈ ℕ. By the Banach-Alaoglu theorem, B_{n}(X^{∗}) is weak-∗ compact, and so B_{n}(X^{∗})^{n} is weak-∗ compact as well. Thus for each n we can find a finite set G_{n} ⊂ {x ∈ X | ∥x∥ > n} such that, for each finite set F ⊂ B_{n}(X^{∗}) of cardinality n, {x ∈ X | |y^{∗}(x)| < 1 for all y^{∗} ∈ F } intersects G_{n}. Letting {x_{k} | k ∈ ℕ} be an enumeration without repetition of ⋃_{n=1}^{∞} G_{n}, we obtain the desired sequence.

Proof of Theorem 2.5. Since X is separable, it follows by Theorem 2.1 that X^{∗} is weak-∗ separable, so let {x_{n}^{∗} | n ∈ ℕ} be a countable weak-∗ dense subset of X^{∗}. By the preceding lemma, for each n we can find a sequence ⟨z_{nk}^{∗} | k ∈ ℕ⟩ such that ∥z_{nk}^{∗}∥ > n for all k and lim_{k} ∥z_{nk}^{∗}∥ = ∞ and x_{n}^{∗} belongs to the weak, and hence weak-∗, closure of {z_{nk}^{∗} | k ∈ ℕ}. Thus Z = {z_{nk}^{∗} | n, k ∈ ℕ} is a countable set which is weak-∗ dense in X^{∗}. On the other hand, for each n, Z ∩B_{n}(X^{∗}) is finite, so by Corollary 2.4 Z is weak-∗ sequentially closed.

The previous theorem shows that a set in X^{∗} can be weak-∗ sequentially closed yet far from weak-∗ closed, even when X is separable. Nevertheless, it turns out that for convex sets in X^{∗}, being weak-∗ sequentially closed is equivalent to being weak-∗ closed, provided X is separable. We shall obtain this result as a consequence of the following well-known theorem:

Theorem 2.7 (Krein-Šmulian). Let X be a Banach space. A convex set in X^{∗} is weak-∗ closed if and only if its intersection with B_{r}(X^{∗}) is weak-∗ closed for every r > 0.

Proof. See [11], page 429.

The special case of the Krein-Šmulian theorem for subspaces of X^{∗} is originally due to Banach ([2] page 124):

Corollary 2.8 (Banach). A subspace of X^{∗} is weak-∗ closed if and only if its intersection with B_{1}(X^{∗}) is weak-∗ closed.

Proof. For a subspace Z of X^{∗}, we have Z ∩ B_{r}(X^{∗}) = r(Z ∩ B_{1}(X^{∗})). Hence Z ∩ B_{r}(X^{∗}) is weak-∗ closed for all r if and only if Z ∩ B_{1}(X^{∗}) is weak-∗ closed. The desired result follows immediately from the Krein-Šmulian theorem.

A set Z in X^{∗} is said to be bounded-weak-∗ closed if Z ∩ B_{r}(X^{∗}) is weak-∗-closed for all r > 0. This defines yet another topology on X^{∗}, the bounded-weak-∗ topology. By the Banach-Alaoglu theorem, weak-∗ closed sets are bounded-weak-∗ closed, but the converse does not hold in general. We can paraphrase the Krein-Šmulian theorem by saying that a convex set in X^{∗} is weak-∗ closed if and only if it is bounded-weak-∗ closed.

Lemma 2.9. Let X be a separable Banach space. A set Z ⊆ X^{∗} is bounded-weak-∗ closed if and only if it is weak-∗ sequentially closed.

Proof. By definition, Z is bounded-weak-∗ closed if and only if Z ∩ B_{r}(X^{∗}) is weak-∗ closed for all r. Since X is separable, we have by Theorem 2.1 that B_{r}(X^{∗}) is weak-∗ compact and weak-∗ metrizable. Hence, for all r, Z ∩ B_{r}(X^{∗}) is weak-∗ closed if and only if Z ∩ B_{r}(X^{∗}) is weak-∗ sequentially closed. By Corollary 2.4 it now follows that Z ∩ B_{r}(X^{∗}) is weak-∗ closed for all r if and only if Z is weak-∗ sequentially closed. This completes the proof.

We now obtain the desired result:

Theorem 2.10. Let X be a separable Banach space. A convex set Z ⊆ X^{∗} is weak-∗ closed if and only if it is weak-∗ sequentially closed.

Proof. Immediate from Theorem 2.7 plus Lemma 2.9.

Again, the special case when Z is a subspace of X^{∗} is due to Banach ([2] page 124):

Corollary 2.11 (Banach). Let X be a separable Banach space. A subspace Z of X^{∗} is weak-∗ closed if and only if it is weak-∗ sequentially closed.

We now turn to a discussion of weak-∗ sequential closure ordinals. For an arbitrary set Z ⊆ X^{∗}, let Z′ denote the set of weak-∗ limits of sequences from Z. Define a transfinite sequence of sets Z^{(α)}, α an ordinal, by

Z^{(0)} = Z ,
Z^{(α+1)} = (Z^{(α)})′ ,
Z^{(δ)} = ⋃_{α<δ} Z^{(α)} for δ a limit ordinal .

Clearly α < β implies Z^{(α)} ⊆ Z^{(β)}. Define ord(Z) to be the least ordinal α such that Z^{(α+1)} = Z^{(α)}. Thus Z^{(ord(Z))} is the weak-∗ sequential closure of Z. We call ord(Z) the closure ordinal of Z. Note that if Z is convex, then Z^{(α)} is convex for all α; also, by the previous theorem Z^{(ord(Z))} = cl*(Z), the weak-∗ closure of Z.

In the remainder of this section and the next section, we shall prove some results which completely answer the question of which ordinals can arise as closure ordinals of subspaces of X^{∗} where X is a separable Banach space. This question was first answered completely by McGehee [18] and Sarason [19, 20, 21].

Lemma 2.12. If X is a separable Banach space, then for any set Z ⊆ X^{∗} the closure ordinal ord(Z) is countable.

Proof. For r > 0 and α an ordinal, let C_{r}^{α} be the weak-∗ closure of Z^{(α)} ∩ B_{r}(X^{∗}). For fixed r > 0, the sets C_{r}^{α} form an increasing, transfinite sequence of compact subsets of a compact metric space, namely B_{r}(X^{∗}) with the weak-∗ topology (Theorem 2.1). This transfinite sequence must therefore stabilize at some countable ordinal. Since C_{r}^{α} ⊆ Z^{(α+1)} ∩ B_{r}(X^{∗}) ⊆ C_{r}^{α+1} for all α, it follows that the transfinite sequence Z^{(α)} ∩ B_{r}(X^{∗}) also stabilizes at a countable ordinal, call it α_{r}. Put α = sup{α_{n} | n ∈ ℕ}. Then α is a countable ordinal. We claim that Z^{(α)} is weak-∗ sequentially closed. To see this, suppose that x^{∗} is the weak-∗ limit of a sequence ⟨x_{k}^{∗} | k ∈ ℕ⟩ from Z^{(α)}. By Corollary 2.3, there exists n ∈ ℕ such that x_{k}^{∗} ∈ B_{n}(X^{∗}) for all k ∈ ℕ. Hence x^{∗} ∈ Z^{(α+1)} ∩ B_{n}(X^{∗}) = Z^{(α)} ∩ B_{n}(X^{∗}), so in particular x^{∗} ∈ Z^{(α)} and our claim is proved. Thus ord(Z) ≤ α < ω_{1}, i.e., ord(Z) is countable.

Specializing to subspaces of X^{∗}, we can say more:

Theorem 2.13. Let X be a separable Banach space and let Z be a subspace of X^{∗}. Then the closure ordinal ord(Z) is a countable successor ordinal, unless Z is already weak-∗ closed, in which case ord(Z) = 0.

Proof. By the previous lemma, ord(Z) is countable. Suppose that cl*(Z) = Z^{(δ)} = ⋃_{α<δ} Z^{(α)}, for some countable limit ordinal δ. As cl*(Z) is norm closed, this implies that cl*(Z) = ⋃_{α<δ} cl(Z^{(α)}), where cl(Y) denotes the norm closure of Y ⊆ X^{∗}. Thus cl*(Z) is a closed subset of a complete metric space, written as a countable union of closed sets. By the Baire category theorem, there must be an ordinal α < δ such that cl(Z^{(α)}) has non-void interior as a subset of cl*(Z), i.e., cl(Z^{(α)}) contains the intersection of an open (in norm) ball with cl*(Z). But cl(Z^{(α)}) is a subspace of cl*(Z), so it must be all of cl*(Z). Since cl(Z^{(α)}) ⊆ Z^{(α+1)}, it follows that Z^{(α+1)} = cl*(Z), whence ord(Z) ≠ δ. We have now shown that ord(Z) is not a limit ordinal. Thus ord(Z) must be either 0 or a successor ordinal. If ord(Z) = 0 then Z is weak-∗ sequentially closed, and hence is weak-∗ closed by Corollary 2.11. This completes the proof. See also Kechris and Louveau [14], page 157.

It is known that the converse of the previous theorem also holds: For every countable successor ordinal α + 1, we can find a subspace Z of the dual X^{∗} of a separable Banach space X such that ord(Z) = α + 1. In the next section we present a proof of this result, with Z ⊆ ℓ_{1} = c_{0}^{∗} and Z weak-∗ dense in ℓ_{1}.

The study of closure ordinals of subspaces of X^{∗} has an interesting history. Von Neumann ([26] page 380) exhibits a set S ⊂ ℓ_{2} such that 0 is in the weak closure of S yet no sequence from S converges weakly to 0. The first example of a subspace Z of X^{∗} such that ord(Z) ≥ 2 is due to Mazurkiewicz [17]. Banach ([2] pages 209–213) proves that for every n ∈ ℕ there is a subspace Z of ℓ_{1} = c_{0}^{∗} such that ord(Z) ≥ n and states the analogous result for all countable ordinals. For the proof Banach refers to a “forthcoming” paper which seems never to have appeared, and this reference is omitted from the English translation [1]. Later, McGehee [18] proves the stronger result that for each countable ordinal α there exists a weak-∗ dense subspace of ℓ_{1} = c_{0}^{∗} whose closure ordinal is exactly α +1 (but note that McGehee’s notation differs from ours). In the next section we reprove this result of McGehee. Sarason [19, 20, 21] proves a similar result for the spaces H^{∞} and ℓ_{∞}. In view of the theorem above, these results of McGehee and Sarason are in a sense best possible. While McGehee’s proof uses sets of synthesis and uniqueness, our proof in the next section is much more elementary.

3. Trees and subspaces of ℓ_{1}

In this section we prove the following result: For each countable ordinal α, there exists a weak-∗ dense subspace Z of ℓ_{1} = c_{0}^{∗} such that ord(Z) = α + 1. Our proof uses some simple concepts and results concerning trees. We give a self-contained treatment of these auxiliary results.

Definition 3.1. Let Seq denote the set of finite sequences of natural numbers, i.e.,

Seq = ⋃_{k=0}^{∞} ℕ^{k} = {⟨n_{0}, …, n_{k−1}⟩ | k ∈ ℕ, n_{i} ∈ ℕ for all i < k} .

For s = ⟨n_{0}, …, n_{k−1}⟩ ∈ Seq, we write

s = ⟨s(0), s(1), …, s(lh(s) − 1)⟩ ,

where lh(s) = k denotes the length of s, and s(i) = n_{i} for all i < lh(s). In particular ⟨⟩ is the empty sequence, the unique sequence of length 0. For s, t ∈ Seq we denote by s^{⌢}t the concatenation of s and t, i.e., the sequence of length lh(s) + lh(t) given by

s^{⌢}t = ⟨s(0), …, s(lh(s) − 1), t(0), …, t(lh(t) − 1)⟩ .

For s, t ∈ Seq, we write s ⊆ t to mean that s is an initial segment of t, i.e., lh(s) ≤ lh(t) and, for all i < lh(s), s(i) = t(i). Given s ∈ Seq, if s ≠ ⟨⟩ let

s′ = ⟨s(0), s(1), …, s(lh(s) − 2)⟩ ,

i.e., s′ is the initial segment of s of length lh(s) − 1. For s = ⟨⟩ we put s′ = ⟨⟩′ = ⟨⟩.

Definition 3.2. We define a tree to be a nonempty set T ⊆ Seq which is closed under taking initial segments, i.e., for all s, t ∈ Seq, if t ∈ T and s ⊆ t then s ∈ T. If T is a tree and s ∈ T, we say that s is a node of T. If s is a node of T such that s^{⌢}⟨n⟩ ∉ T for all n ∈ ℕ, then s is called an end node; otherwise s is called an interior node of T. Given a tree T, a function f : ℕ → ℕ is called a path through T if for all n ∈ ℕ we have f[n] ∈ T, where f[n] = ⟨f(0), f(1), …, f(n − 1)⟩. A tree T is said to be well-founded if it has no path.

Definition 3.3. If T is a tree, let

T′ = {t′ | t ∈ T } = {interior nodes of T } ∪ {⟨⟩} .

Note that T′ is a subtree of T. We define a transfinite sequence of subtrees T^{(α)} of T by

T^{(0)} = T ,
T^{(α+1)} = (T^{(α)})′ ,
T^{(δ)} = ⋂_{α<δ} T^{(α)} for δ a limit ordinal .

Note that T is well-founded if and only if T^{(α)} = {⟨⟩} for some countable ordinal α. The least such α is called the height of T, denoted h(T). Given a well-founded tree T, we define a function h_{T} : Seq → Ord ∪ {−1} (where Ord denotes the set of countable ordinals) by h_{T} (s) = −1 for s ∉ T and, for s ∈ T, h_{T} (s) = the least α such that s is an end node of T^{(α)}. In particular h_{T} (⟨⟩) = h(T). Note that, for all s ∈ T, h_{T} (s) = sup{h_{T} (s^{⌢}⟨n⟩) + 1 | n ∈ ℕ}.

From the definition above, the height of a well-founded tree is a countable ordinal. The following standard theorem shows that the converse holds as well.

Theorem 3.4. For any countable ordinal α, we can construct a well-founded tree T such that h(T) = α.

Proof. We prove this by transfinite induction on α. For α = 0 we have h({⟨⟩}) = 0. For successor ordinals, note that if h(T) = α, then h(T^{+}) = α + 1 where T^{+} = {⟨⟩} ∪ {⟨0⟩^{⌢}s | s ∈ T }. Suppose now that δ is a limit ordinal, say δ = sup{α_{n} | n ∈ ℕ}, where α_{n} < δ for all n ∈ ℕ. For each n let T_{n} be a tree of height α_{n}, and put T = {⟨⟩} ∪ {⟨n⟩^{⌢}s | n ∈ ℕ, s ∈ T_{n}}. Then T is well-founded and, for each n ∈ ℕ, h_{T} (⟨n⟩) = α_{n}. Thus h(T) = sup{α_{n} + 1 | n ∈ ℕ} = δ.

Definition 3.5. Fix an injection # : Seq → ℕ with the following properties:

1. #(⟨⟩) = 1;

2. s ⊆ t implies #(s) ≤ #(t);

3. m < n implies #(s^{⌢}⟨m⟩) < #(s^{⌢}⟨n⟩). Given s ∈ Seq we refer to #(s) as the Gödel number of s. To simplify notation in what follows, we shall often identify sequences with their Gödel numbers, i.e., we write s instead of #(s).

Let X = c_{0}(Seq), the space of sequences of real numbers converging to 0 indexed by Seq. Then we may identify X^{∗} with ℓ_{1}(Seq), the space of absolutely summable sequences of real numbers indexed by Seq. In the rest of this section we shall mainly be interested in the weak-∗ topology on ℓ_{1}(Seq) = c_{0}^{∗}(Seq).

Definition 3.6. For each s ∈ Seq we define a distinguished point y_{s} ∈ ℓ_{1}(Seq) by

y_{s}(t) = \begin{cases}#(t′) & if t ⊆ s, \\ 0 & otherwise. \end{cases}

Using the convention that sequences are to be identified with their Gödel numbers, we can write y_{s}(t) = t′ if t ⊆ s, 0 otherwise. Note that, for all s ∈ Seq, the sequence ⟨y_{s^{⌢}⟨n⟩}: n ∈ ℕ⟩, converges weak-∗ to y_{s} in ℓ_{1}(Seq).

Definition 3.7. Given s ∈ Seq we set

Z_{s} = \{z ∈ ℓ_{1}(Seq) | \frac{1}{s′} z(s) = \frac{1}{s} ∑_{m∈ℕ}z(s^{⌢}⟨m⟩)\} .

If S ⊆ Seq, let Z_{S} = ⋂_{s∈S} Z_{s}. Note that Z_{S} is a norm closed subspace of ℓ_{1}(Seq). Note also that y_{s} ∈ Z_{S} if and only if s ∉ S.

The next two lemmas imply that, for any well-founded tree T, Z_{T} is weak-∗ dense in ℓ_{1}(Seq).

Lemma 3.8. If T is a well-founded tree, then y_{s} ∈ Z_{T}^{(h_{T} (s)+1)} for all s ∈ Seq.

Proof. We proceed by induction on h_{T} (s). If h_{T} (s) = −1 then s ∉ T and y_{s} ∈ Z_{T} = Z_{T}^{(0)}. Suppose now that h_{T} (s) = α ≥ 0, and that the theorem holds for all t such that h_{T} (t) < α. Then for each n ∈ ℕ, h_{T} (s^{⌢}⟨n⟩) < α, so y_{s^{⌢}⟨n⟩} ∈ Z_{T}^{(α)} for all n ∈ ℕ. Since y_{s} is the weak-∗ limit of the sequence ⟨y_{s^{⌢}⟨n⟩}: n ∈ ℕ⟩, it follows that y_{s} ∈ Z_{T}^{(α+1)}, as desired.

Lemma 3.9. If T is a well-founded tree, then Z_{T} is weak-∗ dense in ℓ_{1}(Seq); in fact, Z_{T}^{(h(T)+1)} = ℓ_{1}(Seq).

Proof. Let z ∈ ℓ_{1}(Seq) be given. We can write z = ∑_{s∈Seq} z(s)χ_{s}, where χ_{s} ∈ ℓ_{1}(Seq) is the characteristic function of {s}, i.e., χ_{s}(t) = 1 if t = s, 0 otherwise. Note that if s ≠ ⟨⟩ then y_{s} − y_{s′} = s′χ_{s}, whereas y_{⟨⟩} = χ_{⟨⟩}. Also, by the previous lemma, if s ≠ ⟨⟩ then y_{s} ∈ Z_{T}^{(h(T))}, so, if lh(s) > 1 then χ_{s} ∈ Z_{T}^{(h(T))}. Since z is an absolutely summable series, we have

∑_{s∈Seq} z(s)χ_{s} = z(⟨⟩)y_{⟨⟩} + ∑_{m∈ℕ}z(⟨m⟩)χ_{⟨m⟩} + ∑_{\begin{matrix}s∈Seq \\ lh(s)>1 \end{matrix}} z(s)χ_{s}

= z(⟨⟩)y_{⟨⟩} + ∑_{m∈ℕ}z(⟨m⟩)(y_{⟨m⟩} − y_{⟨⟩}) + ∑_{lh(s)>1} z(s)χ_{s}

= (z(⟨⟩) − ∑_{m∈ℕ}z(⟨m⟩)) y_{⟨⟩} + ∑_{m∈ℕ}z(⟨m⟩)y_{⟨m⟩} + ∑_{lh(s)>1} z(s)χ_{s} .

Now, z(⟨⟩)−∑_{m∈ℕ} z(⟨m⟩) is just a real number since z is absolutely summable, and y_{⟨⟩} is the weak-∗ limit of the sequence ⟨y_{⟨m⟩}: m ∈ ℕ⟩, so the first term in this last sum is in Z_{T}^{(h(T)+1)}. Likewise ∑_{m∈ℕ} z(⟨m⟩)y_{⟨m⟩}+∑_{lh(s)>1} z(s)χ_{s}, viewed as a series in ℓ_{1}(Seq), converges in norm, and hence converges weak-∗; since the functionals y_{⟨m⟩} and χ_{s} are in Z_{T}^{(h(T))} for all m ∈ ℕ and all s ∈ Seq with lh(s) > 1, it, too, is the weak-∗ limit of a sequence from Z_{T}^{(h(T))}. Hence z is the sum of two weak-∗ limits of sequences from Z_{T}^{(h(T))}, whence z is in Z_{T}^{(h(T)+1)} as desired.

Corollary 3.10. If T is a well-founded tree, then ord(Z_{T}) ≤ h(T) + 1.

Thus we have an upper bound on the closure ordinal of Z_{T} in terms of the height of T. To get a lower bound, we use the following technical lemma, which gives us a handle on the growth of the spaces Z_{T}^{(α)}.

Lemma 3.11. Suppose that z_{k} → z weak-∗ in ℓ_{1}(Seq) = c_{0}^{∗}(Seq). Let s ∈ Seq be given and suppose that z_{k} ∈ Z_{s} for all k ∈ ℕ. A sufficient condition for z ∈ Z_{s} is the existence of M ∈ ℕ such that z_{k} ∈ Z_{s^{⌢}⟨m⟩} for all k ∈ ℕ and all m ≥ M.

Proof. Assume that the stated condition holds. Suppose for a contradiction that z ∉ Z_{s}, say

|\frac{1}{s′} z(s) − \frac{1}{s} ∑_{m=0}^{∞} z(s^{⌢}⟨m⟩)| > ε > 0 .

Then for all sufficiently large M we have

|\frac{1}{s′} z(s) − \frac{1}{s} ∑_{m<M} z(s^{⌢}⟨m⟩)| > ε .

Fix such an M, with z_{k} ∈ Z_{s^{⌢}⟨m⟩} for all k ∈ ℕ and all m ≥ M as well. Then for all sufficiently large k we have

|\frac{1}{s′} z_{k}(s) − \frac{1}{s} ∑_{m<M} z_{k}(s^{⌢}⟨m⟩)| > ε ,

and hence

ε < |\frac{1}{s} ∑_{m≥M} z_{k}(s^{⌢}⟨m⟩)|  (since z_{k} ∈ Z_{s})

≤ \frac{1}{s} ∑_{m≥M} |z_{k}(s^{⌢}⟨m⟩)|

= \frac{1}{s} ∑_{m≥M} |\frac{s}{s^{⌢}⟨m⟩} ∑_{n=0}^{∞} z_{k}(s^{⌢}⟨m, n⟩)|  (since z_{k} ∈ Z_{s^{⌢}⟨m⟩} for all m ≥ M)

≤ \frac{1}{s^{⌢}⟨M⟩} ∑_{m≥M} ∑_{n=0}^{∞} |z_{k}(s^{⌢}⟨m, n⟩)|

≤ \frac{∥z_{k}∥}{s^{⌢}⟨M⟩} ,

and hence ∥z_{k}∥ > (s^{⌢}⟨M⟩)ε. Thus {∥z_{k}∥ | k ∈ ℕ} is unbounded, contradicting Corollary 2.3.

In particular, we have the following result.

Corollary 3.12. Let S ⊆ Seq be such that, for each s ∈ S, s^{⌢}⟨m⟩ ∈ S for all but finitely many m ∈ ℕ. Then Z_{S} is weak-∗ closed.

Proof. By Lemma 3.11 Z_{S} is weak-∗ sequentially closed. Hence by Corollary 2.11 Z_{S} is weak-∗ closed.

In order to make use of this lemma, we consider a special class of trees known as smooth trees:

Definition 3.13. For s, t ∈ Seq we say s is majorized by t, written s \underline{≪} t, if lh(s) = lh(t) and s(i) ≤ t(i) for all i < lh(s). For any tree T, we define T^{∗} to be the upward closure of T under majorization, i.e.,

T^{∗} = \{t ∈ Seq | ∃s ∈ T (s \underline{≪} t)\} .

A tree T is said to be smooth if it is upward closed under majorization, i.e., T^{∗} = T.

Lemma 3.14 (Marcone [15, 16]). Let T be a tree. Then T is well-founded if and only if T^{∗} is well-founded, in which case h(T) = h(T^{∗}).

Proof. Note first that T ⊆ T^{∗}, so if T^{∗} is well-founded then so is T. Conversely, suppose T^{∗} has a path f; let T_{f} = \{s ∈ T | s \underline{≪} f[lh(s)]\}. Then T_{f} is a finitely-branching subtree of T, and, since f is a path through T^{∗}, T_{f} must be infinite. Hence by König’s Lemma T_{f} has a path, whence T has a path.

Assuming T and T^{∗} are well-founded, we obviously have h(T) ≤ h(T^{∗}). For the opposite inequality, we claim that for all s, h_{T^{∗}}(s) = max\{h_{T} (t) | t \underline{≪} s\}. (Note that \{t | t \underline{≪} s\} is a finite set, so we may take max rather than sup.) We prove the claim by induction on h_{T^{∗}}(s). If h_{T^{∗}}(s) = −1 then s ∉ T^{∗}, so for any t with t \underline{≪} s we have t ∉ T, whence h_{T} (t) = −1 for all such t. Otherwise s ∈ T^{∗} and we have

h_{T^{∗}}(s) = sup{h_{T^{∗}}(s^{⌢}⟨n⟩) + 1 | n ∈ ℕ}
= sup\{max\{h_{T} (t^{⌢}⟨m⟩) + 1 | t \underline{≪} s, m ≤ n\} | n ∈ ℕ\}
= sup\{h_{T} (t^{⌢}⟨n⟩) + 1 | t \underline{≪} s, n ∈ ℕ\}
= max\{sup\{h_{T} (t^{⌢}⟨n⟩) + 1 | n ∈ ℕ\} | t \underline{≪} s\}
= max\{h_{T} (t) | t \underline{≪} s\} .

This proves our claim. In particular h(T^{∗}) = h_{T^{∗}}(⟨⟩) = h_{T} (⟨⟩) = h(T) and the proof of the lemma is complete.

Corollary 3.15. For any countable ordinal α, there exists a smooth well-founded tree T such that h(T) = α.

Proof. This follows immediately from Theorem 3.4 and the previous lemma.

Lemma 3.16. If T is a smooth tree, then T^{(α)} is smooth for all α.

Proof. We proceed by induction on α. For α = 0 there’s nothing to prove. Assume T^{(α)} is smooth, and let s ∈ T^{(α+1)} be given. Suppose s \underline{≪} t; since s ∈ T^{(α+1)} ⊆ T^{(α)} which is smooth, t must be in T^{(α)}; furthermore, since s is an interior node of T^{(α)}, there is an m ∈ ℕ such that s^{⌢}⟨m⟩ ∈ T^{(α)}. But s^{⌢}⟨m⟩ \underline{≪} t^{⌢}⟨m⟩, so t^{⌢}⟨m⟩ ∈ T^{(α)}, whence t ∈ T^{(α+1)}. Finally, smoothness is clearly preserved under intersections, so the induction goes through at limit stages.

Lemma 3.17. Let T be a smooth well-founded tree. Then for all α ≤ h(T), Z_{T}^{(α)} ⊆ Z_{T^{(α)}}.

Proof. We proceed by induction on α. If α = 0 there’s nothing to prove. Assume Z_{T}^{(α)} ⊆ Z_{T^{(α)}} and α < h(T) and let z ∈ Z_{T}^{(α+1)} be given. Then z is the weak-∗ limit of some sequence ⟨z_{k} | k ∈ ℕ⟩ from Z_{T}^{(α)} ⊆ Z_{T^{(α)}}. Since α < h(T), we have that any s ∈ T^{(α+1)} is an interior node of T^{(α)}, i.e., s ∈ T^{(α)} and s^{⌢}⟨M⟩ ∈ T^{(α)} for some M. Since T is smooth, so is T^{(α)}, and hence s^{⌢}⟨m⟩ ∈ T^{(α)} for all m ≥ M. Hence, for each k ∈ ℕ we have z_{k} ∈ Z_{s} and z_{k} ∈ Z_{s^{⌢}⟨m⟩} for all m ≥ M. By Lemma 3.11 it follows that z ∈ Z_{s}. Since s is an arbitrary node in T^{(α+1)}, we have z ∈ Z_{T^{(α+1)}}. This shows that Z_{T}^{(α+1)} ⊆ Z_{T^{(α+1)}}. Finally, if δ is a limit ordinal ≤ h(T) and Z_{T}^{(α)} ⊆ Z_{T^{(α)}} for all α < δ, it follows easily that Z_{T^{(α)}} ⊆ Z_{T^{(δ)}} for all α < δ, whence Z_{T}^{(δ)} ⊆ Z_{T^{(δ)}}. This completes the proof.

Corollary 3.18. If T is a smooth well-founded tree, then ord(Z_{T}) = h(T) + 1.

Proof. By Lemma 3.9 we have Z_{T}^{(ord(Z_{T}))} = ℓ_{1}(Seq) and ord(Z_{T}) ≤ h(T) + 1. On the other hand, T^{(h(T))} = {⟨⟩} so y_{⟨⟩} ∉ Z_{T^{(h(T))}}; hence, by the previous lemma, y_{⟨⟩} ∉ Z_{T}^{(h(T))} so in particular Z_{T}^{(h(T))} ≠ ℓ_{1}(Seq), and hence h(T) < ord(Z_{T}). This completes the proof.

We now obtain the main result of this section, originally due to McGehee [18]:

Theorem 3.19. For any countable ordinal α, there exists a weak-∗ dense subspace Z of ℓ_{1} = c_{0}^{∗} such that ord(Z) = α + 1.

Proof. Since Seq is a countably infinite set, we may identify ℓ_{1} = c_{0}^{∗} with ℓ_{1}(Seq) = c_{0}^{∗}(Seq). By Corollary 3.15 let T be a smooth well-founded tree of height α. By Lemma 3.9 Z_{T} is weak-∗ dense in ℓ_{1} and by Corollary 3.18 we have ord(Z_{T}) = h(T) + 1 = α + 1.

Corollary 3.20. The ordinals which can occur as closure ordinals of subspaces of the dual of a separable Banach space are precisely the countable non-limit ordinals.

Proof. This is immediate from Theorems 2.13 and 3.19. The result is originally due to Sarason [19, 20, 21] and McGehee [18].

This settles the question of closure ordinals of subspaces of ℓ_{1} = c_{0}^{∗}, but what about ℓ_{2}? It turns out that the answer is much simpler (see Corollary 3.23 below).

Theorem 3.21. Let X be a Banach space, and let C ⊆ X be convex. Then for any x ∈ X, the following conditions are equivalent:

1. x is in the weak closure of C.

2. x is in the norm closure of C.

3. x is the norm limit of a sequence of points in C.

4. x is the weak limit of a sequence of points in C.

Proof. The equivalence of (1) and (2) follows from the well-known fact (Theorem V.3.13 in [11]) that a convex set is weakly closed if and only if it is norm closed. The implications (2)⇒(3)⇒(4)⇒(1) are all trivial.

Corollary 3.22. If X is a reflexive Banach space and C ⊆ X^{∗} is convex, then the weak-∗ sequential closure ordinal of C is 0 if C is weak-∗ closed, and is 1 otherwise.

Proof. If X is reflexive then so is X^{∗} (see Corollary II.3.24 in [11]), and hence the weak and weak-∗ topologies on X^{∗} coincide. The result now follows immediately from Theorem 3.21.

We would like to thank Howard Becker for pointing this out to us.

Corollary 3.23. If C ⊆ ℓ_{2} is convex, then the weak-∗ (i.e., weak) sequential closure ordinal of C is 0 if C is weak-∗ (i.e., weakly) closed, 1 otherwise.

We do not know whether the closure ordinal of a convex set in the dual of a separable Banach space can be a limit ordinal.

4. The weak-∗ topology in subsystems of Z_{2}

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

(φ(0) ∧ ∀n(φ(n) → φ(n + 1))) → ∀nφ(n)

plus the comprehension scheme

∃W ∀n (n ∈ W ↔ φ(n))

where φ(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 φ(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 ∈ W ∧ ∀n (n ∈ W → n + 1 ∈ W)) → ∀n (n ∈ W) .

Two of the most important subsystems of second order arithmetic are ACA_{0} and Π_{1}^{1}- 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 ACA_{0} consist of the basic arithmetical axioms, the restricted induction axiom, and arithmetical comprehension, i.e., the comprehension scheme for formulas φ(n) which are arithmetical. A Π_{1}^{1} formula is one of the form ∀W θ where θ is arithmetical. The axioms of Π_{1}^{1}-CA_{0} consist of the axioms of ACA_{0} plus Π_{1}^{1} comprehension.

Obviously Π_{1}^{1}-CA_{0} is much stronger than ACA_{0}. Three other very important subsystems of second order arithmetic are RCA_{0} and WKL_{0}, both of which are weaker than ACA_{0}, and ATR_{0}, which is intermediate between ACA_{0} and Π_{1}^{1}-CA_{0}. For background material on subsystems of second order arithmetic, we refer the reader to [12, 5, 6, 25].

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 ACA_{0} and weaker systems. In particular, we show that a version of the Krein-Šmulian theorem is provable in 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, 25]; see also the paper of Shioji and Tanaka [22].

Definition 4.1 (RCA_{0}). A (code for a) complete separable metric space Â is defined to be a set A ⊆ ℕ together with a function d : A × A → ℝ such that, for all a, b, c ∈ A,

1. d(a, a) = 0,

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

3. d(a, c) ≤ d(a, b) + d(b, c). A (code for a) point of Â is defined to be a sequence ⟨a_{n} | n ∈ ℕ⟩ of elements of A such that ∀m ∀n (m < n ⟶ d(a_{m}, a_{n}) ≤ 1/2^{m}). Although Â does not formally exist as a set within RCA_{0}, we use notations such as x ∈ Â to mean that x is a point of Â, etc. We then straightforwardly extend our definitions of = and d to Â in such a way that ⟨Â, d⟩ is a complete metric space, with A dense in Â.

Definition 4.2 (RCA_{0}). Let Â be a complete separable metric space as defined above. A (code for an) open set in Â is defined to be a sequence of ordered pairs U = ⟨(a_{i}, q_{i}) | i ∈ ℕ⟩, a_{i} ∈ A, q_{i} ∈ ℚ. We write x ∈ U to mean that x ∈ Â and d(x, a_{i}) < q_{i} for some i ∈ ℕ. A closed set in Â is defined to be the complement of an open set.

Building on the definitions above within 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 ACA_{0} or WKL_{0} or RCA_{0} many fundamental results about the topology of complete separable metric spaces. For details, see [25]. In particular, one can prove within WKL_{0} (see Chapter IV of [25]) the Heine-Borel covering lemma (“if C is compact then any covering of C by a sequence of open sets has a finite subcovering”), using the following RCA_{0} notion of compactness:

Definition 4.3 (RCA_{0}). Let C be a closed set in a complete separable metric space Â. We say that C is compact if there exists a countable sequence of finite sequences of points ⟨⟨x_{ni} | i ≤ k_{n}⟩ | n ∈ ℕ⟩ in Â such that for all x ∈ C and all n ∈ ℕ there exists i ≤ k_{n} such that d(x, x_{ni}) < 1/2^{n}.

In the same setting, there is a useful version of the Tychonoff product theorem, and one can prove within RCA_{0} the compactness of the product space ∏_{n∈ℕ}[a_{n}, b_{n}], where ⟨[a_{n}, b_{n}] | n ∈ ℕ⟩ is any sequence of closed bounded intervals. For details, see Chapter IV of [25].

We now turn to our development of separable Banach space theory within RCA_{0} and ACA_{0}.

Definition 4.4 (RCA_{0}). A (code for a) separable Banach space consists of a countable set A ⊆ ℕ together with operations + : A × A → A, − : A × A → A, and · : ℚ × A → A and a distinguished element 0 ∈ A such that ⟨A, +, −, ·, 0⟩ forms a countable vector space over the rational field ℚ, together with a function ∥ ∥ : A → ℝ satisfying

1. ∥qa∥ = |q|∥a∥ for all a ∈ A and q ∈ ℚ, and

2. ∥a + b∥ ≤ ∥a∥ + ∥b∥ for all a, b ∈ A.

In other words, a code for a separable Banach space Â is a countable pseudo-normed vector space A over ℚ. Note that Â is a complete separable metric space under d(a, b) = ∥a − b∥. Thus a point of the separable Banach space Â is by definition a sequence ⟨a_{n} | n ∈ ℕ⟩ such that ∀m ∀n (m < n ⟶ ∥a_{m} − a_{n}∥ < 1/2^{m}).

Definition 4.5 (RCA_{0}). Let X = Â and Y = B̂ be separable Banach spaces. A (code for a) bounded linear operator F : X → Y is a linear mapping F : A → B̂ such that, for some 0 ≤ r < ∞, ∥F ∥ ≤ r, i.e., ∥F (a)∥ ≤ r∥a∥ for all a ∈ A. If x = ⟨a_{n} | n ∈ ℕ⟩ is a point of X = Â, we write F (x) = lim_{n} F (a_{n}).

It can be proved in RCA_{0} [5, 7, 25] that bounded linear operators F : X → Y are identifiable with continuous linear mappings from X into Y. Also within RCA_{0} one can prove a useful version of the Banach-Steinhaus theorem:

Theorem 4.6. The following is provable in RCA_{0}. Given separable Banach spaces X and Y and a sequence of bounded linear operators F_{n} : X → Y, n ∈ ℕ, if {∥F_{n}(x)∥ | n ∈ ℕ} is bounded for all x ∈ X, then there exists r < ∞ such that ∥F_{n}∥ ≤ r for all n ∈ ℕ.

Proof. See [7, 6, 25].

Definition 4.7 (RCA_{0}). Let X be a separable Banach space. A bounded linear functional on X is a bounded linear operator f : X → ℝ. We write f ∈ X^{∗} to mean that f is a bounded linear functional on X. For 0 ≤ r < ∞, we write f ∈ B_{r}(X^{∗}) to mean that f ∈ X^{∗} and ∥f∥ ≤ r.

Note that X^{∗} and B_{r}(X^{∗}) do not formally exist as sets within 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 ∏_{a∈A}[−r∥a∥, r∥a∥], where X = Â. Thus the compactness of B_{r}(X^{∗}) is provable in RCA_{0}. This version of the Banach-Alaoglu theorem turns out to be very useful for the development of separable Banach space theory within WKL_{0}. See [5, 22] and Chapter IV of [25] 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 WKL_{0}. Let X be a separable Banach space and let Y be a subspace of X. If g : Y → ℝ is a bounded linear functional with ∥g∥ ≤ r, then there exists a bounded linear functional f : X → ℝ such that ∥f∥ ≤ r and f extends g, i.e., f(x) = g(x) for all x ∈ Y.

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

Theorem 4.9. The following extension of the Hahn-Banach Theorem is provable in WKL_{0}. Let X be a separable Banach space. Let p : X → ℝ be a continuous function such that p(rx) = rp(x) and p(x + y) ≤ p(x) + p(y) for all r ≥ 0 and x, y ∈ X. Let Y be a subspace of X and let g : Y → ℝ be a bounded linear functional such that g(x) ≤ p(x) for all x ∈ Y. Then there exists a bounded linear functional f : X → ℝ such that f extends g and f(x) ≤ p(x) for all x ∈ 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 ACA_{0}:

Lemma 4.10. The following is provable in ACA_{0}. Let X be a separable Banach space. Let Z be a countable set in X such that ||x|| ≥ 1 for all x in the convex hull of Z. Then there exists f ∈ B_{1}(X^{∗}) such that f(x) ≥ 1 for all x in the convex hull of Z.

Proof. Put

W = {∑_{i<n} q_{i}z_{i} | n ∈ ℕ , q_{i} ∈ ℚ ∩ [0, 1] , ∑_{i<n} q_{i} = 1 , z_{i} ∈ Z} .

Note that ∥w∥ ≥ 1 for all w ∈ W. Fix x_{0} ∈ W. By arithmetical comprehension, there is a continuous function p : X → ℝ defined by

p(x) = inf{c ∈ ℚ | c > 0 ∧ ∃w ∈ W (∥(x/c) + w − x_{0}∥ ≤ 1)} .

Then p satisfies the following:

1. p(x_{0}) ≥ 1.

2. 0 ≤ p(x) ≤ ∥x∥ for all x ∈ X.

3. p(rx) = rp(x) for all r ≥ 0 and x ∈ X.

4. p(x + y) ≤ p(x) + p(y) for all x, y ∈ X. Some remarks: if property 1 failed, then there would be w ∈ W and a rational c < 1 such that ∥(x_{0}/c) + w − x_{0}∥ ≤ 1, whence ∥(1 − c)x_{0} + cw∥ ≤ c < 1, contrary to (1 − c)x_{0} + 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_{1} and w_{2} in W such that ∥(x/a) + w_{1} − x_{0}∥ ≤ 1 and ∥(y/b) + w_{2} − x_{0}∥ ≤ 1. Then

\frac{x + y}{a + b} + \frac{a}{a + b}w_{1} + \frac{b}{a + b}w_{2} − x_{0} = (\frac{a}{a + b}) (\frac{x}{a} + w_{1} − x_{0}) + (\frac{b}{a + b}) (\frac{y}{b} + w_{2} − x_{0}) ,

so

∥\frac{x + y}{a + b} + \frac{a}{a + b}w_{1} + \frac{b}{a + b}w_{2} − x_{0}∥ ≤ \frac{a}{a + b} + \frac{b}{a + b} = 1

whence p(x + y) ≤ a + b = c.

Let Y be the subspace of X generated by x_{0}, i.e., Y = ℝx_{0}. Define g : Y → ℝ by g(rx_{0}) = rp(x_{0}). Then g is a bounded linear functional on Y. Moreover, if r ≥ 0 then g(rx_{0}) = rp(x_{0}) = p(rx_{0}), and if r < 0 then g(rx_{0}) = rp(x_{0}) ≤ 0 ≤ p(rx_{0}), so g ≤ p on Y. Thus, by our extended Hahn-Banach theorem 4.9 in WKL_{0}, we can extend g to a bounded linear functional f : X → ℝ such that f ≤ p on X.

Let w ∈ W be given, and suppose y is such that ∥y∥ ≤ 1. Then ∥(y − w + x_{0}) + w − x_{0}∥ = ∥y∥ ≤ 1, whence f(y − w + x_{0}) ≤ p(y − w + x_{0}) ≤ 1 by definition of p. But f(y − w + x_{0}) = f(y) − f(w) + f(x_{0}) and f(x_{0}) ≥ 1, so f(y) ≤ f(w). Replacing f by f/∥f∥, we see that f ∈ B_{1}(X^{∗}) and f(x) ≥ 1 for all x in the convex hull of Z. This completes the proof.

We conjecture that this separation principle is actually provable in WKL_{0} and not only in ACA_{0}.

We now begin our treatment of the weak-∗ topology within RCA_{0}. We start by introducing an RCA_{0} version of the bounded-weak-∗ topology:

Definition 4.11 (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} ⊆ B_{n}(X^{∗}), n ∈ ℕ, such that

∀m ∀n (m < n ⟶ C_{m} = B_{m}(X^{∗}) ∩ C_{n}) .

We write x^{∗} ∈ C to mean ∃n (x^{∗} ∈ C_{n}), or equivalently ∀n(n > ∥x^{∗}∥ → x^{∗} ∈ 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 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 ACA_{0}. Let X be a separable Banach space. If ⟨x_{n} | n ∈ ℕ⟩ is a sequence of points in X such that x_{n} → 0, then

{x^{∗} ∈ X^{∗} | ∀n |x^{∗}(x_{n})| < 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 ⟨x_{n} | n ∈ ℕ⟩ in X such that x_{n} → 0 and {x^{∗} ∈ X^{∗} | ∀n |x^{∗}(x_{n})| ≤ 1} ⊆ U.

Proof. Reasoning in ACA_{0}, let ⟨x_{n} | n ∈ ℕ⟩ be a sequence of points in X such that lim_{n} x_{n} = 0. By arithmetical comprehension, there exists a sequence of integers N_{m}, m ∈ ℕ, such that ∥x_{n}∥ < 1/m for all m ∈ ℕ and n ≥ N_{m}. Using the sequence ⟨N_{m} | m ∈ ℕ⟩ as a parameter, we can define a sequence of closed sets C_{m} ⊆ B_{m}(X^{∗}), m ∈ ℕ, by

C_{m} = {x^{∗} ∈ B_{m}(X^{∗}) | ∃n < N_{m}(|x^{∗}(x_{n})| ≥ 1)} .

It is easy to verify that

C_{m} = {x^{∗} ∈ B_{m}(X^{∗}) | ∃n |x^{∗}(x_{n})| ≥ 1}

and hence C_{k} = C_{m} ∩ B_{k}(X^{∗}) for all k < m. Thus by Definition 4.11 we have a boundedweak-∗-closed set C = ⋃_{m∈ℕ} C_{m} and clearly

X^{∗} \ C = {x^{∗} ∈ X^{∗} | ∀n |x^{∗}(x_{n})| < 1} .

This shows that {x^{∗} ∈ X^{∗} | ∀n |x^{∗}(x_{n})| < 1} is bounded-weak-∗-open in X^{∗}.

The proof of the converse will be carried out in WKL_{0}. Let U be a bounded-weak-∗-open set in X^{∗} containing 0. Then C = X^{∗} \ U is a bounded-weak-∗-closed set with 0 ∉ C. For any countable set S ⊆ X let S^{o} be the polar of S, i.e.,

S^{o} = {x^{∗} ∈ X^{∗} | ∀x ∈ S |x^{∗}(x)| ≤ 1} .

To complete the proof, we need to construct a sequence of points ⟨x_{k} | k ∈ ℕ⟩ in X such that lim_{k} x_{k} = 0 and {x_{k} | k ∈ ℕ}^{o} ∩ C = ∅.

Let X = Â where A is a countable dense set in X. Put A_{0} = A and, for each n ≥ 1, A_{n} = {a ∈ A | ∥a∥ < 1/n}. Claim: for any n ∈ ℕ and any countable set S ⊆ X, if S^{o} ∩ B_{n}(X^{∗}) ∩ C = ∅ then there exists a finite set F ⊂ A_{n} such that (S ∪ F)^{o} ∩ B_{n+1}(X^{∗}) ∩ C = ∅. If such an F does not exist, then for all finite sets F ⊂ A_{n} we would have (S ∪ F)^{o} ∩ B_{n+1}(X^{∗}) ∩ C ≠ ∅, so by the Heine-Borel covering property of the compact set B_{n+1}(X^{∗}) it would follow that

(S ∪ A_{n})^{o} ∩ B_{n+1}(X^{∗}) ∩ C ≠ ∅ .

But (S ∪ A_{n})^{o} = S^{o} ∩ A_{n}^{o} = S^{o} ∩ B_{n}(X^{∗}), and hence S^{o} ∩ B_{n}(X^{∗}) ∩ C ≠ ∅, a contradiction. This proves the claim.

Within WKL_{0}, we can apply the claim above repeatedly starting with F_{0} = ∅ to obtain a sequence of finite sets F_{n+1} ⊆ A_{n}, n ∈ ℕ, such that

(F_{0} ∪ … ∪ F_{n})^{o} ∩ B_{n}(X^{∗}) ∩ C = ∅

for all n ∈ ℕ. The construction can be carried out effectively within WKL_{0} because, by Lemma 5.8 of [3], the predicates F ⊂ A_{n} and F^{o} ∩ B_{n}(X^{∗}) ∩ C = ∅ are provably in WKL_{0} equivalent to Σ_{1}^{0} formulas. Thus the existence of a sequence of finite sets ⟨F_{n} | n ∈ ℕ⟩ with the mentioned properties is provable in WKL_{0}.

Letting ⟨x_{k} | k ∈ ℕ⟩ be an enumeration without repetition of ⋃_{n∈ℕ} F_{n}, it is clear that x_{k} → 0 in X and that {x_{k} | k ∈ ℕ}^{o} ∩ C = ∅. This completes the proof.

We now introduce our RCA_{0} version of the weak-∗ topology.

Definition 4.13 (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}^{∗} ∈ U there exists a finite sequence of points x_{0}, …, x_{n−1} ∈ X such that

{x^{∗} ∈ X^{∗} | ∀k < n (|x^{∗}(x_{k}) − x_{0}^{∗}(x_{k})| ≤ 1)} ⊆ 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 RCA_{0} that any weak-∗-closed set is bounded-weak-∗-closed. In ACA_{0} we have following version of the Krein-Šmulian theorem:

Theorem 4.14. The following is provable in ACA_{0}. Let X be a separable Banach space. Suppose that C ⊆ X^{∗} is convex and bounded-weak-∗-closed. Then C is weak-∗-closed.

Proof. Let x_{0}^{∗} ∉ C be given. Then C − x_{0}^{∗} is also bounded-weak-∗-closed and convex, and 0 ∉ C − x_{0}^{∗}. Thus (C − x_{0}^{∗}) ∩ B_{n}(X^{∗}) is a closed subset of B_{n}(X^{∗}) for each n ∈ ℕ. Since B_{n}(X^{∗}) is compact, in ACA_{0} there exists a countable dense subset D_{n} ⊂ (C − x_{0}^{∗}) ∩ 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_{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 {x_{n} | n ∈ ℕ} such that x_{n} → 0 and {x^{∗} ∈ X^{∗} | ∀n|x^{∗}(x_{n})| ≤ 1} ⊆ U.

Now, for each m ∈ ℕ, define a function T_{m} : B_{m}(X^{∗}) → c_{0} by T_{m}(x^{∗}) = ⟨x^{∗}(x_{n}) | n ∈ ℕ⟩. 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^{∗} → c_{0} by T (x^{∗}) = T_{m}(x^{∗}) where x^{∗} ∈ B_{m}(X^{∗}). Notice that T is linear, and ∥T (x^{∗})∥ ≤ 1 implies x^{∗} ∈ U for all x^{∗} ∈ X^{∗}. Let D be an enumeration of the dense sets D_{n} ⊂ (C − x_{0}^{∗}) ∩ B_{n}(X^{∗}), and let E = T (D) (which exists by arithmetical comprehension); then E is a countable subset of c_{0}, and ∥x∥ > 1 for all x in the convex hull of E. By Lemma 4.10 there exists f ∈ B_{1}(c_{0}^{∗}) = B_{1}(ℓ_{1}) such that f(x) ≥ 1 for all x in the convex hull of E. Write f = ⟨α_{n} : n ∈ ℕ⟩ ∈ ℓ_{1}.

Let x = ∑_{n∈ℕ} α_{n}x_{n}; note that {x^{∗} ∈ X^{∗} | |x^{∗}(x)| < 1} is weak-∗-open and contains 0. Also, if y^{∗} ∈ C − x_{0}^{∗} then y^{∗} ∈ B_{m}(X^{∗}) for some m. Thus |y^{∗}(x)| = | ∑_{n∈ℕ} α_{n}y^{∗}(x_{n})| = |f(T (y^{∗}))| = |f(T_{m}(y^{∗}))| ≥ 1 since D_{m} is dense in B_{m}(X^{∗}) and f and T_{m} are continuous. So let N = {x^{∗} ∈ X^{∗} | |x^{∗}(2x)| < 1} = {x^{∗} ∈ X^{∗} | |x^{∗}(x)| < 1/2}; 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:

Corollary 4.15. The following is provable in ACA_{0}. Let X be a separable Banach space. Let C be a closed set in B_{1}(X^{∗}) such that C = B_{1}(X^{∗}) ∩ span(C) where

span(C) = {∑_{i=0}^{n} a_{i} x_{i}^{∗} | a_{i} ∈ ℝ , x_{i}^{∗} ∈ C , n ∈ ℕ} .

Then 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.

5. Proof of the main result

In this section we show that a rather strong set existence axiom, Π_{1}^{1} comprehension, is needed to prove a very elementary (indeed trivial-sounding) fact of separable Banach space theory. Namely, Π_{1}^{1}-CA_{0} is equivalent over ACA_{0} to the following statement:

Given a separable Banach space X and a countable set Y ⊂ X^{∗}, there is a smallest weak-∗-closed subspace C of X^{∗} such that Y ⊆ C.

(S)

This equivalence is the content of our main result, Theorem 5.6 below.

The forward direction is the assertion that (S) is provable in Π_{1}^{1}-CA_{0}. This will be obtained as a special case of:

Lemma 5.1. The following is provable in Π_{1}^{1}-CA_{0}. Let X be a separable Banach space. Given a countable set Y ⊂ X^{∗}, there is a smallest weak-∗-closed set C ⊆ X^{∗} such that Y ⊆ C.

Proof. We reason in Π_{1}^{1}-CA_{0}. For each x_{0}^{∗} ∈ X^{∗} and each finite set F ⊂ X, there is a weak-∗-open set

U(x_{0}^{∗}, F) = {x^{∗} ∈ X^{∗} | ∀x ∈ F (|x^{∗}(x) − x_{0}^{∗}(x)| < 1)} .

By Σ_{1}^{1} comprehension, let U be the weak-∗-open set which is the union of the U(x_{0}^{∗}, F) for all x_{0}^{∗} ∈ X^{∗} and all finite F ⊂ X satisfying the arithmetical condition Y ∩ U(x_{0}^{∗}, F) = ∅. In terms of Definitions 4.2 and 4.13, the code of U_{n} = U ∩ B_{n}(X^{∗}) for each n ∈ ℕ is the union of the codes of U(x_{0}^{∗}, F) ∩ B_{n}(X^{∗}) for all x_{0}^{∗} ∈ X^{∗} and all finite F ⊂ X such that Y ∩ U(x_{0}^{∗}, F) = ∅. Clearly C = X^{∗} \ U is the smallest weak-∗-closed set that includes Y. This completes the proof.

For the reversal, we must show that (S) implies Π_{1}^{1}-CA_{0}. The standard method of proving that a mathematical statement implies Π_{1}^{1}-CA_{0} is to apply the following lemma [12, 25]:

Lemma 5.2. It is provable in RCA_{0} that the following are equivalent:

1. Π_{1}^{1}-CA_{0};

2. For any sequence of trees ⟨T_{n} | n ∈ ℕ⟩, there exists a set W ⊆ ℕ consisting of all n ∈ ℕ such that T_{n} is well-founded.

Proof. The assertion that T_{n} is well-founded is Π_{1}^{1} (using the sequence ⟨T_{n} | n ∈ ℕ⟩ as a parameter). The implication from (1) to (2) is therefore obvious. For the converse, reasoning in RCA_{0}, first we show that (2) implies ACA_{0}. It is well-known (see [25]) that ACA_{0} is equivalent over RCA_{0} to the statement that, for any one-to-one function f: ℕ → ℕ, the range of f exists. Accordingly, let f: ℕ → ℕ be one-to-one. By recursive comprehension (using f as a parameter), we define a sequence ⟨T_{n} | n ∈ ℕ⟩ by s ∈ T_{n} if and only if ∀k < lh(s) (n ≠ f(k)). Note that T_{n} is well-founded if and only if n is in the range of f. By (2), there is a set W such that n ∈ W if and only if T_{n} is well-founded, and so n ∈ W if and only if n is in the range of f, i.e., the range of f exists, as desired. This proves ACA_{0}.

Now, reasoning in ACA_{0}, let φ(n) be a Π_{1}^{1} formula. By the Normal Form Theorem formalized within ACA_{0} (see [25]), we can write φ(n) ≡ ∀f ∃m θ(f[m], n), where θ is Σ_{0}^{0}. Use recursive comprehension to form a sequence of trees

T_{n} = {s | ∀m ≤ lh(s) ¬θ(s[m], n)} ,

n ∈ ℕ. Note that, for all n, φ(n) holds if and only if T_{n} is well-founded. By (2) there exists a set W consisting of all n such that T_{n} is well-founded. Thus for all n ∈ ℕ we have φ(n) if and only if n ∈ W. This proves Π_{1}^{1} comprehension. Thus we have the implication from (2) to (1). This completes the proof.

In showing that the implication from (S) to Π_{1}^{1}-CA_{0} is provable in ACA_{0}, we shall want to know that some of our results from Section 3 are provable in ACA_{0}. Our ACA_{0} version of part of Lemma 3.14 is:

Lemma 5.3. The following is provable in ACA_{0} (actually WKL_{0}). Let T ⊆ Seq be a tree and let

T^{∗} = \{s ∈ Seq | ∃t ∈ T (t \underline{≪} s)\}

be the upward closure of T under majorization. Then T is well-founded if and only if T^{∗} is well-founded.

Proof. We reason in WKL_{0}. If T^{∗} is well-founded then obviously T is well-founded, since T ⊆ T^{∗}. Suppose now that T^{∗} is not well-founded. Let f be a path through T^{∗}. By recursive comprehension form the tree T_{f} = \{t ∈ T | t \underline{≪} f[lh(t)]\}. Since f is a path through T^{∗}, we have that for each n there exists t ∈ T_{f} such that t \underline{≪} f[n], and hence lh(t) = n, 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 WKL_{0} (see [12] and Lemma IV.1.4 of [25]). Since T_{f} ⊆ T, 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.

Lemma 5.4. It is provable in ACA_{0} (actually in WKL_{0}) that the following are pairwise equivalent:

1. Π_{1}^{1}-CA_{0};

2. For any sequence of trees ⟨T_{n} | n ∈ ℕ⟩, there exists a set W ⊆ ℕ consisting of all n ∈ ℕ such that T_{n} is well-founded.

3. For any sequence of smooth trees ⟨T_{n} | n ∈ ℕ⟩, there exists a set W ⊆ ℕ consisting of all n ∈ ℕ such that T_{n} is well-founded.

Proof. The equivalence of (1) and (2) is Lemma 5.2. Given a sequence of trees ⟨T_{n} | n ∈ ℕ⟩, we can use recursive comprehension to form a sequence of smooth trees ⟨T_{n}^{∗} | n ∈ ℕ⟩. By the previous lemma we have in WKL_{0} that for all n, T_{n} is well-founded if and only if T_{n}^{∗} is well-founded. The equivalence of (2) and (3) follows.

Our ACA_{0} version of Corollary 3.12 is:

Lemma 5.5. The following is provable in ACA_{0}. Let S ⊆ Seq be such that, for each s ∈ S, s^{⌢}⟨m⟩ ∈ S for all but finitely many m. Then Z_{S} is a weak-∗-closed subspace of ℓ_{1}(Seq) = c_{0}^{∗}(Seq).

Proof. To simplify notation, let us write X = c_{0}(Seq), so that X^{∗} = ℓ_{1}(Seq). Clearly Z_{S} is a subspace of X^{∗}. In order to show that Z_{S} is weak-∗-closed, we shall first show that Z_{S} ∩ B_{1}(X^{∗}) is weak-∗-closed.

By arithmetical comprehension, there exists a sequence ⟨M_{s} | s ∈ S⟩ where M_{s} is the least M such that s^{⌢}⟨m⟩ ∈ S for all m ≥ M. Using ⟨M_{s} | s ∈ S⟩ as a parameter, let φ(z) be a Σ_{1}^{0} formula asserting for z ∈ X^{∗} the existence of s ∈ S and M ≥ M_{s} such that

|\frac{1}{s′} z(s) − \frac{1}{s} ∑_{m<M} z(s^{⌢}⟨m⟩)| > \frac{1}{s^{⌢}⟨M⟩} . (1)

Since φ(z) is Σ_{1}^{0}, it follows by standard RCA_{0} techniques (see Lemma II.5.7 of [25]) that there exists a relatively weak-∗-open set U ⊆ B_{1}(X^{∗}) consisting of all z ∈ B_{1}(X^{∗}) such that φ(z) holds.

We claim that U = B_{1}(X^{∗}) \ Z_{S}. To see this, let z ∈ B_{1}(X^{∗}) be given. If z ∉ Z_{S}, then for some s ∈ S we have

|\frac{1}{s′} z(s) − \frac{1}{s} ∑_{m=0}^{∞} z(s^{⌢}⟨m⟩)| > 0 ,

whence (1) holds for all sufficiently large M ≥ M_{s}, whence z ∈ U. Conversely, if z ∈ U ∩ Z_{S}, then by (1) we have

\frac{1}{s^{⌢}⟨M⟩} < |\frac{1}{s} ∑_{m≥M} z(s^{⌢}⟨m⟩)|  (since z ∈ Z_{s})

≤ \frac{1}{s} ∑_{m≥M} |z(s^{⌢}⟨m⟩)|

= \frac{1}{s} ∑_{m≥M} |\frac{s}{s^{⌢}⟨m⟩} ∑_{n=0}^{∞} z(s^{⌢}⟨m, n⟩)|  (since z ∈ Z_{s^{⌢}⟨m⟩} for all m ≥ M)

≤ \frac{1}{s^{⌢}⟨M⟩} ∑_{m≥M} ∑_{n=0}^{∞} |z(s^{⌢}⟨m, n⟩)|

≤ \frac{∥z∥}{s^{⌢}⟨M⟩} ,

whence ∥z∥ > 1, i.e., z ∉ B_{1}(X^{∗}), a contradiction. This proves the claim.

The claim implies that Z_{S} ∩ B_{1}(X^{∗}) is weak-∗-closed. By Corollary 4.15, it follows in ACA_{0} that Z_{S} is weak-∗-closed. This completes the proof.

We are now ready to prove our main result:

Theorem 5.6 (RCA_{0}). The following are pairwise equivalent:

1. Π_{1}^{1}-CA_{0}.

2. For every separable Banach space X and countable set Y ⊆ X^{∗}, there exists a smallest weak-∗-closed set in X^{∗} containing Y.

3. For every separable Banach space X and countable set Y ⊆ X^{∗}, there exists a smallest weak-∗-closed convex set in X^{∗} containing Y.

4. For every separable Banach space X and countable set Y ⊆ X^{∗}, there exists a smallest weak-∗-closed subspace of X^{∗} containing Y;

5. For every countable set Y ⊆ ℓ_{1} = c_{0}^{∗}, there exists a smallest weak-∗-closed set in ℓ_{1} containing Y.

6. For every countable set Y ⊆ ℓ_{1} = c_{0}^{∗}, there exists a smallest weak-∗-closed convex set in ℓ_{1} containing Y.

7. For every countable set Y ⊆ ℓ_{1} = c_{0}^{∗}, there exists a smallest weak-∗-closed subspace of ℓ_{1} containing Y.

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

{∑_{i=0}^{n} q_{i} y_{i}^{∗} | ∑_{i=0}^{n} q_{i} = 1, q_{i} ∈ ℚ, q_{i} > 0, y_{i}^{∗} ∈ Y, n ∈ ℕ} .

The implications from (3) to (4) and (6) to (7) are straightforward by considering the countable set

{∑_{i=0}^{n} q_{i} y_{i}^{∗} | q_{i} ∈ ℚ, y_{i}^{∗} ∈ Y, n ∈ ℕ} .

The implications from (2) to (5) and (3) to (6) and (4) to (7) are trivial.

It remains to prove in RCA_{0} that (7) implies Π_{1}^{1}-CA_{0}. First we show in RCA_{0} that (7) implies ACA_{0}. Toward that end, let f: ℕ → ℕ be one-to-one; we want to show that the range of f exists. Using f as a parameter, let Y = {y_{⟨n,m⟩} | ∃k ≤ m (f(k) = n)} ⊂ ℓ_{1}. By (7), let C be the smallest weak-∗-closed subspace of ℓ_{1} containing Y. Claim: for all n ∈ ℕ, y_{⟨n⟩} ∈ C if and only if n is in the range of f. To see this, first suppose n = f(k) for some k. Then y_{⟨n,m⟩} ∈ Y for all m ≥ k, and, since y_{⟨n,m⟩} → y_{⟨n⟩} weak-∗ as m → ∞, we have y_{⟨n⟩} ∈ C. Conversely, suppose n is not in the range of f. Then y_{⟨n,m⟩} ∉ Y for all m ∈ ℕ, and hence, for all y_{⟨k,m⟩} ∈ Y, y_{⟨k,m⟩}(⟨n⟩) = 0. Let C′ be the set of all y ∈ ℓ_{1}(Seq) such that y(⟨n⟩) = 0. Then C′ is a weak-∗-closed subspace of ℓ_{1} which contains Y (and hence contains C), but y_{⟨n⟩} ∉ C′ ⊇ C. This proves the claim. Now, ‘y_{⟨n⟩} ∈ C’ is Π_{1}^{0} (as C is a code for a weak-∗-closed set), whereas ‘n is in the range of f’ is Σ_{1}^{0}, so by recursive comprehension, the range of f exists, as desired. Thus (7) implies ACA_{0}.

So, reasoning within ACA_{0}, assume (7). Instead of proving Π_{1}^{1}-CA_{0} directly, we shall prove the equivalent statement given by Lemma 5.4.

Let ⟨T_{n} | n ∈ ℕ⟩ be a sequence of smooth trees. By recursive comprehension, form the set

T = {⟨n⟩^{⌢}s | n ∈ ℕ, s ∈ T_{n}} .

Using the notation of Definition 3.6, consider the countable set Y = {y_{t} | t ∉ T }. Note that Y ⊆ Z_{T}. By (7) there is a smallest weak-∗-closed subspace C of ℓ_{1}(Seq) such that C ⊇ Y. Since the predicate y ∈ C is arithmetical (in fact Π_{1}^{0}, using a code for C as a parameter), we can use arithmetical comprehension to form the set

W = {n | y_{⟨n⟩} ∈ C} .

We claim that, for all n ∈ ℕ, T_{n} is well-founded if and only if n ∈ W.

To prove the claim, let n be such that T_{n} is well-founded. We shall argue by arithmetical transfinite induction on the well-founded tree T_{n} that y_{⟨n⟩^{⌢}s} ∈ C for all s ∈ Seq. (Note that arithmetical transfinite induction is available in ACA_{0}; see Lemma V.2.1 of [25].) The base step consists of observing that s ∉ T_{n} implies ⟨n⟩^{⌢}s ∉ T which implies y_{⟨n⟩^{⌢}s} ∈ Y ⊆ C. For the inductive step, let s ∈ T_{n} be given such that y_{⟨n⟩^{⌢}s^{⌢}⟨m⟩} ∈ C for all m ∈ ℕ. Clearly y_{⟨n⟩^{⌢}s^{⌢}⟨m⟩} converges weak-∗ to y_{⟨n⟩^{⌢}s} as m → ∞. Since C is weak-∗-closed, it follows that y_{⟨n⟩^{⌢}s} ∈ C. This gives the inductive step. Thus y_{⟨n⟩^{⌢}s} ∈ C for all s ∈ Seq. In particular y_{⟨n⟩} ∈ C, i.e., n ∈ W. This proves half of the claim.

For the other half, let n be such that T_{n} is not well-founded. We shall show that n ∉ W. Let f be a path through T_{n}. By recursive comprehension form the set

S = \{⟨n⟩^{⌢}s | f[lh(s)] \underline{≪} s\} .

Note that ⟨n⟩ ∈ S. Since T_{n} is smooth, we have S ⊆ T, and hence y_{⟨n⟩} ∉ Z_{S} ⊇ Z_{T} ⊇ Y. Moreover, for any ⟨n⟩^{⌢}s ∈ S, we have ⟨n⟩^{⌢}s^{⌢}⟨m⟩ ∈ S for all m ≥ f(lh(s)), whence by Lemma 5.5 Z_{S} is a weak-∗-closed subspace of X^{∗}. It follows that Z_{S} ⊇ C, and hence y_{⟨n⟩} ∉ C, i.e., n ∉ W. This completes the proof of the claim.

From our assumption (7) we have shown that for all sequences of smooth trees ⟨T_{n} | n ∈ ℕ⟩, there exists a set W consisting of all n such that T_{n} is well-founded. Hence by Lemma 5.4 we see that (7) implies Π_{1}^{1} comprehension, i.e., (1). This completes the proof of Theorem 5.6.

Theorem 5.7 (RCA_{0}). The following are pairwise equivalent:

1. Π_{1}^{1}-CA_{0}.

2. For every separable Banach space X such that X^{∗} is also separable, and for every norm closed subspace Z ⊆ X^{∗}, there exists a smallest weak-∗-closed subspace of X^{∗} containing Z.

3. For every separable Banach space X such that X^{∗} is also separable, and for every weakly closed subspace Z ⊆ X^{∗}, there exists a smallest weak-∗-closed subspace of X^{∗} containing Z.

4. For every norm closed subspace Z ⊆ ℓ_{1} = c_{0}^{∗}, there exists a smallest weak-∗-closed subspace of ℓ_{1} containing Z.

5. For every weakly closed subspace Z ⊆ ℓ_{1} = c_{0}^{∗}, there exists a smallest weak-∗-closed subspace of ℓ_{1} containing Z.

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 RCA_{0}.

Proof. Let X be a separable Banach space, with Z ⊆ X^{∗} a norm closed subspace. In Π_{1}^{1}- CA_{0}, since Z is norm closed there is a countable set S ⊂ X^{∗} 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 RCA_{0} that (5)⇒(1). As in the proof of Theorem 5.6, we first show that (5) implies ACA_{0}. So assume (5) and let f: ℕ → ℕ be one-to-one; we want to show in RCA_{0} that the range of f exists. By recursive comprehension (using f as a parameter), define a tree T by

T = {⟨⟩} ∪ {⟨n⟩^{⌢}s | ∀k ≤ lh(s) (f(k) ≠ n)}.

Then Z_{T} is a weakly closed subspace of ℓ_{1} = c_{0}^{∗}. By (5), let C be the smallest weak-∗ closed subspace of ℓ_{1} containing Z_{T}. We claim that for all n ∈ ℕ, n is in the range of f if and only if y_{⟨n⟩} ∈ C. To see this, first suppose n is in the range of f, say f(m) = n. We’ll show by Π_{1}^{0}-induction (which is available in RCA_{0}; see Corollary 3.10 in [25]) that for all s ∈ Seq, y_{⟨n⟩^{⌢}s} ∈ C. Let φ(i) be the Π_{1}^{0} formula ∀s ∈ Seq (lh(s) = m − i → y_{⟨n⟩^{⌢}s} ∈ C). By the definition of T, if lh(s) ≥ m then ⟨n⟩ ∉ T, whence y_{⟨n⟩^{⌢}s} ∈ Z_{T} ⊆ C, and so φ(0) holds. Now suppose lh(s) = m − i, and y_{⟨n⟩^{⌢}t} ∈ C for all t ∈ Seq with lh(t) = m − i + 1. Then y_{⟨n⟩^{⌢}s^{⌢}⟨k⟩} ∈ C for all k ∈ ℕ, and y_{⟨n⟩^{⌢}s^{⌢}⟨k⟩} → y_{⟨n⟩^{⌢}s} weak-∗ as k → ∞, so y_{⟨n⟩^{⌢}s} ∈ C since C is weak-∗ closed. Thus φ(i − 1) implies φ(i), so it follows by Π_{1}^{0}-induction that φ(i) holds for all i ∈ ℕ. In particular, φ(m) holds, i.e., y_{⟨n⟩} ∈ C. This proves one half of the claim.

Conversely, suppose n is not in the range of f; we want to show that y_{⟨n⟩} ∉ C. Let S = {⟨n⟩^{⌢}s | s ∈ Seq}. Then S ⊆ T, whence Z_{S} ⊇ Z_{T}. It suffices therefore to show that Z_{S} is weak-∗ closed, because then Z_{S} ⊇ C, and y_{⟨n⟩} ∉ Z_{S} since ⟨n⟩ ∈ S. In fact, we’ll show that Z_{S} = {z ∈ ℓ_{1}(Seq) | ∀t ∈ S (z(t) = 0)}, which is clearly weak-∗ closed. Obviously, if z(t) = 0 for all t ∈ S, it follows from the definition of Z_{S} that z ∈ Z_{S}. On the other hand, suppose z ∈ Z_{S} and let t ∈ S be given. Since z ∈ Z_{S} ⊂ Z_{t^{⌢}s} for all s ∈ Seq, it follows that (1/t′)z(t) = (1/t) ∑_{m_{1}∈ℕ} z(t^{⌢}⟨m_{1}⟩), which in turn equals ∑_{m_{1}∈ℕ}(1/(t^{⌢}⟨m_{1}⟩)) ∑_{m_{2}∈ℕ} z(t^{⌢}⟨m_{1}, m_{2}⟩), which equals

∑_{m_{1},m_{2}∈ℕ} \frac{1}{t^{⌢}⟨m_{1}, m_{2}⟩} ∑_{m_{3}∈ℕ}z(t^{⌢}⟨m_{1}, m_{2}, m_{3}⟩),

and so on. Thus for all k ∈ ℕ we have

\frac{1}{t′} z(t) = ∑_{s∈ℕ^{k}} \frac{1}{t^{⌢}s} ∑_{m∈ℕ}z(t^{⌢}s^{⌢}⟨m⟩).

From this it follows easily that

\frac{1}{t′} |z(t)| ≤ \frac{1}{t^{⌢}⟨0⟩^{k}} ∥z∥_{1} for all k ∈ ℕ,

where ⟨0⟩^{k} is the sequence of length k, all of whose terms are 0. The right hand side of this inequality approaches 0 as k → ∞. Thus z(t) = 0. We have shown that z ∈ Z_{S} if and only if z(t) = 0 for all t ∈ S. This completes the proof of the claim. Since ‘n is in the range of f’ is Σ_{1}^{0} and ‘y_{⟨n⟩} ∈ C’ is Π_{1}^{0}, it follows by recursive comprehension that the range of f exists. Thus (5) implies ACA_{0}.

To prove that (5) implies Π_{1}^{1}-CA_{0}, we observe that the subspace Z_{T} ⊆ ℓ_{1} in the proof of Theorem 5.6 is weakly closed, so we need only repeat the ACA_{0} part of that argument. This completes the proof of Theorem 5.7.

References

1. S. Banach, Theory of linear operators, North Holland, 1987, English translation of [2] by F. Jellett.

2. Stefan Banach, Théorie des opérations linéaires, Subwencji Funduszu Kultury Narodowej, 1932.

3. Andreas R. Blass, Jeffry L. Hirst, and Stephen G. Simpson, Logical analysis of some theorems of combinatorics and topological dynamics, In Simpson [24], pp. 125–156.

4. Douglas K. Brown, Notions of closed subsets of a complete separable metric space in weak subsystems of second order arithmetic, In Sieg [23], pp. 39–50.

5. Douglas K. Brown and Stephen G. Simpson, Which set existence axioms are needed to prove the separable Hahn-Banach theorem?, Annals of Pure and Applied Logic 31 (1986), 123–144.

6. , The Baire category theorem in weak subsytems of second order arithmetic, Journal of Symbolic Logic 58 (1993), 557–578.

7. Douglas Kenyon Brown, Functional analysis in weak subsystems of second order arithmetic, Ph.D. thesis, The Pennsylvania State University, 1987.

8. Georg Cantor, Contributions to the founding of the theory of transfinite numbers, Dover Publications, Inc., 1955, translated and provided with an introduction and notes by Philip E. B. Jourdain.

9. Joseph W. Dauben, The trigonometric background to Georg Cantor’s theory of sets, Archive for History of Exact Sciences (1971), no. 7, 181–216.

10. Joseph Warren Dauben, Georg Cantor: His mathematics and philosophy of the infinite, Harvard University Press, 1979.

11. Nelson Dunford and Jacob T. Schwartz, Linear operators, Interscience Publishers, Inc., 1958.

12. Harvey Friedman, Stephen G. Simpson, and Rick Smith, Countable algebra and set existence axioms, Annals of Pure and Applied Logic 25 (1983), 141–181.

13. A. S. Kechris and A. Louveau, Descriptive set theory and harmonic analysis, Journal of Symbolic Logic 57 (1992), no. 2, 413–441.

14. Alexander S. Kechris and Alain Louveau, Descriptive set theory and the structure of sets of uniqueness, Cambridge University Press, 1987.

15. Alberto Marcone, Foundations of bqo theory and subsystems of second order arithmetic, Ph.D. thesis, The Pennsylvania State University, 1993.

16. , Foundations of BQO theory, Transactions of the American Mathematical Society (1994), no. 345, 641–660.

17. S. Mazurkiewicz, Sur la dérivée faible d’un ensemble de fonctionelles linéaires, Studia Mathematica 2 (1930), 68–71.

18. O. Carruth McGehee, A proof of a statement of Banach on the weak-∗ topology, Michigan Mathematical Journal 15 (1968), 135–140.

19. Donald Sarason, Weak-star generators of H^{∞}, Pacific Journal of Mathematics 17 (1966), 519–528.

20. , On the order of a simply connected domain, Michigan Mathematical Journal 15 (1968), 129–133.

21. , A remark on the weak-star topology of ℓ^{∞}, Studia Mathematica 30 (1968), 355–359.

22. Naoki Shioji and Kazuyuki Tanaka, Fixed point theory in weak second-order arithmetic, Annals of Pure and Applied Logic 47 (1990), 167–188.

23. Wilfried Sieg (ed.), Logic and computation, Contemporary Mathematics, no. 106, American Mathematical Society, 1990.

24. Stephen G. Simpson (ed.), Logic and combinatorics, Contemporary Mathematics, no. 65, American Mathematical Society, 1987.

25. , Subsystems of second order arithmetic, Perspectives in Mathematical Logic, Springer–Verlag, 1996, in preparation.

26. J. von Neumann, Zur Algebra der Funktionaloperationen und Theorie der normalen Operatoren, Mathematische Annalen 102 (1929), 370–427.

STRONG SET EXISTENCE AXIOMS 27

The Pennsylvania State University, University Park, PA 16802

E-mail address: jimbo@math.psu.edu, simpson@math.psu.edu