Preliminaries

The prerequisite for a thorough understanding of this paper is familiarity with the basics of separable Banach space theory as developed in $\mathsf{RCA}_0$. This material has been presented in several places: [3, §§2-5], [4, §1], [12, §4], [20, § II.10]. We briefly review some of the concepts that we shall need.

Within $\mathsf{RCA}_0$, a (code for a) complete separable metric space $X=\widehat{A}$ is defined to be a countable set $A\subseteq{\mathbf{N}}$together with a function $d:A\times A\to{\mathbf{R}}$ satisfying d(a,a)=0, d(a,b)=d(b,a), and $d(a,b)+d(b,c)\ge d(a,c)$. A (code for a) point of X is defined to be a sequence $x=\left\langle a_n\right\rangle_{n\in{\mathbf{N}}}$ of elements of A such that $\forall m\forall n(m<n\to d(a_m,a_n)\le1/2^m)$. We extend d from A to X in the obvious way. For $x,y\in X$ we define x=y to mean that d(x,y)=0.

Within $\mathsf{RCA}_0$, (a code for) an open set in X is defined to be a sequence of ordered pairs $U=\left\langle(a_m,r_m)\right\rangle_{m\in{\mathbf{N}}}$ where $a_m\in A$ and $r_m\in{\mathbf{Q}}$, the rational numbers. We write $x\in U$to mean that d(a_m,x)<r_m for some $m\in{\mathbf{N}}$. A closed set $C\subseteq X$ is defined to be the complement of an open set U, i.e., $\forall x\in X(x\in C\leftrightarrow x\notin U)$.

It will sometimes be necessary to consider a slightly different notion. A (code for a) separably closed set $K=\overline{S}\subseteq X$ is defined to be a countable sequence of points $S\subseteq X$. We write $x\in K$ to mean that for all $\varepsilon>0$ there exists $y\in S$ such that $d(x,y)<\varepsilon$. It is provable in $\mathsf{ACA}_0$ (but not in weaker systems) that for every separably closed set K there exists an equivalent closed set C, i.e., $\forall x\in X(x\in C\leftrightarrow x\in K)$. For further details on separably closed sets, see [2,3,4].

Within $\mathsf{RCA}_0$, a compact set $K\subseteq X$ is defined to be a separably closed set such that there exists a sequence of finite sequences of points $x_{ni}\in K$, $i\le k_n$, $n\in{\mathbf{N}}$, such that for all $n\in{\mathbf{N}}$ and all $x\in K$ there exists $i\le k_n$ with d(x,x_ni)<1/2ⁿ. The sequence of positive integers k_n, $n\in{\mathbf{N}}$, is also required to exist. It is provable in $\mathsf{RCA}_0$ that compact sets are closed and located [8]. It is provable in $\mathsf{WKL}_0$ that compact sets have the Heine-Borel covering property, i.e., any covering of K by a sequence of open sets has a finite subcovering.

Within $\mathsf{RCA}_0$, a (code for a) separable Banach space $X=\widehat{A}$ is defined to be a countable pseudonormed vector space A over Q. With $d(a,b)=\Vert a-b\Vert$, X is a complete separable metric space and has the usual structure of a Banach space over R. A bounded linear functional $F:X\to{\mathbf{R}}$ may be defined as a continuous function which is linear. The equivalence of continuity and boundedness is provable in $\mathsf{RCA}_0$. We write $\Vert F\Vert\le\alpha$ to mean that $\vert F(x)\vert\le\alpha\Vert x\Vert$ for all $x\in X$.