Proof of the main result

In this section we show that a rather strong set existence axiom, $\Pi^1_1$ comprehension, is needed to prove a very elementary (indeed trivial-sounding) fact of separable Banach space theory. Namely, $\Pi^1_1$- $\mathsf{CA}_0$ is equivalent over $\mathsf{ACA}_0$ to the following statement (S):

$$\vcenter{\hsize=4.5truein \baselineskip=14.4truept \noindent ... ... subspace $C$\space of $X^*$\space such that $Y\subseteq C$ .}$$

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

The forward direction is the assertion that (S) is provable in $\Pi^1_1$- $\mathsf{CA}_0$. This will be obtained as a special case of:

Lemma 5.1   The following is provable in $\Pi^1_1$- $\mathsf{CA}_0$. Let X be a separable Banach space. Given a countable set $Y\subset X^*$, there is a smallest weak-*-closed set $C\subseteq X^*$ such that $Y\subseteq C$.  

Proof. We reason in $\Pi^1_1$- $\mathsf{CA}_0$. For each $x_0^*\in X^*$ and each finite set $F\subset X$, there is a weak-*-open set

$$U(x_0^*,F)=\{x^*\in X^*\mid\forall x\in F\,(\vert x^*(x)-x_0^*(x)\vert<1)\}\,.$$

By $\Sigma^1_1$comprehension, let U be the weak-*-open set which is the union of the U(x₀^*,F) for all $x_0^*\in X^*$ and all finite $F\subset X$satisfying the arithmetical condition $Y\cap U(x_0^*,F)=\emptyset$. In terms of Definitions 4.2 and 4.13, the code of $U_n=U\cap B_n(X^*)$ for each $n\in{\mathbb{N} }$ is the union of the codes of $U(x_0^*,F)\cap B_n(X^*)$ for all $x_0^*\in X^*$ and all finite $F\subset X$ such that $Y\cap U(x_0^*,F)=\emptyset$. Clearly $C=X^*\setminus U$ is the smallest weak-*-closed set that includes Y. This completes the proof.

For the reversal, we must show that (S) implies $\Pi^1_1$- $\mathsf{CA}_0$. The standard method of proving that a mathematical statement implies $\Pi^1_1$- $\mathsf{CA}_0$ is to apply the following lemma [12,23]:

Lemma 5.2   It is provable in $\mathsf{RCA}_0$ that the following are equivalent:

1.

 $\Pi^1_1$- $\mathsf{CA}_0$;

2.

 For any sequence of trees $\langle{}T_n\mid n\in{\mathbb{N} }\rangle{}$, there exists a set $W\subseteq{\mathbb{N} }$ consisting of all $n\in{\mathbb{N} }$ such that T_n is well-founded.

 

Proof. The assertion that T_n is well-founded is $\Pi^1_1$ (using the sequence $\langle{}T_n\mid n\in{\mathbb{N} }\rangle{}$ as a parameter). The implication from (1) to (2) is therefore obvious. For the converse, reasoning in $\mathsf{RCA}_0$, first we show that (2) implies $\mathsf{ACA}_0$. It is well-known (see [23]) that $\mathsf{ACA}_0$ is equivalent over $\mathsf{RCA}_0$ to the statement that, for any one-to-one function $f\colon{\mathbb{N} }\to{\mathbb{N} }$, the range of f exists. Accordingly, let $f\colon{\mathbb{N} }\to{\mathbb{N} }$ be one-to-one. By recursive comprehension (using f as a parameter), we define a sequence  $\langle{}T_n\mid n\in{\mathbb{N} }\rangle{}$ by $s\in T_n$ if and only if $\forall k<\mbox{\rm lh}(s)\,(n\ne 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 Wsuch that $n\in W$ if and only if T_n is well-founded, and so $n\in W$ if and only if n is in the range of f, i.e., the range of f exists, as desired. This proves $\mathsf{ACA}_0$.

Now, reasoning in $\mathsf{ACA}_0$, let $\varphi(n)$ be a $\Pi^1_1$ formula. By the Normal Form Theorem formalized within $\mathsf{ACA}_0$ (see [23]), we can write $\varphi(n)\equiv\forall f\,\exists m\,\theta(f[m],n)$, where $\theta$ is $\Sigma_0^0$. Use recursive comprehension to form a sequence of trees

$$T_n=\{s\mid\forall m\le\mbox{\rm lh}(s)\,\,\neg\theta(s[m],n)\}\,,$$

$n\in{\mathbb{N} }$. Note that, for all n, $\varphi(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\in{\mathbb{N} }$ we have $\varphi(n)$ if and only if $n\in W$. This proves $\Pi^1_1$comprehension. Thus we have the implication from (2) to (1). This completes the proof.

In showing that the implication from (S) to $\Pi^1_1$- $\mathsf{CA}_0$ is provable in $\mathsf{ACA}_0$, we shall want to know that some of our results from Section 3 are provable in $\mathsf{ACA}_0$. Our $\mathsf{ACA}_0$ version of part of Lemma 3.14 is:

Lemma 5.3   The following is provable in $\mathsf{ACA}_0$ (actually $\mathsf{WKL}_0$). Let $T\subseteq\mbox{\rm Seq}$ be a tree and let

$$T^*=\{s\in\mbox{\rm Seq}\mid\exists t\in T\,(t\,\underline\ll\,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 $\mathsf{WKL}_0$. If T^* is well-founded then obviously T is well-founded, since $T\subseteq 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\in T\mid t\,\underline\ll\,f[\mbox{\rm lh}(t)]\}$. Since f is a path through T^*, we have that for each n there exists $t\in T_f$ such that $t\,\underline\ll\,f[n]$, and hence $\mbox{\rm lh}(t)=n$, so T_fis 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 $\mathsf{WKL}_0$ (see [12] and Lemma IV.1.4 of [23]). Since $T_f\subseteq 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 $\mathsf{ACA}_0$ (actually in $\mathsf{WKL}_0$) that the following are pairwise equivalent:

1.

 $\Pi^1_1$- $\mathsf{CA}_0$;

2.

 For any sequence of trees $\langle{}T_n\mid n\in{\mathbb{N} }\rangle{}$, there exists a set $W\subseteq{\mathbb{N} }$ consisting of all $n\in{\mathbb{N} }$ such that T_n is well-founded.

3.

 For any sequence of smooth trees $\langle{}T_n\mid n\in{\mathbb{N} }\rangle{}$, there exists a set $W\subseteq{\mathbb{N} }$ consisting of all $n\in{\mathbb{N} }$ such that T_n is well-founded.

 

Proof. The equivalence of (1) and (2) is Lemma 5.2. Given a sequence of trees $\langle{}T_n\mid n\in{\mathbb{N} }\rangle{}$, we can use recursive comprehension to form a sequence of smooth trees $\langle{}T_n^*\mid n\in{\mathbb{N} }\rangle{}$. By the previous lemma we have in $\mathsf{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 $\mathsf{ACA}_0$ version of Corollary 3.12 is:

Lemma 5.5   The following is provable in $\mathsf{ACA}_0$. Let $S\subseteq\mbox{\rm Seq}$ be such that, for each $s\in S$, $s^\smallfrown{}\langle m\rangle\in S$ for all but finitely many m. Then Z_S is a weak-*-closed subspace of $\ell_1(\mbox{\rm Seq})=c_0^*(\mbox{\rm Seq})$.

Proof. To simplify notation, let us write $X=c_0(\mbox{\rm Seq})$, so that $X^*=\ell_1(\mbox{\rm 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\cap B_1(X^*)$ is weak-*-closed.

By arithmetical comprehension, there exists a sequence $\langle{}M_s\mid s\in S\rangle{}$ where M_s is the least M such that $s^\smallfrown{}\langle m\rangle\in S$ for all $m\ge M$. Using $\langle{}M_s\mid s\in S\rangle{}$ as a parameter, let $\varphi(z)$ be a $\Sigma^0_1$ formula asserting for $z\in X^*$the existence of $s\in S$ and $M\ge M_s$ such that

$$\left\vert{\frac1{s'}}z(s)-{\frac1{s}}\sum_{m<M}z(s^\smallfro... ...{})\right\vert>{\frac1{s^\smallfrown{}\langle{}M\rangle{}}}\,.$$ (1)

Since $\varphi(z)$ is $\Sigma^0_1$, it follows by standard $\mathsf{RCA}_0$ techniques (see Lemma II.5.7 of [23]) that there exists a relatively weak-*-open set $U\subseteq B_1(X^*)$ consisting of all $z\in B_1(X^*)$ such that $\varphi(z)$ holds.

We claim that $U=B_1(X^*)\setminus Z_S$. To see this, let $z\in B_1(X^*)$ be given. If $z\notin Z_S$, then for some $s\in S$ we have

$$\left\vert{\frac1{s'}}z(s)-{\frac1{s}}\sum_{m=0}^\infty z(s^\smallfrown{}\langle{} m\rangle{})\right\vert>0\,,$$

whence (1) holds for all sufficiently large $M\ge M_s$, whence $z\in U$. Conversely, if $z\in U\cap Z_S$, then by (1) we have

$$\begin{eqnarray*}{\frac1{s^\smallfrown{}\langle{}M\rangle{}}} &<& \left\vert{\fr... ...le& {\frac{\Vert z\Vert}{s^\smallfrown{}\langle{}M\rangle{}}}\,, \end{eqnarray*}$$

whence $\Vert z\Vert>1$, i.e., $z\notin B_1(X^*)$, a contradiction. This proves the claim.

The claim implies that $Z_S\cap B_1(X^*)$ is weak-*-closed. By Corollary 4.15, it follows in $\mathsf{ACA}_0$ that Z_S is weak-*-closed. This completes the proof.

We are now ready to prove our main result:

Theorem 5.6 (tex2html_wrap_inline$RCA_0$)   The following are pairwise equivalent:

1.

  $\Pi^1_1$- $\mathsf{CA}_0$.

2.

  For every separable Banach space X and countable set $Y\subseteq X^*$, there exists a smallest weak-*-closed set in X^* containing Y.

3.

  For every separable Banach space X and countable set $Y\subseteq X^*$, there exists a smallest weak-*-closed convex set in X^* containing Y.

4.

  For every separable Banach space X and countable set $Y\subseteq X^*$, there exists a smallest weak-*-closed subspace of X^* containing Y;

5.

  For every countable set $Y\subseteq\ell_1=c_0^*$, there exists a smallest weak-*-closed set in $\ell _1$ containing Y.

6.

  For every countable set $Y\subseteq\ell_1=c_0^*$, there exists a smallest weak-*-closed convex set in $\ell _1$ containing Y.

7.

  For every countable set $Y\subseteq\ell_1=c_0^*$, there exists a smallest weak-*-closed subspace of $\ell _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

$$\left\{\sum_{i=0}^n q_i\,y^*_i\Bigm\vert \sum_{i=0}^nq_i=1,\ ... ...mathbb{Q} },\ q_i>0,\ y^*_i\in Y,\ n\in{\mathbb{N} }\right\}\,.$$

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

$$\left\{\sum_{i=0}^n q_i\,y^*_i\Bigm\vert q_i\in{\mathbb{Q} },\ y^*_i\in Y,\ n\in{\mathbb{N} }\right\}\,.$$

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

It remains to prove in $\mathsf{RCA}_0$ that (7) implies $\Pi^1_1$- $\mathsf{CA}_0$. First we show in $\mathsf{RCA}_0$ that (7) implies $\mathsf{ACA}_0$. Toward that end, let $f\colon{\mathbb{N} }\to{\mathbb{N} }$ be one-to-one; we want to show that the range of f exists. Using f as a parameter, let $Y=\{y_{\langle{}n,m\rangle{}}\mid\exists k\le m\,(f(k)=n)\}\subset\ell_1$. By (7), let C be the smallest weak-*-closed subspace of $\ell _1$ containing Y. Claim: for all $n\in{\mathbb{N} }$, $y_{\langle{}n\rangle{}}\in 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_{\langle{}n,m\rangle{}}\in Y$ for all $m\ge k$, and, since $y_{\langle{} n,m\rangle{}}\to y_{\langle{}n\rangle{}}$ weak-* as $m\to\infty$, we have $y_{\langle{}n\rangle{}}\in C$. Conversely, suppose n is not in the range of f. Then $y_{\langle{}n,m\rangle{}}\notin Y$ for all $m\in{\mathbb{N} }$, and hence, for all $y_{\langle{} k,m\rangle{}}\in Y$, $y_{\langle{}k,m\rangle{}}(\langle{}n\rangle{})=0$. Let C' be the set of all $y\in\ell_1(\mbox{\rm Seq})$ such that $y(\langle{}n\rangle{})=0$. Then C' is a weak-*-closed subspace of $\ell _1$ which contains Y (and hence contains C), but $y_{\langle{}n\rangle{}}\notin C'\supseteq C$. This proves the claim. Now, ` $y_{\langle{}n\rangle{}}\in C$' is $\Pi^0_1$ (as C is a code for a weak-*-closed set), whereas `n is in the range of f' is  $\Sigma^0_1$, so by recursive comprehension, the range of f exists, as desired. Thus (7) implies  $\mathsf{ACA}_0$.

So, reasoning within $\mathsf{ACA}_0$, assume (7). Instead of proving $\Pi^1_1$- $\mathsf{CA}_0$ directly, we shall prove the equivalent statement given by Lemma 5.4.

Let $\langle{}T_n\mid n\in{\mathbb{N} }\rangle{}$ be a sequence of smooth trees. By recursive comprehension, form the set

$$T=\{\langle{}n\rangle{}^\smallfrown{}s\mid n\in{\mathbb{N} },\ s\in T_n\}\,.$$

Using the notation of Definition 3.6, consider the countable set $Y=\{y_t\mid t\notin T\}$. Note that $Y\subseteq Z_T$. By (7) there is a smallest weak-*-closed subspace C of $\ell_1(\mbox{\rm Seq})$ such that $C\supseteq Y$. Since the predicate $y\in C$ is arithmetical (in fact $\Pi^0_1$, using a code for C as a parameter), we can use arithmetical comprehension to form the set

$$W=\{n\mid y_{\langle{}n\rangle{}}\in C\}\,.$$

We claim that, for all $n\in{\mathbb{N} }$, T_n is well-founded if and only if $n\in 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_{\langle{}n\rangle{}^\smallfrown{}s}\in C$ for all $s\in\mbox{\rm Seq}$. (Note that arithmetical transfinite induction is available in $\mathsf{ACA}_0$; see Lemma V.2.1 of [23].) The base step consists of observing that $s\notin T_n$ implies $\langle{}n\rangle{}^\smallfrown{}s\notin T$ which implies $y_{\langle{}n\rangle{}^\smallfrown{}s}\in Y\subseteq C$. For the inductive step, let $s\in T_n$ be given such that $y_{\langle{}n\rangle{}^\smallfrown{}s^\smallfrown{}\langle{}m\rangle{}}\in C$ for all $m\in{\mathbb{N} }$. Clearly $y_{\langle{}n\rangle{}^\smallfrown{}s^\smallfrown{}\langle{}m\rangle{}}$converges weak-* to $y_{\langle{}n\rangle{}^\smallfrown{}s}$ as $m\to\infty$. Since C is weak-*-closed, it follows that $y_{\langle{}n\rangle{}^\smallfrown{}s}\in C$. This gives the inductive step. Thus $y_{\langle{}n\rangle{}^\smallfrown{}s}\in C$ for all $s\in\mbox{\rm Seq}$. In particular $y_{\langle{}n\rangle{}}\in C$, i.e., $n\in 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\notin W$. Let f be a path through T_n. By recursive comprehension form the set

$$S=\{\langle{}n\rangle{}^\smallfrown{}s\mid f[\mbox{\rm lh}(s)]\,\underline\ll\,s\}\,.$$

Note that $\langle{}n\rangle{}\in S$. Since T_n is smooth, we have $S\subseteq T$, and hence $y_{\langle{}n\rangle{}}\notin Z_S\supseteq Z_T\supseteq Y$. Moreover, for any $\langle{}n\rangle{}^\smallfrown{}s\in S$, we have $\langle{}n\rangle{}^\smallfrown{}s^\smallfrown{}\langle{}m\rangle{}\in S$ for all $m\ge f(\mbox{\rm lh}(s))$, whence by Lemma 5.5 Z_S is a weak-*-closed subspace of X^*. It follows that $Z_S\supseteq C$, and hence $y_{\langle{}n\rangle{}}\notin C$, i.e., $n\notin W$. This completes the proof of the claim.

From our assumption (7) we have shown that for all sequences of smooth trees $\langle{}T_n\mid n\in{\mathbb{N} }\rangle{}$, 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 $\Pi^1_1$comprehension, i.e., (1). This completes the proof of Theorem 5.6.

Theorem 5.7 (tex2html_wrap_inline$RCA_0$)   The following are pairwise equivalent:

1.

  $\Pi^1_1$- $\mathsf{CA}_0$.

2.

  For every separable Banach space X such that X^* is also separable, and for every norm closed subspace $Z\subseteq 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\subseteq X^*$, there exists a smallest weak-*-closed subspace of X^* containing Z.

4.

  For every norm closed subspace $Z\subseteq\ell_1=c_0^*$, there exists a smallest weak-*-closed subspace of $\ell _1$ containing Z.

5.

  For every weakly closed subspace $Z\subseteq\ell_1=c_0^*$, there exists a smallest weak-*-closed subspace of $\ell _1$ containing Z.

Of course, in light of Theorem 3.21, with enough comprehension the equivalences (2) $\Leftrightarrow$(3) and (4) $\Leftrightarrow$(5) are trivial; however, we do not know the status of Theorem 3.21 in $\mathsf{RCA}_0$.

Proof. Let X be a separable Banach space, with $Z\subseteq X^*$ a norm closed subspace. In $\Pi^1_1$- $\mathsf{CA}_0$, since Z is norm closed there is a countable set $S\subset 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) $\Rightarrow$(4) and (3) $\Rightarrow$(5) are trivial, and the implications (2) $\Rightarrow$(3) and (4) $\Rightarrow$(5) follow from the norm topology being stronger than the weak topology.

It remains only to prove in $\mathsf{RCA}_0$ that (5) $\Rightarrow$(1). As in the proof of Theorem 5.6, we first show that (5) implies $\mathsf{ACA}_0$. So assume (5) and let $f\colon{\mathbb{N} }\to{\mathbb{N} }$be one-to-one; we want to show in $\mathsf{RCA}_0$ that the range of fexists. By recursive comprehension (using f as a parameter), define a tree T by

$$T=\{\langle{}\rangle{}\}\cup\{\langle{}n\rangle{}^\smallfrown{}s\mid \forall k\le\mbox{\rm lh}(s)\,(f(k)\ne n)\}.$$

Then Z_T is a weakly closed subspace of $\ell_1=c_0^*$. By (5), let C be the smallest weak-* closed subspace of $\ell _1$ containing Z_T. We claim that for all $n\in{\mathbb{N} }$, n is in the range of f if and only if $y_{\langle{}n\rangle{}}\in C$. To see this, first suppose n is in the range of f, say f(m)=n. We'll show by $\Pi^0_1$-induction (which is available in $\mathsf{RCA}_0$; see Corollary 3.10 in [23]) that for all $s\in\mbox{\rm Seq}$, $y_{\langle{}n\rangle{}^\smallfrown{}s}\in C$. Let $\varphi(i)$ be the $\Pi^0_1$ formula $\forall s\in\mbox{\rm Seq}\;(\mbox{\rm lh}(s)=m-i\to y_{\langle{}n\rangle{}^\smallfrown{}s}\in C)$. By the definition of T, if $\mbox{\rm lh}(s)\ge m$ then $\langle{}n\rangle{}\notin T$, whence $y_{\langle{}n\rangle{}^\smallfrown{}s}\in Z_T\subseteq C$, and so $\varphi(0)$holds. Now suppose $\mbox{\rm lh}(s)=m-i$, and $y_{\langle{}n\rangle{}^\smallfrown{}t}\in C$ for all $t\in\mbox{\rm Seq}$ with $\mbox{\rm lh}(t)=m-i+1$. Then $y_{\langle{}n\rangle{}^\smallfrown{} s^\smallfrown{}\langle{}k\rangle{}}\in C$ for all $k\in{\mathbb{N} }$, and $y_{\langle{}n\rangle{}^\smallfrown{} s^\smallfrown{}\langle{}k\rangle{}}\to y_{\langle{}n\rangle{}^\smallfrown{}s}$ weak-* as $k\to\infty$, so $y_{\langle{}n\rangle{}^\smallfrown{}s}\in C$ since C is weak-* closed. Thus $\varphi(i-1)$ implies $\varphi(i)$, so it follows by $\Pi^0_1$-induction that $\varphi(i)$ holds for all $i\in{\mathbb{N} }$. In particular, $\varphi(m)$holds, i.e., $y_{\langle{}n\rangle{}}\in C$. This proves one half of the claim.

Conversely, suppose n is not in the range of f; we want to show that $y_{\langle{}n\rangle{}}\notin C$. Let $S=\{\langle{} n\rangle{}^\smallfrown{}s\mid s\in\mbox{\rm Seq}\}$. Then $S\subseteq T$, whence $Z_S\supseteq Z_T$. It suffices therefore to show that Z_S is weak-* closed, because then $Z_S\supseteq C$, and $y_{\langle{} n\rangle{}}\notin Z_S$ since $\langle{}n\rangle{}\in S$. In fact, we'll show that $Z_S=\{z\in\ell_1(\mbox{\rm Seq})\mid\forall t\in S\,(z(t)=0)\}$, which is clearly weak-* closed. Obviously, if z(t)=0 for all $t\in S$, it follows from the definition of Z_S that $z\in Z_S$. On the other hand, suppose $z\in Z_S$ and let $t\in S$ be given. Since $z\in Z_S\subset Z_{t^\smallfrown{}s}$ for all $s\in\mbox{\rm Seq}$, it follows that $(1/{t'})z(t) =(1/t)\sum_{m_1\in{\mathbb{N} }}z(t^\smallfrown{}\langle{}m_1\rangle{})$, which in turn equals $\sum_{m_1\in{\mathbb{N} }}(1/(t^\smallfrown{}\langle{} m_1\rangle{}))\sum_{m_2\in{\mathbb{N} }}z(t^\smallfrown{}\langle{}m_1,m_2\rangle{})$, which equals

$$\sum_{m_1,m_2\in{\mathbb{N} }}\frac1{t^\smallfrown{}\langle{}... ...n{\mathbb{N} }}z(t^\smallfrown{}\langle{}m_1,m_2,m_3\rangle{}),$$

and so on. Thus for all $k\in{\mathbb{N} }$ we have

$$\frac1{t'}z(t)= \sum_{s\in{\mathbb{N} }^k}\frac1{t^\smallfrow... ...thbb{N} }}z(t^\smallfrown{}s^\smallfrown{}\langle{}m\rangle{}).$$

From this it follows easily that

$$\frac1{t'}\vert z(t)\vert\le\frac1{t^\smallfrown{}\langle{}0\rangle{}^k}\Vert z\Vert _1 \quad\mbox{for all }k\in{\mathbb{N} },$$

where $\langle{}0\rangle{}^k$ is the sequence of length k, all of whose terms are 0. The right hand side of this inequality approaches 0 as $k\to\infty$. Thus z(t)=0. We have shown that $z\in Z_S$ if and only if z(t)=0 for all $t\in S$. This completes the proof of the claim. Since `n is in the range of f' is $\Sigma^0_1$ and ` $y_{\langle{}n\rangle{}}\in C$' is $\Pi^0_1$, it follows by recursive comprehension that the range of f exists. Thus (5) implies $\mathsf{ACA}_0$.

To prove that (5) implies $\Pi^1_1$- $\mathsf{CA}_0$, we observe that the subspace $Z_T\subseteq\ell_1$ in the proof of Theorem 5.6 is weakly closed, so we need only repeat the $\mathsf{ACA}_0$ part of that argument. This completes the proof of Theorem 5.7.