Date: April 18, 1998 Title: Located Sets and Reverse Mathematics Authors: Mariagnese Giusto and Stephen G. Simpson Author e-mail: simpson@math.psu.edu Available: http://www.math.psu.edu/simpson/papers/loc9804.ps Format: PostScript file (AMS-LaTeX source is also available) Publication: accepted August 26, 1998 for publication in the Journal of Symbolic Logic Abstract: The notion of located set has been useful in Bishop-style constructivism. We transplant this notion to another context: subsystems of second order arithmetic and reverse mathematics. The following definitions are made in RCA_0. Let X be a compact metric space, or we may take X=[0,1]. A set K included in X is said to be closed if it is the complement of a sequence of open balls; separably closed if it is the closure of a sequence of points; located if the distance function d(x,K) exists as a continuous real-valued function on X; weakly located if the predicate d(x,K)>r is Sigma^0_1 (allowing parameters, of course). Note that located implies weakly located. We denote by C(K) the continuous real-valued functions on K which have a modulus of uniform continuity. The strong Tietze theorem for K says that every phi in C(K) extends to Phi in C(X). Theorem 1. In RCA_0 we have: 1. the functions in C(X) form a separable Banach space (with the sup norm); 2. the nonempty closed located sets in X form a compact metric space (with the Hausdorff metric); 3. closed + located implies separably closed; 4. separably closed + weakly located implies closed + located; 5. strong Tietze theorem for closed, weakly located sets. Theorem 2. In RCA_0 the following statements are pairwise equivalent: 1. ACA_0; 2. closed implies located; 3. closed implies separably closed; 4. separably closed implies closed; 5. separably closed implies located; 6. separably closed implies weakly located; 7. closed + weakly located implies located; 8. closed + weakly located implies separably closed; Theorem 3. In RCA_0 the following statements are pairwise equivalent: 1. WKL_0; 2. closed implies weakly located; 3. closed + separably closed implies located; 4. closed + separably closed implies weakly located; 5. strong Tietze theorem for separably closed sets. In particular, WKL_0 proves the strong Tietze theorem for closed sets. We conjecture the reverse. We can show that the strong Tietze theorem for closed, separably closed sets implies the DNR axiom: for all A included in N there exists f : N -> N which is diagonally nonrecursive relative to A.