
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsMathematical and Theoretical Analysis · Computability, Logic, AI Algorithms · Philosophy and History of Science
