arXiv subjects

Sam Sanders

Publications and source records attributed to Sam Sanders.

69 records · Page 4Linked to original sources

arXiv2017

The Gandy-Hyland functional and a hitherto unknown computational aspect of Nonstandard Analysis

In this paper, we highlight a new computational aspect of Nonstandard Analysis relating to higher-order computability theory. In particular, we prove that the Gandy-Hyland functional equals a primitive recursive functional involving nonstandard numbers inside Nelson's internal set theory. From this classical and ineffective proof in Nonstandard Analysis, a term from Goedel's system T is extracted which computes the Gandy-Hyland functional in terms of a modulus-of-continuity functional and a special case of the fan functional. We obtain several similar relative computability results not involving Nonstandard Analysis from their associated nonstandard theorems, in particular involving the weak continuity functional. By way of reversal, we show that certain relative computability results, called Herbrandisations, also imply the nonstandard theorem from whence they were obtained. Thus, we establish a direct two-way connection between the field Computability (in particular theoretical computer science) and the field Nonstandard Analysis.

math.LO↗

arXiv2017

Approaches to analysis with infinitesimals following Robinson, Nelson, and others

This is a survey of several approaches to the framework for working with infinitesimals and infinite numbers, originally developed by Abraham Robinson in the 1960s, and their constructive engagement with the Cantor-Dedekind postulate and the Intended Interpretation hypothesis. We highlight some applications including (1) Loeb's approach to the Lebesgue measure, (2) a radically elementary approach to the vibrating string, (3) true infinitesimal differential geometry. We explore the relation of Robinson's and related frameworks to the multiverse view as developed by Hamkins. Keywords: axiomatisations, infinitesimal, nonstandard analysis, ultraproducts, superstructure, set-theoretic foundations, multiverse, naive integers, intuitionism, soritical properties, ideal elements, protozoa.

math.CA↗

arXiv2017

Refining the taming of the Reverse Mathematics zoo

Reverse Mathematics is a program in the foundations of mathematics. It provides an elegant classification in which the majority of theorems of ordinary mathematics fall into only five categories, based on the 'Big Five' logical systems. Recently, a lot of effort has been directed towards finding exceptional theorems, i.e. which fall outside the Big Five. The so-called Reverse Mathematics zoo is a collection of such exceptional theorems (and their relations). It was shown in [17] that a number of uniform versions of the zoo-theorems, i.e. where a functional computes the objects stated to exist, fall in the third Big Five category arithmetical comprehension, inside Kohlenbach's higher-order Reverse Mathematics. In this paper, we extend and refine the results from [17]. In particular, we establish analogous results for recent additions to the Reverse Mathematics zoo, thus establishing that the latter disappear at the uniform level. Furthermore, we show that the aforementioned equivalences can be proved using only intuitionistic logic. Perhaps most surprisingly, these explicit equivalences are extracted from nonstandard equivalences in Nelson's internal set theory, and we show that the nonstandard equivalence can be recovered from the explicit ones.

math.LO↗

arXiv2017

Reverse Formalism 16

In his remarkable paper Formalism64, Robinson defends his philsophocal position as follows: (i) Any mention of infinite totalities is literally meaningless. (ii) We should act as if infinite totalities really existed. Being the originator of Nonstandard Analysis, it stands to reason that Robinson would have often been faced with the opposing position that 'some infinite totalities are more meaningful than others', the textbook example being that of infinitesimals (versus less controversial infinite totalities). For instance, Bishop and Connes have made such claims regarding infinitesimals, and Nonstandard Analysis in general, going as far as calling the latter respectively a debasement of meaning and virtual, while accepting as meaningful other infinite totalities and the associated mathematical framework. We shall study the critique of Nonstandard Analysis by Bishop and Connes, and observe that these authors equate 'meaning' and 'computational content', though their interpretations of said content vary. As we will see, Bishop and Connes claim that the presence of ideal objects (in particular infinitesimals) in Nonstandard Analysis yields the absence of meaning (i.e. computational content). We will debunk the Bishop-Connes critique by establishing the contrary, namely that the presence of ideal objects (in particular infinitesimals) in Nonstandard Analysis yields the ubiquitous presence of computational content. In particular, infinitesimals provide an elegant shorthand for expressing computational content. To this end, we introduce a direct translation be- tween a large class of theorems of Nonstandard Analysis and theorems rich in computational content (not involving Nonstandard Analysis), similar to the 'reversals' from the foundational program Reverse Mathematics. The latter also plays an important role in gauging the scope of this translation.

math.LO↗

arXiv2017

From Nonstandard Analysis to various flavours of Computability Theory

As suggested by the title, it has recently become clear that theorems of Nonstandard Analysis (NSA) give rise to theorems in computability theory (no longer involving NSA). Now, the aforementioned discipline divides into classical and higher-order computability theory, where the former (resp. the latter) sub-discipline deals with objects of type zero and one (resp. of all types). The aforementioned results regarding NSA deal exclusively with the higher-order case; we show in this paper that theorems of NSA also give rise to theorems in classical computability theory by considering so-called textbook proofs.

math.LO↗

arXiv2016

On the computational content of the Loeb measure

The Loeb measure is one of the cornerstones of Nonstandard Analysis. The traditional development of the Loeb measure makes use of saturation and external sets. Inspired by [13], we give meaning to special cases of the Loeb measure in the weak fragment $\textsf{P}$ of Nelson's internal set theory from [1]. Perhaps surprisingly, our definition of the Loeb measure has computational content in the sense of the `term extraction' framework from [1].

math.LO↗

arXiv2016

The computational content of Nonstandard Analysis

Kohlenbach's proof mining program deals with the extraction of effective information from typically ineffective proofs. Proof mining has its roots in Kreisel's pioneering work on the so-called unwinding of proofs. The proof mining of classical mathematics is rather restricted in scope due to the existence of sentences without computational content which are provable from the law of excluded middle and which involve only two quantifier alternations. By contrast, we show that the proof mining of classical Nonstandard Analysis has a very large scope. In particular, we will observe that this scope includes any theorem of pure Nonstandard Analysis, where `pure' means that only nonstandard definitions (and not the epsilon-delta kind) are used. In this note, we survey results in analysis, computability theory, and Reverse Mathematics.

cs.LO↗

arXiv2015

The effective content of Reverse Nonstandard Mathematics and the nonstandard content of effective Reverse Mathematics

The aim of this paper is to highlight a hitherto unknown computational aspect of Nonstandard Analysis pertaining to Reverse Mathematics (RM). In particular, we shall establish RM-equivalences between theorems from Nonstandard Analysis in a fragment of Nelson's internal set theory. We then extract primitive recursive terms from Goedel's system T (not involving Nonstandard Analysis) from the proofs of the aforementioned nonstandard equivalences. The resulting terms turn out to be witnesses for effective1 equivalences in Kohlenbach's higher-order RM. In other words, from an RM-equivalence in Nonstandard Analysis, we can extract the associated effective higher-order RM-equivalence which does not involve Nonstandard Analysis anymore. Finally, we show that certain effective equivalences in turn give rise to the original nonstandard theorems from which they were derived.

math.LO↗

arXiv2015

Non-standard Nonstandard Analysis and the computational content of standard mathematics

The aim of this paper is to highlight a hitherto unknown computational aspect of Nonstandard Analysis. Recently, a number of nonstandard versions of Goedel's system T have been introduced ([2,9,12]), and it was shown in [26] that the systems from [2] play a pivotal role in extracting computational information from proofs in Nonstandard Analysis. It is a natural question if similar techniques may be used to extract computational information from proofs not involving Nonstandard Analysis. In this paper, we provide a positive answer to this question using the nonstandard system from [9]. This system validates so-called non-standard uniform boundedness principles which are central to Kohlenbach's approach to proof mining ([14]). In particular, we show that from classical and ineffective existence proofs (not involving Nonstandard Analysis but using weak Koenig's lemma), one can `automatically' extract approximations to the objects claimed to exist.

math.LO↗

arXiv2015

The taming of the Reverse Mathematics zoo

Reverse Mathematics is a program in the foundations of mathematics. Its results give rise to an elegant classification of theorems of ordinary mathematics based on computability. In particular, the majority of these theorems fall into only five categories of which the associated logical systems are dubbed `the Big Five'. Recently, a lot of effort has been directed towards finding \emph{exceptional} theorems, i.e.\ which fall outside the Big Five categories. The so-called Reverse Mathematics zoo is a collection of such exceptional theorems (and their relations). In this paper, we show that the uniform versions of the zoo-theorems, i.e. where a functional computes the objects stated to exist, all fall in the third Big Five category arithmetical comprehension, inside Kohlenbach's higher-order Reverse Mathematics. In other words, the zoo seems to disappear at the uniform level. Our classification applies to all theorems whose objects exhibit little structure, a notion we conjecture to be connected to Montalban's notion robustness. Surprisingly, our methodology reveals a hitherto unknown `computational' aspect of Nonstandard Analysis: We shall formulate an algorithm $\mathfrak{RS}$ which takes as input the proof of a specific equivalence in Nelson's internal set theory, and outputs the proof of the desired equivalence (not involving Nonstandard Analysis) between the uniform zoo principle and arithmetical comprehension. Moreover, the equivalences thus proved are even explicit, i.e. a term from the language converts the functional from one uniform principle into the functional from the other one and vice versa.

math.LO↗

arXiv2015

More than bargained for in Reverse Mathematics

Reverse Mathematics (RM for short) is a program in the foundations of mathematics with the aim of finding the minimal axioms required for proving theorems about countable and separable objects. RM usually takes place in second-order arithmetic and due to this choice of framework, continuous real-valued functions have to be represented by so-called codes. Kohlenbach has shown that the RM-definition of continuity-via-codes constitutes a slight constructive enrichment of the epsilon-delta definition, namely in the form of a modulus of continuity. In this paper, we show that the RM-definition of continuity also gives rise to a `nonstandard' enrichment in the form of nonstandard continuity from Nonstandard Analysis. This observation allows us to (i) establish that RM-theorems related to continuity are implicitly higher-order statements, (ii) prove equivalences between RM-theorems concerning continuity and their associated higher-order versions, and (iii) obtain explicit equivalences between higher-order theorems from the equivalence between the corresponding RM-theorems. Moreover, we show that it is exactly the RM-definition of continuity-via-codes which gives rise to these higher-order phenomena. In conclusion, we establish that the practice of coding in RM, designed to obviate higher-type objects, actually introduces a host of new ones.

math.LO↗

arXiv2015

Searching through the reals

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 $Δ_{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.

math.LO↗

arXiv2015

Uniform and nonstandard existence in Reverse Mathematics

Reverse Mathematics is a program in the foundations of mathematics which provides an elegant classification of theorems of ordinary mathematics based on computability. Our aim is to provide an alternative classification of theorems based on the central tenet of Feferman's Explicit Mathematics, namely that a proof of existence of an object yields a procedure to compute said object. Our classification gives rise to the Explicit Mathematics theme (EMT) of Nonstandard Analysis. Intuitively speaking, the EMT states that a standard object with certain properties can be computed by a functional if and only if this object exists classically with these same standard and nonstandard properties. In this paper, we establish examples for the EMT ranging from the weakest to the strongest Big Five system of Reverse Mathematics. Our results are proved over the usual base theory of Reverse Mathematics, conservatively extended with higher types and Nelson's internal approach to Nonstandard Analysis.

math.LO↗

arXiv2015

Reverse Mathematics of Brouwer's continuity theorem and related principles

In intuitionistic mathematics, the Brouwer Continuity Theorem states that all total real functions are (uniformly) continuous on the unit interval. We study this theorem and related principles from the point of view of Reverse Mathematics over a base theory accommodating higher types and Nonstandard Analysis. With regard to the bigger picture, Reverse Mathematics provides a classification of theorems of ordinary mathematics based on computability. Our aim is to provide an alternative classification of theorems based on the central tenet of Feferman's Explicit Mathematics}, namely that a proof of existence of an object yields a procedure to compute said object. Our classification gives rise to the Explicit Mathematics theme (EMT). Intuitively speaking, the EMT states that a standard object with certain properties can be computed by a functional if and only if this object exists classically with these same standard and nonstandard properties. Hence, we establish the EMT for a series of intuitionistic principles in this paper.

math.LO↗

arXiv2014

Algorithm and proof as Ω-invariance and transfer: A new model of computation in nonstandard analysis

We propose a new model of computation based on nonstandard analysis. Intuitively, the role of "algorithm" is played by a new notion of finite procedure, called Omega-invariance and inspired by physics, from nonstandard analysis. Moreover, the role of 'proof' is taken up by the Transfer Principle from nonstandard analysis. We obtain a number of results in Constructive Reverse Mathematics to illustrate the tight correspondence to Errett Bishop's Constructive Analysis and the associated Constructive Reverse Mathematics.

cs.LO↗