On the connection between Nonstandard Analysis and Computability Theory

As reported in [11-14], higher-order computability results (including Reverse Mathematics) can be extracted from a large class of theorems in Nonstandard Analysis (NSA). Two possible points of criticism regarding these results are as follows: (1) Classical computabilitytheory and Friedman-Simpson-style ReverseMathematics do not really deal with higher type objects (beyond zero and one). Is it possible to obtain low type (i.e. second-order) computability theoretic results (including Reverse Mathematics) from NSA? (2) So-called Weihrauch reducibility provides a computability theoretic classification of mathematical theorems which takes into account the use of resources. Is it possible to obtain resource-sensitive results in computability theory from NSA? In this paper, we provide partial positive answers to these questions. The crux of our approach is the replacement in theorems of NSA of all type one quantifiers by (type zero) quantifiers over all A-computable functions, for some oracle A which appears as a parameter. This operation sufficiently lowers all types involved and also leads to resource sensitive results. We discuss an example based on the monotone convergence theorem, and one based on weak Koenig's lemma. We make essential use of the ECF-translation.