Much is known concerning reverse mathematics for real analysis and the topology of complete separable metric spaces. Some of the inspiration for this comes from recursive analysis  and Bishop-style constructivism . We shall not discuss those connections here, but see my book  for more information.
In Giusto/Simpson  we presented a rather thorough reverse mathematics discussion of various notions of closed set, and of various forms of the Tietze extension theorem for real-valued continuous functions on closed sets, in compact metric spaces. The purpose of this section is to call attention to one open problem left over from that paper.
Let X be a compact metric space. For concreteness we may take X=[0,1], the unit interval. In we define 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 (allowing parameters, of course). C(X) denotes the separable Banach space of continuous real-valued functions on X which have a modulus of uniform continuity. The strong Tietze theorem for K is the statement that every extends to some . See  for details.
Known results from  are:
It is known from  that (3) and (4) are provable in and not provable in . There is a partial reversal: (3) or (4) implies the DNR axiom over . We shall outline the proof of this below. But first we discuss the DNR axiom.
The DNR axiom says: For every there exists which is diagonally nonrecursive relative to A, i.e., for all . Here is the set of natural numbers. It would be possible to restate the DNR axiom in a combinatorial way, not involving recursion theory, but we shall not do so here.
The DNR axiom is known to be weaker than ( weak König's lemma). Indeed, the DNR axiom is provable in the strictly weaker system ( weak weak König's lemma) which arises in connection with reverse mathematics for measure theory. (See [32, §X.1], , .) Because of Kumabe's result , it seems likely that the DNR axiom is strictly weaker than .
Recursion theorists can understand these variants of weak König's lemma in terms of separating sets, recursively bounded classes, etc. Thus there is a close connection with Jockusch's talk at this conference. In descending order we have:
We shall now end this section with an outline of the proof that the strong Tietze theorem for closed, separably closed subsets of [0,1]implies the DNR axiom.
We may as well assume that weak König's lemma fails. For each nlet In be the closed interval [1/22n+1,1/22n]. Since weak König's lemma fails, the Heine/Borel covering lemma fails, so let (ank,bnk), , be a covering of In by open intervals with no finite subcovering. We may assume that these coverings are disjoint from one other.
is defined, let sn be the least s such that
is defined, and put
Define a real-valued continuous function on K, as follows. First let pi(x), , be a fixed, one-to-one, recursive enumeration of , the ring of polynomials with rational coefficients in one indeterminate, x. Using this, define and, for and , if for some , otherwise. It can be shown that .
By the strong Tietze theorem for K, let be an extension of from K to all of [0,1]. By Weierstrass polynomial approximation in , let pin(x), , be a sequence of polynomials such that for all n. It is not difficult to show that the function given by f(n)=in is DNR.
By relativizing the above to an arbitrary , we get a function that is DNR relative to A. This completes the proof.
Note: Recursion theorists may want to view the above as a standard diagonal construction leading to a recursive counterexample to (4). However, from the viewpoint of reverse mathematics, there seems to be something unusual going on here. Usually, a recursive counterexample leads to a reversal to or , but in this instance all we seem to get is a reversal to the DNR axiom.