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.
The coarse similarity class $[A]$ of $A$ is the set of all $B$ whose symmetric difference with $A$ has asymptotic density 0. There is a natural metric $δ$ on the space $\mathcal{S}$ of coarse similarity classes defined by letting $δ([A],[B])$ be the upper density of the symmetric difference of $A$ and $B$. We study the resulting metric space, showing in particular that between any two distinct points there are continuum many geodesic paths. We also study subspaces of the form $\{[A] : A \in \mathcal U\}$ where $\mathcal U$ is closed under Turing equivalence, and show that there is a tight conn…
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 Pi…
A set $X \subseteq 2^ω$ with positive measure contains a perfect subset. We study such perfect subsets from the viewpoint of computability and prove that these sets can have weak computational strength. Then we connect the existence of perfect subsets of sets with positive measure with reverse mathematics.
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 connect…
Ramsey's theorem states that each coloring has an infinite homogeneous set, but these sets can be arbitrarily spread out. Paul Erdos and Fred Galvin proved that for each coloring f, there is an infinite set that is "packed together" which is given "a small number" of colors by f. We analyze the strength of this theorem from the perspective of computability theory and reverse mathematics. We show that this theorem is close in computational strength to standard Ramsey's theorem by giving arithmetical upper and lower bounds for solutions to computable instances. In reverse mathematics, we show th…
We identify computability-theoretic properties enabling us to separate various statements about partial orders in reverse mathematics. We obtain simpler proofs of existing separations, and deduce new compound ones. This work is part of a larger program of unification of the separation proofs of various Ramsey-type theorems in reverse mathematics in order to obtain a better understanding of the combinatorics of Ramsey's theorem and its consequences. We also answer a question of Murakami, Yamazaki and Yokoyama about pseudo Ramsey's theorem for pairs.
Matroids generalize the familiar notion of linear dependence from linear algebra. Following a brief discussion of founding work in computability and matroids, we use the techniques of reverse mathematics to determine the logical strength of some basis theorems for matroids and enumerated matroids. Next, using Weihrauch reducibility, we relate the basis results to combinatorial choice principles and statements about vector spaces. Finally, we formalize some of the Weihrauch reductions to extract related reverse mathematics results. In particular, we show that the existence of bases for vector s…
We study the computational content of various theorems with reverse mathematical strength around Arithmetical Transfinite Recursion ($\mathsf{ATR}_0$) from the point of view of computability-theoretic reducibilities, in particular Weihrauch reducibility. Our first main result states that it is equally hard to construct an embedding between two given well-orderings, as it is to construct a Turing jump hierarchy on a given well-ordering. This answers a question of Marcone. We obtain a similar result for Fraïssé's conjecture restricted to well-orderings. We then turn our attention to König's dual…
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 an…
We explore in the framework of Quantum Computation the notion of {\em Computability}, which holds a central position in Mathematics and Theoretical Computer Science. A quantum algorithm for Hilbert's tenth problem, which is equivalent to the Turing halting problem and is known to be mathematically noncomputable, is proposed where quantum continuous variables and quantum adiabatic evolution are employed. If this algorithm could be physically implemented, as much as it is valid in principle--that is, if certain hamiltonian and its ground state can be physically constructed according to the propo…
We extend theories of reverse mathematics by a non-principal ultrafilter, and show that these are conservative extensions of the usual theories ACA0, ATR0, and Pi11-Comprehension.
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 …
We extend a study by Lempp and Hirst of infinite versions of some problems from finite complexity theory, using an intuitionistic version of reverse mathematics and techniques of Weihrauch analysis.
We examine a number of results of infinite combinatorics using the techniques of reverse mathematics. Our results are inspired by similar results in recursive combinatorics. Theorems included concern colorings of graphs and bounded graphs, Euler paths, and Hamilton paths.
No natural principle is currently known to be strictly between the arithmetic comprehension axiom (ACA) and Ramsey's theorem for pairs (RT^2_2) in reverse mathematics. The tree theorem for pairs (TT^2_2) is however a good candidate. The tree theorem states that for every finite coloring over tuples of comparable nodes in the full binary tree, there is a monochromatic subtree isomorphic to the full tree. The principle TT^2_2 is known to lie between ACA and RT^2_2 over RCA, but its exact strength remains open. In this paper, we prove that RT^2_2 together with weak König's lemma (WKL) does not im…
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 Nons…
We prove that several versions of the Tietze extension theorem for functions with moduli of uniform continuity are equivalent to WKL_0 over RCA_0. This confirms a conjecture of Giusto and Simpson that was also phrased as a question in Montalbán's "Open questions in reverse mathematics."
It is a striking fact from reverse mathematics that almost all theorems of countable and countably representable mathematics are equivalent to just five subsystems of second order arithmetic. The standard view is that the significance of these equivalences lies in the set existence principles that are necessary and sufficient to prove those theorems. In this article I analyse the role of set existence principles in reverse mathematics, and argue that they are best understood as closure conditions on the powerset of the natural numbers.
Building on previous work by Mummert, Saadaoui and Sovine, we study the logic underlying the web of implications and nonimplications which constitute the so called reverse mathematics zoo. We introduce a tableaux system for this logic and natural deduction systems for important fragments of the language.
The Carlson-Simpson lemma is a combinatorial statement occurring in the proof of the Dual Ramsey theorem. Formulated in terms of variable words, it informally asserts that given any finite coloring of the strings, there is an infinite sequence with infinitely many variables such that for every valuation, some specific set of initial segments is homogeneous. Friedman, Simpson, and Montalban asked about its reverse mathematical strength. We study the computability-theoretic properties and the reverse mathematics of this statement, and relate it to the finite union theorem. In particular, we prov…
Reverse mathematics studies which subsystems of second order arithmetic are equivalent to key theorems of ordinary, non-set-theoretic mathematics. The main philosophical application of reverse mathematics proposed thus far is foundational analysis, which explores the limits of different foundations for mathematics in a formally precise manner. This paper gives a detailed account of the motivations and methodology of foundational analysis, which have heretofore been largely left implicit in the practice. It then shows how this account can be fruitfully applied in the evaluation of major foundat…
In reverse mathematics, is is possible to have a curious situation where we know that an implication does not reverse, but appear to have no information on on how to weaken the assumption while preserving the conclusion. A main cause of this phenomenon is the proof of a $Π^1_2$ sentence from the theory {\Pioo}. Using methods based on the functional interpretation, we introduce a family of weakenings of {\Pioo} and use them to give new upper bounds for the Nash-Williams Theorem of wqo theory and Menger's Theorem for countable graphs.
Working in subsystems of second order arithmetic, we formulate several representations for hypergraphs. We then prove the equivalence of various vertex coloring theorems to ${\sf WKL}_0$, ${\sf ACA}_0$ and $Π^1_ 1$-${\sf CA}_0$.
This paper analyzes theorems about algebraic field extensions using the techniques of reverse mathematics. In section 2, we show that $\mathsf{WKL}_0$ is equivalent to the ability to extend $F$-automorphisms of field extensions to automorphisms of $\bar{F}$, the algebraic closure of $F$. Section 3 explores finitary conditions for embeddability. Normal and Galois extensions are discussed in section 4, and the Galois correspondence theorems for infinite field extensions are treated in section 5.
This paper falls within the general program of investigating the proof theoretic strength (in terms of reverse mathematics) of combinatorial principals which follow from versions of Ramsey's theorem. We examine two statements in graph theory and one statement in lattice theory proved by Galvin, Rival and Sands \cite{GRS:82} using Ramsey's theorem for 4-tuples. Our main results are that the statements concerning graph theory are equivalent to Ramsey's theorem for 4-tuples over $\RCA$ while the statement concerning lattices is provable in $\RCA$. Revised 12/2010. To appear in Archive for Mathema…
We investigate subsystems $COM_{fcn}$, $COMI_{fcn}$ and $PRA_{fcn}$ of the elementary theory of functions $ETF$, the base theory for countable strict reverse mathematics. We show that inductions on any variable for unary, binary and ternary functions are pairwise equivalent over $COM_{fcn}$. We prove that weakened primitive recursion axiom $WPRA$ is equivalent to primitive recursion axiom $PRA$ over $COMI_{fcn}$. We show that permutation axiom and minimization axioms $MIN^1$, $MIN^2$, $MIN^3$ are pairwise equivalent over $PRA_{fcn}$. Thus, we present several equivalent axiomatizations of $ETF$…
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.
We analyze the strength of the existence of idempotent ultrafilters in higher-order reverse mathematics. Let (Uidem) be the statement that an idempotent ultrafilter on the natural numbers exists. We show that over ACA_0^w, the higher-order extension of ACA_0, the statement (Uidem) implies the iterated Hindman's theorem (IHT), and we show that ACA_0^w + (Uidem) is Pi^1_2-conservative over ACA_0^w + IHT and thus over ACA_0^+.
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,…
In his book, John Stillwell wrote "finding the exact strength of the Brouwer invariance theorems seems to me one of the most interesting open problems in reverse mathematics." In this article, we solve Stillwell's problem by showing that (some forms of) the Brouwer invariance theorems are equivalent to weak König's lemma over the base system ${\sf RCA}_0$. In particular, there exists an explicit algorithm which, whenever weak König's lemma is false, constructs a topological embedding of $\mathbb{R}^4$ into $\mathbb{R}^3$.
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 …
In this paper, we propose a weak regularity principle which is similar to both weak König's lemma and Ramsey's theorem. We begin by studying the computational strength of this principle in the context of reverse mathematics. We then analyze different ways of generalizing this principle.
In this paper we investigate the reverse mathematics of higher-order analogues of the theory \ATRz{} within the framework of higher order reverse mathematics developed by Kohlenbach \cite{Koh01}. We define a theory \RCAzthr, a close higher-type analogue of the classical base theory \RCAz, and show that it is essentially a conservative subtheory of Kohlenbach's base theory \RCAzo. Working over \RCAzthr, we study higher-type analogues of statements classically equivalent to \ATRz, including open and clopen determinacy, as well as two choice principles, and prove several equivalences and separati…
The separation between two theorems in reverse mathematics is usually done by constructing a Turing ideal satisfying a theorem P and avoiding the solutions to a fixed instance of a theorem Q. Lerman, Solomon and Towsner introduced a forcing technique for iterating a computable non-reducibility in order to separate theorems over omega-models. In this paper, we present a modularized version of their framework in terms of preservation of hyperimmunity and show that it is powerful enough to obtain the same separations results as Wang did with his notion of preservation of definitions.
In the context of reverse mathematics, effective transfinite recursion refers to a principle that allows us to construct sequences of sets by recursion along arbitrary well orders, provided that each set is $Δ^0_1$-definable relative to the previous stages of the recursion. It is known that this principle is provable in $\mathbf{ACA}_0$. In the present note, we argue that a common formulation of effective transfinite recursion is too restrictive. We then propose a more liberal formulation, which appears very natural and is still provable in $\mathbf{ACA}_0$.
Every function over the natural numbers has an infinite subdomain on which the function is non-decreasing. Motivated by a question of Dzhafarov and Schweber, we study the reverse mathematics of variants of this statement. It turns out that this statement restricted to computably bounded functions is computationally weak and does not imply the existence of the halting set. On the other hand, we prove that it is not a consequence of Ramsey's theorem for pairs. This statement can therefore be seen as an arguably natural principle between the arithmetic comprehension axiom and stable Ramsey's theo…
Satisfiability problems play a central role in computer science and engineering as a general framework for studying the complexity of various problems. Schaefer proved in 1978 that truth satisfaction of propositional formulas given a language of relations is either NP-complete or tractable. We classify the corresponding satisfying assignment construction problems in the framework of reverse mathematics and show that the principles are either provable over RCA or equivalent to WKL. We formulate also a Ramseyan version of the problems and state a different dichotomy theorem. However, the differe…
We show that the well-partial orderedness of the finite downwards closed subsets of $\mathbb{N}^k$ ,ordered by inclusion, is equivalent to the well-foundedness of the ordinal $ω^{ω^ω}$. This was conjectured to be the case by Hatzikiriakou and Simpson. Since we use Friedman's adjacent Ramsey theorem for fixed dimensions in the upper bound, we also give a treatment of the reverse mathematical status of that theorem.
We show that there is a strong connection between Weihrauch reducibility on one hand, and provability in EL_0, the intuitionistic version of RCA_0, on the other hand. More precisely, we show that Weihrauch reducibility to the composition of finitely many instances of a theorem is captured by provability in EL_0 together with Markov's principle, and that Weihrauch reducibility is captured by an affine subsystem of EL_0 plus Markov's principle.
We show that when certain statements are provable in subsystems of constructive analysis using intuitionistic predicate calculus, related sequential statements are provable in weak classical subsystems. In particular, if a $Π^1_2$ sentence of a certain form is provable using E-HA${}^ω$ along with the axiom of choice and an independence of premise principle, the sequential form of the statement is provable in the classical system RCA. We obtain this and similar results using applications of modified realizability and the \textit{Dialectica} interpretation. These results allow us to use techniqu…
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 rest…
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 Nonstan…
Cousin's lemma is a compactness principle that naturally arises when studying the gauge integral, a generalisation of the Lebesgue integral. We study the axiomatic strength of Cousin's lemma for various classes of functions, using Friedman and Simpson's reverse mathematics in second-order arithmetic. We prove that, over $\mathsf{RCA}_0$: (i) Cousin's lemma for continuous functions is equivalent to the system $\mathsf{WKL}_0$; (ii) Cousin's lemma for Baire 1 functions is at least as strong as $\mathsf{ACA}_0$; (iii) Cousin's lemma for Baire 2 functions is at least as strong as $\mathsf{ATR}_0$.
We study the reverse mathematics of the theory of countable second-countable topological spaces, with a focus on compactness. We show that the general theory of such spaces works as expected in the subsystem $\mathsf{ACA}_0$ of second-order arithmetic, but we find that many unexpected pathologies can occur in weaker subsystems. In particular, we show that $\mathsf{RCA}_0$ does not prove that every compact discrete countable second-countable space is finite and that $\mathsf{RCA}_0$ does not prove that the product of two compact countable second-countable spaces is compact. To circumvent these …
In this thesis, we investigate the computational content and the logical strength of Ramsey's theorem and its consequences. For this, we use the frameworks of reverse mathematics and of computable reducibility. We proceed to a systematic study of various Ramsey-type statements under a unified and minimalistic framework and obtain a precise analysis of their interrelations. We clarify the role of the number of colors in Ramsey's theorem. In particular, we show that the hierarchy of Ramsey's theorem induced by the number of colors is strictly increasing over computable reducibility, and exhibit …
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 …
We introduce the notion of τ-like partial order, where τis one of the linear order types ω, ω*, ω+ω*, and ζ. For example, being ω-like means that every element has finitely many predecessors, while being ζ-like means that every interval is finite. We consider statements of the form "any τ-like partial order has a τ-like linear extension" and "any τ-like partial order is embeddable into τ" (when τ is ζ this result appears to be new). Working in the framework of reverse mathematics, we show that these statements are equivalent either to BΣ^0_2 or to ACA_0 over the usual base system RCA_0.
The tree theorem for pairs ($\mathsf{TT}^2_2$), first introduced by Chubb, Hirst, and McNicholl, asserts that given a finite coloring of pairs of comparable nodes in the full binary tree $2^{<ω}$, there is a set of nodes isomorphic to $2^{<ω}$ which is homogeneous for the coloring. This is a generalization of the more familiar Ramsey's theorem for pairs ($\mathsf{RT}^2_2$), which has been studied extensively in computability theory and reverse mathematics. We answer a longstanding open question about the strength of $\mathsf{TT}^2_2$, by showing that this principle does not imply the arithmeti…
