The authors show that some reverse mathematics proofs translate naturally into computable analysis proofs. For this they relate to each statement of a form that often appears in the context of reverse mathematics a certain multivalued function.
In this way the multivalued function Sep – which for each \(p\), \(q\) of elements of Baire space with disjoint ranges yields the set of the characteristic functions of sets of natural numbers separating the range of \(p\) and the range of \(q\) – corresponds to a statement that is equivalent to WKL\(_0\).
It is shown that a multivalued function associated with the Hahn-Banach Extension Theorem is Sep-complete.