arXiv subjects

Sam Sanders

Publications and source records attributed to Sam Sanders.

At least 55 records · Page 3Linked to original sources

arXiv2020

Reverse Mathematics of the uncountability of $\mathbb{R}$: Baire classes, metric spaces, and unordered sums

Dag Normann and the author have recently initiated the study of the logical and computational properties of the uncountability of $\mathbb{R}$ formalised as the statement $\textsf{NIN}$ (resp. $\textsf{NBI}$ that there is no injection (resp. bijection) from $[0,1]$ to $\mathbb{N}$. On one hand, these principles are hard to prove relative to the usual scale based on comprehension and discontinuous functionals. On the other hand, these principles are among the weakest principles on a new complimentary scale based on (classically valid) continuity axioms from Brouwer's intuitionistic mathematics. We continue the study of $\textsf{NIN}$ and $\textsf{NBI}$ relative to the latter scale, connecting these principles with theorems about Baire classes, metric spaces, and unordered sums. The importance of the first two topics requires no explanation, while the final topic's main theorem, i.e. that when they exist, unordered sums are (countable) series, has the rather unique property of implying $\textsf{NIN}$ formulated with the Cauchy criterion, and (only) $\textsf{NBI}$ when formulated with limits. This study is undertaken within Ulrich Kohlenbach's framework of higher-order Reverse Mathematics.

math.LO↗

arXiv2020

Open sets in computability theory and Reverse Mathematics

To enable the study of open sets in computational approaches to mathematics, lots of extra data and structure on these sets is assumed. For both foundational and mathematical reasons, it is then a natural question, and the subject of this paper, what the influence of this extra data and structure is on the logical and computational properties of basic theorems pertaining to open sets. To answer this question, we study various basic theorems of analysis, like the Baire category, Heine, Heine-Borel, Urysohn, and Tietze theorems, all for open sets given by their (third-order) characteristic functions. Regarding computability theory, the objects claimed to exist by the aforementioned theorems undergo a shift from `computable' to `not computable in any type two functional', following Kleene's S1-S9. Regarding Reverse Mathematics, the latter's so-called Main Question, namely which set existence axioms are necessary for proving a given theorem, does not have a unique or unambiguous answer for the aforementioned theorems, working in Kohlenbach's higher-order framework. A finer study of representations of open sets leads to the new `$Δ$-functional' which has unique (computational) properties.

math.LO↗

arXiv2020

Plato and the foundations of mathematics

Plato is well-known in mathematics for the eponymous foundational philosophy Platonism based on ideal objects. Plato's allegory of the cave provides a powerful visual illustration of the idea that we only have access to shadows or reflections of these ideal objects. An inquisitive mind might then wonder what the current foundations of mathematics, like e.g. Reverse Mathematics and the associated Goedel hierarchy, are reflections of. In this paper, we identify a hierarchy in higher-order arithmetic that maps to the Big Five of Reverse Mathematics under the canonical embedding of higher-order into second-order arithmetic. Conceptually pleasing, the latter mapping replaces uncountable objects by countable 'codes', i.e. the very practise of formalising mathematics in second-order arithmetic. This higher-order hierarchy can be defined in Hilbert-Bernays' Grundlagen, the spiritual ancestor of second-order arithmetic, while the associated embedding preserves equivalences. Also, in contrast to Kohlenbach's hierarchy based on discontinuity, our hierarchy can be formulated in terms of (classically valid) continuity axioms from Brouwer's intuitionistic mathematics. Moreover, the higher-order counterpart of sequences is provided by nets, aka Moore-Smith sequences, while the gauge integral is the correct generalisation of the Riemann integral. For all these reasons, we baptise our higher-order hierarchy the Plato hierarchy.

math.LO↗

arXiv2020

Lifting countable to uncountable mathematics

Turing's famous 'machine' framework provides an intuitively clear conception of 'computing with real numbers'. A recursive counterexample to a theorem shows that the theorem does not hold when restricted to computable objects. These counterexamples are often crucial in establishing reversals in the Reverse Mathematics program. All the previous is essentially limited to a language that can only express countable mathematics directly. The aim of this paper is to show that reversals and recursive counterexamples, countable in nature as they might be, directly yield new and interesting results about uncountable mathematics with little-to-no modification. We shall treat the following topics/theorems: the monotone convergence theorem/Specker sequences, compact and closed sets in metric spaces, the Rado selection lemma, the ordering and algebraic closures of fields, and ideals of rings. The higher-order generalisation of sequence is of course provided by nets (aka Moore-Smith sequences ).

math.LO↗

arXiv2020

Reverse Mathematics of topology: dimension, paracompactness, and splittings

Reverse Mathematics (RM hereafter) is a program in the foundations of mathematics founded by Friedman and developed extensively by Simpson and others. The aim of RM is to find the minimal axioms needed to prove a theorem of ordinary, i.e. non-set-theoretic, mathematics. As suggested by the title, this paper deals with the study of the topological notions of dimension and paracompactness, inside Kohlenbach's higher-order RM. As to splittings, there are some examples in RM of theorems $A, B, C$ such that $A\leftrightarrow(B\wedge C)$, i.e. $A$ can be split into two independent (fairly natural) parts $B$ and $C$, and the aforementioned topological notions give rise to a number of splittings involving highly natural $A, B, C$. Nonetheless, the higher-order picture is markedly different from the second-one: in terms of comprehension axioms, the proof in higher-order RM of e.g. the paracompactness of the unit interval requires full second-order arithmetic, while the second-order/countable version of paracompactness of the unit interval is provable in the base theory of second-order RM. We obtain similarly 'exceptional' results for the Urysohn identity, the Lindelöf lemma, and partitions of unity. We show that our results exhibit a certain robustness, in that they do not depend on the exact definition of cover, even in the absence of the axiom of choice.

math.LO↗

arXiv2020

Pincherle's theorem in Reverse Mathematics and computability theory

We study the logical and computational properties of basic theorems of uncountable mathematics, in particular Pincherle's theorem, published in 1882. This theorem states that a locally bounded function is bounded on certain domains, i.e. one of the first 'local-to-global' principles. It is well-known that such principles in analysis are intimately connected to (open-cover) compactness, but we nonetheless exhibit fundamental differences between compactness and Pincherle's theorem. For instance, the main question of Reverse Mathematics, namely which set existence axioms are necessary to prove Pincherle's theorem, does not have an unique or unambiguous answer, in contrast to compactness. We establish similar differences for the computational properties of compactness and Pincherle's theorem. We establish the same differences for other local-to-global principles, even going back to Weierstrass. We also greatly sharpen the known computational power of compactness, for the most shared with Pincherle's theorem however. Finally, countable choice plays an important role in the previous, we therefore study this axiom together with the intimately related Lindelöf lemma.

math.LO↗

arXiv2019

Nets and Reverse Mathematics, a pilot study

Nets are generalisations of sequences involving possibly uncountable index sets; this notion was introduced about a century ago by Moore and Smith. They also established the generalisation to nets of various basic theorems of analysis due to Bolzano-Weierstrass, Dini, Arzela, and others. More recently, nets are central to the development of domain theory, providing intuitive definitions of the associated Scott and Lawson topologies, among others. This paper deals with the Reverse Mathematics study of basic theorems about nets. We restrict ourselves to nets indexed by subsets of Baire space, and therefore third-order arithmetic, as such nets suffice to obtain our main results. Over Kohlenbach's base theory of higher-order Reverse Mathematics, the Bolzano-Weierstrass theorem for nets implies the Heine-Borel theorem for uncountable covers. We establish similar results for other basic theorems about nets and even some equivalences, e.g. for Dini's theorem for nets. Finally, we show that replacing nets by sequences is hard, but that replacing sequences by nets can obviate the need for the Axiom of Choice, a foundational concern in domain theory. In an appendix, we study the power of more general index sets, establishing that the 'size' of a net is directly proportional to the power of the associated convergence theorem.

math.LO↗

arXiv2019

Computability Theory, Nonstandard Analysis, and their connections

We investigate the connections between computability theory and Nonstandard Analysis. In particular, we investigate the two following topics and show that they are intimately related. (T.1) A basic property of Cantor space $2^{\mathbb{N}}$ is Heine-Borel compactness: For any open cover of $2^{\mathbb{N}}$, there is a finite sub-cover. A natural question is: How hard is it to compute such a finite sub-cover? We make this precise by analyzing the complexity of functionals that given any $g:2^{\mathbb{N}}\rightarrow \mathbb{N}$, output a finite sequence $\langle f_0 , \dots, f_n\rangle $ in $2^{\mathbb{N}}$ such that the neighbourhoods defined from $\bar{f_i}g(f_i)$ for $i\leq n$ form a cover of Cantor space. (T.2) A basic property of Cantor space in Nonstandard Analysis is Abraham Robinson's nonstandard compactness, i.e. that every binary sequence is `infinitely close' to a standard binary sequence. We analyze the strength of this nonstandard compactness property of Cantor space, compared to the other axioms of Nonstandard Analysis and usual mathematics. The study of (T.1) gives rise to exotic objects in computability theory, while (T.2) leads to surprising results in Reverse Mathematics. We stress that (T.1) and (T.2) are highly intertwined and that our study of these topics is `holistic' in nature: results in computability theory give rise to results in Nonstandard Analysis and vice versa.

math.LO↗

arXiv2019

The strength of compactness in Computability Theory and Nonstandard Analysis

Compactness is one of the core notions of analysis: it connects local properties to global ones and makes limits well-behaved. We study the computational properties of the compactness of Cantor space $2^{\mathbb{N}}$ for uncountable covers. The most basic question is: how hard is it to compute a finite sub-cover from such a cover of $2^{\mathbb{N}}$? Another natural question is: how hard is it to compute a sequence that covers $2^{\mathbb{N}}$ minus a measure zero set from such a cover? The special and weak fan functionals respectively compute such finite sub-covers and sequences. In this paper, we establish the connection between these new fan functionals on one hand, and various well-known comprehension axioms on the other hand, including arithmetical comprehension, transfinite recursion, and the Suslin functional. In the spirit of Reverse Mathematics, we also analyse the logical strength of compactness in Nonstandard Analysis. Perhaps surprisingly, the results in the latter mirror (often perfectly) the computational properties of the special and weak fan functionals. In particular, we show that compactness (nonstandard or otherwise) readily brings us to the outer edges of Reverse Mathematics (namely $Π_2^1$-CA$_0$), and even into Schweber's higher-order framework (namely $Σ_{1}^{2}$-separation).

math.LO↗

arXiv2019

On the mathematical and foundational significance of the uncountable

We study the logical and computational properties of basic theorems of uncountable mathematics, including the Cousin and Lindelöf lemma published in 1895 and 1903. Historically, these lemmas were among the first formulations of open-cover compactness and the Lindelöf property, respectively. These notions are of great conceptual importance: the former is commonly viewed as a way of treating uncountable sets like e.g. $[0,1]$ as 'almost finite', while the latter allows one to treat uncountable sets like e.g. $\mathbb{R}$ as 'almost countable'. This reduction of the uncountable to the finite/countable turns out to have a considerable logical and computational cost: we show that the aforementioned lemmas, and many related theorems, are extremely hard to prove, while the associated sub-covers are extremely hard to compute. Indeed, in terms of the standard scale (based on comprehension axioms), a proof of these lemmas requires at least the full extent of second-order arithmetic, a system originating from Hilbert-Bernays' Grundlagen der Mathematik. This observation has far-reaching implications for the Grundlagen's spiritual successor, the program of Reverse Mathematics, and the associated Gödel hierachy. We also show that the Cousin lemma is essential for the development of the gauge integral, a generalisation of the Lebesgue and improper Riemann integrals that also uniquely provides a direct formalisation of Feynman's path integral.

math.LO↗

arXiv2019

Splittings and disjunctions in Reverse Mathematics

Reverse Mathematics (RM hereafter) is a program in the foundations of mathematics founded by Friedman and developed extensively by Simpson and others. The aim of RM is to find the minimal axioms needed to prove a theorem of ordinary, i.e. non-set-theoretic, mathematics. As suggested by the title, this paper deals with two (relatively rare) RM-phenomena, namely splittings and disjunctions. As to splittings, there are some examples in RM of theorems $A, B, C$ such that $A\leftrightarrow (B\wedge C)$, i.e. $A$ can be split into two independent (fairly natural) parts $B$ and $C$. As to disjunctions, there are (very few) examples in RM of theorems $D, E, F$ such that $D\leftrightarrow (E\vee F)$, i.e. $D$ can be written as the disjunction of two independent (fairly natural) parts $E$ and $F$. By contrast, we show in this paper that there is a plethora of (natural) splittings and disjunctions in Kohlenbach's higher-order RM. Finally, we discuss the role of these results in the grand scheme of things.

math.LO↗

arXiv2018

A note on non-classical Nonstandard Arithmetic

Recently, a number of formal systems for Nonstandard Analysis restricted to the language of finite types, i.e. nonstandard arithmetic, have been proposed. We single out one particular system by Dinis-Gaspar, which is categorised by the authors as being part of intuitionistic nonstandard arithmetic. Their system is indeed inconsistent with the Transfer axiom of Nonstandard Analysis, and the latter axiom is classical in nature as it implies (higher-order) comprehension. In this paper, we answer the following questions: (Q1) In the spirit of Reverse Mathematics, what is the minimal fragment of Transfer that is inconsistent with the Dinis-Gaspar system? (Q2) What other axioms are inconsistent with the Dinis-Gaspar system? Perhaps surprisingly, the answer to the second question shows that the Dinis-Gaspar system is inconsistent with a number of (non-classical) continuity theorems which one would -- in our opinion -- categorise as intuitionistic. Finally, we show that the Dinis-Gaspar system involves a standard part map, suggesting this system also pushes the boundary of what still counts as 'Nonstandard Analysis' or 'internal set theory'.

math.LO↗

arXiv2018

Reverse Mathematics and parameter-free Transfer

Recently, conservative extensions of Peano and Heyting arithmetic in the spirit of Nelson's axiomatic approach to Nonstandard Analysis, have been proposed. In this paper, we study the Transfer axiom of Nonstandard Analysis restricted to formulas without parameters. Based on this axiom, we formulate a base theory for the Reverse Mathematics of Nonstandard Analysis and prove some natural reversals, and show that most of these equivalences do not hold in the absence of parameter-free Transfer.

math.LO↗

arXiv2018

Some nonstandard equivalences in Reverse Mathematics

Reverse Mathematics (RM) is a program in the foundations of mathematics founded by Friedman and developed extensively by Simpson. The aim of RM is finding the minimal axioms needed to prove a theorem of ordinary (i.e. non-set theoretical) mathematics. In the majority of cases, one also obtains an equivalence between the theorem and its minimal axioms. This equivalence is established in a weak logical system called the base theory; four prominent axioms which boast lots of such equivalences are dubbed mathematically natural by Simpson. In this paper, we show that a number of axioms from Nonstandard Analysis are equivalent to theorems of ordinary mathematics not involving Nonstandard Analysis. These equivalences are proved in a weak base theory recently introduced by van den Berg and the author. In particular, our base theories have the first-order strength of elementary function arithmetic, in contrast to the original version of this paper [22]. Our results combined with Simpson's criterion for naturalness suggest the controversial point that Nonstandard Analysis is actually mathematically natural.

math.LO↗

arXiv2018

A footnote to The crisis in contemporary mathematics

We examine the preparation and context of the paper "The Crisis in Contemporary Mathematics" by Errett Bishop, published 1975 in Historia Mathematica. Bishop tried to moderate the differences between Hilbert and Brouwer with respect to the interpretation of logical connectives and quantifiers. He also commented on Robinson's Non-standard Analysis, fearing that it might lead to what he referred to as 'a debasement of meaning.' The 'debasement' comment can already be found in a draft version of Bishop's lecture, but not in the audio file of the actual lecture of 1974. We elucidate the context of the 'debasement' comment and its relation to Bishop's position vis-a-vis the Law of Excluded Middle. Keywords: Constructive mathematics; Robinson's framework; infinitesimal analysis.

math.HO↗

arXiv2017

Grilliot's trick in Nonstandard Analysis

The technique known as Grilliot's trick constitutes a template for explicitly defining the Turing jump functional $(\exists^2)$ in terms of a given effectively discontinuous type two functional. In this paper, we discuss the standard extensionality trick: a technique similar to Grilliot's trick in Nonstandard Analysis. This nonstandard trick proceeds by deriving from the existence of certain nonstandard discontinuous functionals, the Transfer principle from Nonstandard analysis limited to $Π_1^0$-formulas; from this (generally ineffective) implication, we obtain an effective implication expressing the Turing jump functional in terms of a discontinuous functional (and no longer involving Nonstandard Analysis). The advantage of our nonstandard approach is that one obtains effective content without paying attention to effective content. We also discuss a new class of functionals which all seem to fall outside the established categories. These functionals directly derive from the Standard Part axiom of Nonstandard Analysis.

cs.LO↗

arXiv2017

To be or not to be constructive, that is not the question

In the early twentieth century, L.E.J. Brouwer pioneered a new philosophy of mathematics, called intuitionism. Intuitionism was revolutionary in many respects but stands out -mathematically speaking- for its challenge of Hilbert's formalist philosophy of mathematics and rejection of the law of excluded middle from the 'classical' logic used in mainstream mathematics. Out of intuitionism grew intuitionistic logic and the associated Brouwer-Heyting-Kolmogorov interpretation by which 'there exists x' intuitively means 'an algorithm to compute x is given'. A number of schools of constructive mathematics were developed, inspired by Brouwer's intuitionism and invariably based on intuitionistic logic, but with varying interpretations of what constitutes an algorithm. This paper deals with the dichotomy between constructive and non-constructive mathematics, or rather the absence of such an 'excluded middle'. In particular, we challenge the 'binary' view that mathematics is either constructive or not. To this end, we identify a part of classical mathematics, namely classical Nonstandard Analysis, and show it inhabits the twilight-zone between the constructive and non-constructive. Intuitively, the predicate 'x is standard' typical of Nonstandard Analysis can be interpreted as 'x is computable', giving rise to computable (and sometimes constructive) mathematics obtained directly from classical Nonstandard Analysis. Our results formalise Osswald's longstanding conjecture that classical Nonstandard Analysis is locally constructive. Finally, an alternative explanation of our results is provided by Brouwer's thesis that logic depends upon mathematics.

math.LO↗

arXiv2017

Nonstandard Analysis and Constructivism!

Almost two decades ago, Wattenberg published a paper with the title 'Nonstandard Analysis and Constructivism?' in which he speculates on a possible connection between Nonstandard Analysis and constructive mathematics. We study Wattenberg's work in light of recent research on the aforementioned connection. On one hand, with only slight modification, some of Wattenberg's theorems in Nonstandard Analysis are seen to yield effective and constructive theorems (not involving Nonstandard Analysis). On the other hand, we establish the incorrectness of some of Wattenberg's (explicit and implicit) claims regarding the constructive status of the axioms Transfer and Standard Part of Nonstandard Analysis.

math.LO↗