Searching through the reals

TL;DR

This paper explores principles from Nonstandard Analysis that enable a form of 'searching through the reals', linking these principles to known systems in Reverse Mathematics and revealing their computational strength.

Contribution

It introduces and analyzes principles (PB) and (TB) that formalize a 'search through the reals' concept, connecting them to hyperjump and $ riangle_{1}^{1}$-comprehension systems.

Findings

(PB) and (TB) are equivalent to hyperjump existence and $ riangle_{1}^{1}$-comprehension.

These principles show that Nonstandard Analysis can treat number and set quantifiers as bounded searches.

The principles reveal a similarity to Turing jump and recursive comprehension.

Abstract

It is a commonplace to say that `one can search through the natural numbers', by which is meant the following: For a property, decidable in finite time and which is not false for all natural numbers, checking said property starting at zero, then for one, for two, and so on, one will eventually find a natural number which satisfies the property, assuming no resource bounds. By contrast, it seems one cannot search through the real numbers in any similarly `basic' fashion: The reals numbers are not countable, and their well-orders carry extreme logical strength compared to the basic notions involved in `searching through the natural numbers'. In this paper, we study two principles (PB) and (TB) from Nonstandard Analysis which essentially state that `one can search through the reals'. These principle are basic in that they involve only constructive objects of type zero and one, and the associated `search through the reals' amounts to nothing more than a bounded search involving nonstandard numbers as upper bound, but independent of the choice of this number. We show that (PB) and (TB) are equivalent to known systems from Reverse Mathematics, namely respectively the existence of the hyperjump and $\Delta_{1}^{1}$-comprehension. We also show that (PB) and (TB) exhibit remarkable similarity to, respectively,the Turing jump and recursive comprehension. In particular, we show that Nonstandard Analysis allows us to treat number quantifiers as `one-dimensional' bounded searches, and set quantifiers as `two-dimensional' bounded searches.