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.