In this paper, we discuss uniform versions of some axioms of second order arithmetic in the context of higher order arithmetic. We prove that uniform versions of weak weak König's lemma WWKL and Σ01 separation are equivalent to over a suitable base theory of higher order arithmetic, where is the assertion that there exists Φ2 such that Φf1 = 0 if and only if ∃x0 for all f. We also prove that uniform versions of some well-known theorems are equivalent to (...) or the axiom of the existence of the Suslin operator. (shrink)

A very weak omniscience principle is formulated, related omniscience principlesare considered, and the theorem that a function of bounded variation is the difference of two increasing functions is shown to be equivalent to the omniscience principle WLPO. It is a so shown that an arbitrary function with located variation on an interval is the difference of two increasing functions.

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. (shrink)

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. [Formula: see text] as “almost finite”, while the latter allows one to treat uncountable sets like e.g. [Formula: see text] (...) 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 hierarchy. We also show that the Cousin lemma is essential for the development of the gauge integral, a generalization of the Lebesgue and improper Riemann integrals that also uniquely provides a direct formalization of Feynman’s path integral. (shrink)

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 ${\mathsf {NIN}}$ (resp. ${\mathsf {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 ${\mathsf {NIN}}$ and ${\mathsf {NBI}}$ are hard to prove in terms of (conventional) comprehension axioms, (...) while many basic theorems, like Arzelà’s convergence theorem for the Riemann integral (1885), are shown to imply ${\mathsf {NIN}}$ and/or ${\mathsf {NBI}}$. Working in Kleene’s higher-order computability theory based on S1–S9, we show that the following fourth-order process based on ${\mathsf {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. (shrink)

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. A basic property of Cantor space$2^ $ is Heine–Borel compactness: for any open covering of $2^ $, there is a finite subcovering. A natural question is: How hard is it to compute such a finite subcovering? We make this precise by analysing the complexity of so-called fan functionals that given any $G:2^ \to $, output a (...) finite sequence $\langle f_0, \ldots,f_n \rangle $ in $2^ $ such that the neighbourhoods defined from $\overline {f_i } G\left$ for $i \le n$ form a covering of $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 analyse the strength of this nonstandard compactness property of Cantor space, compared to the other axioms of Nonstandard Analysis and usual mathematics.Our study of yields exotic objects in computability theory, while leads to surprising results in Reverse Mathematics. We stress that and are highly intertwined, i.e., our study is holistic in nature in that results in computability theory yield results in Nonstandard Analysis and vice versa. (shrink)

The Jordan decomposition theorem states that every function $f \colon \, [0,1] \to \mathbb {R}$ of bounded variation can be written as the difference of two non-decreasing functions. Combining this fact with a result of Lebesgue, every function of bounded variation is differentiable almost everywhere in the sense of Lebesgue measure. We analyze the strength of these theorems in the setting of reverse mathematics. Over $\mathsf {RCA}_{0}$, a stronger version of Jordan’s result where all functions are continuous is equivalent to (...) $\mathsf {ACA}_0$, while the version stated is equivalent to ${\textsf {WKL}}_{0}$. The result that every function on $[0,1]$ of bounded variation is almost everywhere differentiable is equivalent to ${\textsf {WWKL}}_{0}$. To state this equivalence in a meaningful way, we develop a theory of Martin–Löf randomness over $\mathsf {RCA}_0$. (shrink)

We initiate the reverse mathematics of general topology. We show that a certain metrization theorem is equivalent to Π2 1 comprehension. An MF space is defined to be a topological space of the form MF(P) with the topology generated by $\lbrace N_p \mid p \in P \rbrace$ . Here P is a poset, MF(P) is the set of maximal filters on P, and $N_p = \lbrace F \in MF(P) \mid p \in F \rbrace$ . If the poset P is countable, (...) the space MF(P) is said to be countably based. The class of countably based MF spaces can be defined and discussed within the subsystem ACA0 of second order arithmetic. One can prove within ACA0 that every complete separable metric space is homeomorphic to a countably based MF space which is regular. We show that the converse statement, "every countably based MF space which is regular is homeomorphic to a complete separable metric space," is equivalent to Π2 1-CA0. The equivalence is proved in the weaker system Π1 1-CA0. This is the first example of a theorem of core mathematics which is provable in second order arithmetic and implies Π2 1 comprehension. (shrink)

We present a list of open questions in reverse mathematics, including some relevant background information for each question. We also mention some of the areas of reverse mathematics that are starting to be developed and where interesting open question may be found.

A statement of hyperarithmetic analysis is a sentence of second order arithmetic S such that for every Y⊆ω, the minimum ω-model containing Y of RCA0 + S is HYP, the ω-model consisting of the sets hyperarithmetic in Y. We provide an example of a mathematical theorem which is a statement of hyperarithmetic analysis. This statement, that we call INDEC, is due to Jullien [13]. To the author's knowledge, no other already published, purely mathematical statement has been found with this property (...) until now. We also prove that, over RCA0, INDEC is implied by [Formula: see text] and implies ACA0, but of course, neither ACA0, nor ACA 0+ imply it. We introduce five other statements of hyperarithmetic analysis and study the relations among them. Four of them are related to finitely-terminating games. The fifth one, related to iterations of the Turing jump, is strictly weaker than all the other statements that we study in this paper, as we prove using Steel's method of forcing with tagged trees. (shrink)

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 $\Pi^1_2$ sentence of a certain form is provable using E-HA ${}^\omega$ 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 Dialectica interpretation. (...) These results allow us to use techniques of classical reverse mathematics to demonstrate the unprovability of several mathematical principles in subsystems of constructive analysis. (shrink)

Kierstead showed that every computable marriage problem has a computable matching under the assumption of computable expanding Hall condition and computable local finiteness for boys and girls. The strength of the marriage theorem reaches or if computable expanding Hall condition or computable local finiteness for girls is weakened. In contrast, the provability of the marriage theorem is maintained in even if local finiteness for boys is completely removed. Using these conditions, we classify the strength of variants of marriage theorems in (...) the context of reverse mathematics. Furthermore, we introduce another condition that also makes the marriage theorem provable in, and investigate the sequential and Weihrauch strength of marriage theorems under that condition. (shrink)

Pursuing the proof-theoretic program of Friedman and Simpson, we begin the study of the metamathematics of countable linear orderings by proving two main results. Over the weak base system consisting of arithmetic comprehension, II 1 1 -CA0 is equivalent to Hausdorff's theorem concerning the canonical decomposition of countable linear orderings into a sum over a dense or singleton set of scattered linear orderings. Over the same base system, ATR0 is equivalent to a version of the Continuum Hypothesis for linear orderings, (...) which states that every countable linear ordering either has countably many or continuum many Dedekind cuts. (shrink)

This paper gives a formalization of general topology in second-order arithmetic using countably based MF spaces. This formalization is used to study the reverse mathematics of general topology. For each poset P we let MF denote the set of maximal filters on P endowed with the topology generated by {Np | p ∈ P}, where Np = {F ∈ MF | p ∈ F}. We define a countably based MF space to be a space of the form MF for some (...) countable poset P. The class of countably based MF spaces includes all complete separable metric spaces as well as many nonmetrizable spaces. The following reverse mathematics results are obtained. The proposition that every nonempty Gδ subset of a countably based MF space is homeomorphic to a countably based MF space is equivalent to [Formula: see text] over ACA0. The proposition that every uncountable closed subset of a countably based MF space contains a perfect set is equivalent over [Formula: see text] to the proposition that [Formula: see text] is countable for all A ⊆ ℕ. The proposition that every regular countably based MF space is homeomorphic to a complete separable metric space is equivalent to [Formula: see text] over [Formula: see text]. (shrink)

It is shown constructively that a strongly extensional function of bounded variation on an interval is regulated, in a sequential sense that is classically equivalent to the usual one.