The prerequisite for a thorough understanding of this paper is familiarity with the basics of separable Banach space theory as developed in . 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 , a (code for a) complete separable metric space is defined to be a countable set together with a function satisfying d(a,a)=0, d(a,b)=d(b,a), and . A (code for a) point of X is defined to be a sequence of elements of A such that . We extend d from A to X in the obvious way. For we define x=y to mean that d(x,y)=0.
Within , (a code for) an open set in X is defined to be a sequence of ordered pairs where and , the rational numbers. We write to mean that d(am,x)<rm for some . A closed set is defined to be the complement of an open set U, i.e., .
It will sometimes be necessary to consider a slightly different notion. A (code for a) separably closed set is defined to be a countable sequence of points . We write to mean that for all there exists such that . It is provable in (but not in weaker systems) that for every separably closed set K there exists an equivalent closed set C, i.e., . For further details on separably closed sets, see [2,3,4].
Within , a compact set is defined to be a separably closed set such that there exists a sequence of finite sequences of points , , , such that for all and all there exists with d(x,xni)<1/2n. The sequence of positive integers kn, , is also required to exist. It is provable in that compact sets are closed and located . It is provable in 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 , a (code for a) separable Banach space is defined to be a countable pseudonormed vector space A over Q. With , X is a complete separable metric space and has the usual structure of a Banach space over R. A bounded linear functional may be defined as a continuous function which is linear. The equivalence of continuity and boundedness is provable in . We write to mean that for all .