A Density Theorem for Hierarchies of Limit Spaces over Separable Metric Spaces

In this paper, we show, almost constructively, a density theorem for hierarchies of limit spaces over separable metric spaces. Our proof is not fully constructive, since it relies on the constructively not acceptable fact that the limit relation induced by a metric space satisfies Urysohn's axiom for limit spaces. By adding the condition of strict positivity to Normann's notion of probabilistic projection we establish a relation between strictly positive general probabilistic selections on a sequential space and general approximation functions on a limit space. Showing that Normann's result, that a (general and strictly positive) probabilistic selection is definable on a separable metric space, admits a constructive proof, and based on the constructively shown in [18] cartesian closure property of the category of limit spaces with general approximations, our quite effective density theorem follows. This work, which is a continuation of [18], is within computability theory at higher types and Normann's Program of Internal Computability.