Searcharxiv⌕ Search

arXiv subjects

Sam Sanders

Publications and source records attributed to Sam Sanders.

At least 37 records · Page 2Linked to original sources
arXiv2023

The Biggest Five of Reverse Mathematics

The aim of Reverse Mathematics(RM for short)is to find the minimal axioms needed to prove a given theorem of ordinary mathematics. These minimal axioms are almost always equivalent to the theorem, working over the base theory of RM, a weak system of computable mathematics. The Big Five phenomenon of RM is the observation that a large number of theorems from ordinary mathematics are either provable in the base theory or equivalent to one of only four systems; these five systems together are called the 'Big Five'. The aim of this paper is to greatly extend the Big Five phenomenon as follows: there are two supposedly fundamentally different approaches to RM where the main difference is whether the language is restricted to second-order objects or if one allows third-order objects. In this paper, we unite these two strands of RM by establishing numerous equivalences involving the second-order Big Five systems on one hand, and well-known third-order theorems from analysis about (possibly) discontinuous functions on the other hand. We both study relatively tame notions, like cadlag or Baire 1, and potentially wild ones, like quasi-continuity. We also show that slight generalisations and variations of the aforementioned third-order theorems fall far outside of the Big Five.

math.LO↗
arXiv2023

Big in Reverse Mathematics: the uncountability of the real numbers

The uncountability of $\mathbb{R}$ is one of its most basic properties, known far outside of mathematics. Cantor's 1874 proof of the uncountability of $\mathbb{R}$ even appears in the very first paper on set theory, i.e. a historical milestone. In this paper, we study the uncountability of $\mathbb{R}$ in Kohlenbach's higher-order Reverse Mathematics (RM for short), in the guise of the following principle: $$\hbox{for a countable set $A\subset \mathbb{R}$, there exists $y\in \mathbb{R}\setminus A$.}$$ An important conceptual observation is that the usual definition of countable set -- based on injections or bijections to $\mathbb{N}$ -- does not seem suitable for the RM-study of mainstream mathematics; we also propose a suitable (equivalent over strong systems) alternative definition of countable set, namely union over $\mathbb{N}$ of finite sets; the latter is known from the literature and closer to how countable sets occur 'in the wild'. We identify a considerable number of theorems that are equivalent to the centred theorem based on our alternative definition. Perhaps surprisingly, our equivalent theorems involve most basic properties of the Riemann integral, regulated or bounded variation functions, Blumberg's theorem, and Volterra's early work circa 1881. Our equivalences are also robust, promoting the uncountability of $\mathbb{R}$ to the status of 'big' system in RM.

math.LO↗
arXiv2023

Historical infinitesimalists and modern historiography of infinitesimals

In the history of infinitesimal calculus, we trace innovation from Leibniz to Cauchy and reaction from Berkeley to Mansion and beyond. We explore 19th century infinitesimal lores, including the approaches of Simeon-Denis Poisson, Gaspard-Gustave de Coriolis, and Jean-Nicolas Noel. We examine contrasting historiographic approaches to such lores, in the work of Laugwitz, Schubring, Spalt, and others, and address a recent critique by Archibald et al. We argue that the element of contingency in this history is more prominent than many modern historians seem willing to acknowledge.

math.HO↗
arXiv2023

The non-normal abyss in Kleene's computability theory

Kleene's computability theory based on his S1-S9 computation schemes constitutes a model for computing with objects of any finite type and extends Turing's `machine model' which formalises computing with real numbers. A fundamental distinction in Kleene's framework is between normal and non-normal functionals where the former compute the associated Kleene quantifier $\exists^{n}$ and the latter do not. Historically, the focus was on normal functionals, but recently new non-normal functionals have been studied, based on well-known theorems like the uncountability of the reals. These new non-normal functionals are fundamentally different from historical examples like Tait's fan functional: the latter is computable from $\exists^{2}$ while the former are only computable in $\exists^{3}$. While there is a great divide separating $\exists^{2}$ and $\exists^{3}$, we identify certain closely related non-normal functionals that fall on different sides of this abyss. Our examples are based on mainstream mathematical notions, like quasi-continuity, Baire classes, and semi-continuity.

math.LO↗
arXiv2022

On the computational properties of the Baire Category Theorem

Computability theory is a discipline in the intersection of computer science and mathematical logic where the fundamental question is: given two mathematical objects X and Y, does X compute Y in principle? In case X and Y are real numbers, Turing's famous 'machine' model provides the standard interpretation of 'computation' for this question. To formalise computation involving (total) abstract objects, Kleene introduced his S1-S9 computation schemes. In turn, Dag Normann and the author have introduced a version of the lambda calculus involving fixed point operators that exactly captures S1-S9 and accommodates partial objects. In this paper, we use this new model to develop the computability theory of various well-known theorems due to Baire and Volterra and related results; these theorems only require basic mathematical notions like continuity, open sets, and density. We show that these theorems due to Baire and Volterra are computationally equivalent from the point of view of our new model, sometimes working in rather tame fragments of Goedel's T.

math.LO↗
arXiv2022

On robust theorems due to Bolzano, Weierstrass, Cantor, and Jordan

Reverse Mathematics (RM hereafter) is a program in the foundations of mathematics where the aim is to identify the minimal axioms needed to prove a given theorem from ordinary, i.e. non-set theoretic, mathematics. This program has unveiled surprising regularities: the minimal axioms are very often equivalent to the theorem over the base theory, a weak system of 'computable mathematics', while most theorems are either provable in this base theory, or equivalent to one of only four logical systems. The latter plus the base theory are called the 'Big Five' and the associated equivalences are robust following Montalban, i.e. stable under small variations of the theorems at hand. Working in Kohlenbach's higher-order RM, we obtain two long series of equivalences based on theorems due to Bolzano, Weierstrass, Jordan, and Cantor; these equivalences are extremely robust and have no counterpart among the Big Five systems, as they are strictly between the base theory and the higher-order counterpart of weak Koenig's lemma. Thus, higher-order RM is much richer than its second-order cousin, boasting (at least) two extra 'Big' systems.

math.LO↗
arXiv2022

On the computational properties of the uncountability of the real numbers

The uncountability of the real numbers is one of their most basic properties, known (far) outside of mathematics. Cantor's 1874 proof of the uncountability of the real numbers even appears in the very first paper on set theory, i.e. a historical milestone. Despite this famous status and history, the computational properties of the uncountability of the real numbers have not been studied much. In this paper, we study the following computational operation that witnesses that the real numbers not countable: on input a countable set of reals, output a real not in that set. In particular, we formulate a considerable number of operations that are computationally equivalent to the centred operation, working in Kleene's higher-order computability theory based on his S1-S9 computation schemes. Perhaps surprisingly, our equivalent operations involve most basic properties of the Riemann integral and Volterra's early work circa 1881.

math.LO↗
arXiv2022

Reverse Mathematics of the uncountability of $\mathbb{R}$

In his first set theory paper (1874), Cantor establishes the uncountability of $\mathbb{R}$. We study the latter in Kohlenbach's higher-order Reverse Mathematics, motivated by the observation that one cannot study concepts like `arbitrary mappings from $\mathbb{R}$ to $\mathbb{N}$' in second-order Reverse Mathematics. Now, it was recently shown that the following statement: $$ \text{ NIN: there is no injection from $[0,1]$ to $\mathbb{N}$,} $$ is hard to prove in terms of conventional comprehension. In this paper, we show that NIN is robust by establishing equivalences between NIN and NIN restricted to mainstream function classes, like: bounded variation, semi-continuity, and Borel. Thus, the aforementioned hardness of NIN is not due to the quantification over arbitrary $\mathbb{R}\rightarrow \mathbb{N}$-functions in NIN. Finally, we also study NBI, the restriction of NIN to bijections, and the connection to Cousin's lemma and Jordan's decomposition theorem.

math.LO↗
arXiv2022

On the logical and computational properties of the Vitali covering theorem

We study a version of the Vitali covering theorem, which we call $\textsf{WHBU}$ and which is a direct weakening of the Heine-Borel theorem for uncountable coverings, called $\textsf{HBU}$. We show that $\textsf{WHBU}$ is central to measure theory by deriving it from various central approximation results related to Littlewood's three principles. A natural question is then how hard it is to prove $\textsf{WHBU}$ (in the sense of Kohlenbach's higher-order Reverse Mathematics}), and how hard it is to compute the objects claimed to exist by $\textsf{WHBU}$ (in the sense of Kleene's schemes S1-S9). The answer to both questions is `extremely hard', as follows: on one hand, in terms of the usual scale of (conventional) comprehension axioms, $\textsf{WHBU}$ is only provable using Kleene's $\exists^{3}$, which implies full second-order arithmetic. On the other hand, realisers (aka witnessing functionals) for $\textsf{WHBU}$, so-called $Λ$-functionals, are computable from Kleene's $\exists^{3}$, but not from weaker comprehension functionals. Despite this hardness, we show that $\textsf{WHBU}$, and certain $Λ$-functionals, behave much better than $\textsf{HBU}$ and the associated class of realisers, called $Θ$-functionals. In particular, we identify a specific $Λ$-functional called $Λ_{\textsf{S}}$ which adds no computational power to the Suslin functional $\textsf{S}^2$, in contrast to $Θ$-functionals. Finally, we introduce a hierarchy involving $Θ$-functionals and $\textsf{HBU}$.

math.LO↗
arXiv2022

On the uncountability of $\mathbb{R}$

Cantor's first set theory paper (1874) establishes the uncountability of $\mathbb{R}$. We study this most basic mathematical fact formulated in the language of higher-order arithmetic. In particular, we investigate the logical and computational properties of NIN (resp. NBI), i.e. the third-order statement: there is no injection (resp. bijection) from $[0,1]$ to $\mathbb{N}$. Working in Kohlenbach's higher-order Reverse Mathematics, we show that NIN and NBI are hard to prove in terms of (conventional) comprehension axioms, while many basic theorems, like Arzela's convergence theorem for the Riemann integral (1885), are shown to imply NIN and/or NBI. Working in Kleene's higher-order computability theory based on S1-S9, we show that the following fourth-order process based on NIN is similarly hard to compute: for a given $[0,1]\rightarrow \mathbb{N}$-function, find reals in the unit interval that map to the same natural number.

math.LO↗
arXiv2021

Between Turing and Kleene

Turing's famous `machine' model constitutes the first intuitively convincing framework for computing with real numbers. Kleene's computation schemes S1-S9 extend Turing's approach to computing with objects of any finite type. Both frameworks have their pros and cons and it is a natural question if there is an approach that marries the best of both the Turing and Kleene worlds. In answer to this question, we propose a considerable extension of the scope of Turing's approach. Central is a fragment of the Axiom of Choice involving continuous choice functions, going back to Kreisel-Troelstra and intuitionistic analysis. Put another way, we formulate a relation `is computationally stronger than' involving third-order objects that overcomes (many of) the pitfalls of the Turing and Kleene frameworks.

math.LO↗
arXiv2021

Betwixt Turing and Kleene

Turing's famous 'machine' model constitutes the first intuitively convincing framework for computing with real numbers. Kleene's computation schemes S1-S9 extend Turing's approach and provide a framework for computing with objects of any finite type. Various research programs have been proposed in which higher-order objects, like functions on the real numbers, are represented/coded as real numbers, so as to make them amenable to the Turing framework. It is then a natural question whether there is any significant difference between the Kleene approach or the Turing-approach-via-codes. Continuous functions being well-studied in this context, we study functions of bounded variation, which have at most countably many points of discontinuity. A central result is the Jordan decomposition theorem that a function of bounded variation on $[0, 1]$ equals the difference of two monotone functions. We show that for this theorem and related results, the difference between the Kleene approach and the Turing-approach-via-codes is huge, in that full second-order arithmetic readily comes to the fore in Kleenes approach, in the guise of Kleene's quantifier $\exists^3$.

math.LO↗
arXiv2021

Countable sets versus sets that are countable in Reverse Mathematics

The program Reverse Mathematics (RM for short) seeks to identify the axioms necessary to prove theorems of ordinary mathematics, usually working in the language of second-order arithmetic $L_{2}$. A major theme in RM is therefore the study of structures that are countable or can be approximated by countable sets. Now, countable sets are represented by sequences here, because the usual higher-order definition of `countable set'cannot be expressed in $L_{2}$. Working in Kohlenbach's higher-order RM, we investigate various central theorems, e.g. those due to König, Ramsey, Bolzano, Weierstrass, and Borel, in their (often original) formulation involving the usual definition(s) of `countable set' instead of `sequence'. This study turns out to be closely related to the logical properties of the uncountably of $\mathbb{R}$, recently developed by the author and Dag Normann. Now, `being countable' can be expressed by the existence of an injection to $\mathbb{N}$ (Kunen) or the existence of a bijection to $\mathbb{N}$ (Hrbacek-Jech). The former (and not the latter) choice yields `explosive' theorems, i.e. relatively weak statements that become much stronger when combined with discontinuous functionals, even up to $Π_2^1$-CA$_0$. Nonetheless, replacing `sequence' by `countable set' seriously reduces the first-order strength of these theorems, whatever the notion of `set' used. Finally, we obtain `splittings' involving e.g. lemmas by König and theorems from the RM zoo, showing that the latter are `a lot more tame' when formulated with countable sets.

math.LO↗
arXiv2021

Representations and the foundations of mathematics

The representation of mathematical objects in terms of (more) basic ones is part and parcel of (the foundations of) mathematics. In the usual foundations of mathematics, i.e. $\textsf{ZFC}$ set theory, all mathematical objects are represented by sets, while ordinary, i.e. non-set theoretic, mathematics is represented in the more parsimonious language of second-order arithmetic. This paper deals with the latter representation for the rather basic case of continuous functions on the reals and Baire space. We show that the logical strength of basic theorems named after Tietze, Heine, and Weierstrass, changes significantly upon the replacement of 'second-order representations' to 'third-order functions'. We discuss the implications and connections to the Reverse Mathematics program and its foundational claims regarding predicativist mathematics and Hilbert's program for the foundations of mathematics. Finally, we identify the problem caused by representations of continuous functions and formulate a criterion to avoid problematic codings within the bigger picture of representations.

math.LO↗
arXiv2021

Splittings and robustness for the Heine-Borel theorem

The Heine-Borel theorem for uncountable coverings has recently emerged as an interesting and central principle in higher-order Reverse Mathematics and computability theory, formulated as follows: HBU is the Heine-Borel theorem for uncountable coverings given as $\cup_{x\in [0,1]}(x-Ψ(x), x+Ψ(x))$ for arbitrary $Ψ:[0,1]\rightarrow \mathbb{R}^{+}$, i.e. the original formulation going back to Cousin (1895) and Lindelöf (1903). In this paper, we show that HBU is equivalent to its restriction to functions continuous almost everywhere, an elegant robustness result. We also obtain a nice splitting HBU $\leftrightarrow$ [WHBU$^{+}$+HBC$_{0}$ + WKL$_0]$ where WHBU$^{+}$ is a strengthening of Vitali's covering theorem and where HBC$_{0}$ is the Heine-Borel theorem for countable collections (and \textbf{not sequences}) of basic open intervals, as formulated by Borel himself in 1898.

math.LO↗
arXiv2020

The unreasonable effectiveness of Nonstandard Analysis

As suggested by the title, the aim of this paper is to uncover the vast computational content of classical Nonstandard Analysis. To this end, we formulate a template $\mathfrak{CI}$ which converts a theorem of 'pure' Nonstandard Analysis, i.e. formulated solely with the nonstandard definitions (of continuity, integration, differentiability, convergence, compactness, et cetera), into the associated effective theorem. The latter constitutes a theorem of computable mathematics no longer involving Nonstandard Analysis. To establish the vast scope of $\mathfrak{CI}$, we apply this template to representative theorems from the Big Five categories from Reverse Mathematics. The latter foundational program provides a classification of the majority of theorems from 'ordinary', that is non-set theoretical, mathematics into the aforementioned five categories. The Reverse Mathematics zoo gathers exceptions to this classification, and is studied in [70,71] using $\mathfrak{CI}$. Hence, the template $\mathfrak{CI}$ is seen to apply to essentially all of ordinary mathematics, thanks to the Big Five classification (and associated zoo) from Reverse Mathematics. Finally, we establish that certain 'highly constructive' theorems, called Herbrandisations, imply the original theorem of Nonstandard Analysis from which they were obtained via $\mathfrak{CI}$.

math.LO↗
arXiv2020

The Axiom of Choice in Computability Theory and Reverse Mathematics, with a cameo for the Continuum Hypothesis

The Axiom of Choice (AC for short) is the most (in)famous axiom of the usual foundations of mathematics, ZFC set theory. The (non-)essential use of AC in mathematics has been well-studied and thoroughly classified. Now, fragments of countable AC not provable in ZF have recently been used in Kohlenbach's higher-order Reverse Mathematics to obtain equivalences between closely related compactness and local-global principles. We continue this study and show that NCC, a weak choice principle provable in ZF and much weaker systems, suffices for many of these results. In light of the intimate connection between Reverse Mathematics and computability theory, we also study realisers for NCC, i.e. functionals that produce the choice functions claimed to exist by the latter from the other data. Our hubris of undertaking the hitherto underdeveloped study of the computational properties of (choice functions from) AC leads to interesting results. For instance, using Kleene's S1-S9 computation schemes, we show that various total realisers for NCC compute Kleene's $\exists^3$, a functional that gives rise to full second-order arithmetic, and vice versa. By contrast, partial realisers for NCC should be much weaker, but establishing this conjecture remains elusive. By way of catharsis, we show that the Continuum Hypothesis (CH for short) is equivalent to the existence of a countably based partial realiser for NCC. The latter kind of realiser does not compute Kleene's $\exists^3$ and is therefore strictly weaker than a total one.

math.LO↗