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$.
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 $\mathsf{WKL}_0$; (ii) Cousin's lemma for Baire class 1 functions is equivalent to $\mathsf{ACA}_0$; (iii) Cousin's lemma for Baire class 2 functions, or for Borel functions, are both equivalent to $…
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/coun…
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 analyse in the framework of constructive mathematics (BISH) the validity of Farkas' lemma and related propositions, namely the Fredholm alternative for solvability of systems of linear equations, optimality criteria in linear programming, Stiemke's lemma and the Superhedging Duality from mathematical finance, and von Neumann's minimax theorem with application to constructive game theory.
The paper is devoted to a reverse-mathematical study of some well-known consequences of Ramsey's theorem for pairs, focused on the chain-antichain principle $\mathsf{CAC}$, the ascending-descending sequence principle $\mathsf{ADS}$, and the Cohesive Ramsey Theorem for pairs $\mathsf{CRT}^2_2$. We study these principles over the base theory $\mathsf{RCA}^*_0$, which is weaker than the usual base theory $\mathsf{RCA}_0$ considered in reverse mathematics in that it allows only $Δ^0_1$-induction as opposed to $Σ^0_1$-induction. In $\mathsf{RCA}^*_0$, it may happen that an unbounded subset of $\mat…
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$.
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…
Using Sperner's lemma for modified partition of a simplex we will constructively prove the existence of a Nash equilibrium in a finite strategic game with sequentially locally non-constant payoff functions. We follow the Bishop style constructive mathematics.
In Reverse Mathematics, the axiom system DNR, asserting the existence of diagonally non-recursive functions, is strictly weaker than WWKL$_0$ (weak weak König's Lemma).
We analyze the pointwise convergence of a sequence of computable elements of L^1(2^omega) in terms of algorithmic randomness. We consider two ways of expressing the dominated convergence theorem and show that, over the base theory RCA_0, each is equivalent to the assertion that every G_delta subset of Cantor space with positive measure has an element. This last statement is, in turn, equivalent to weak weak König's lemma relativized to the Turing jump of any set. It is also equivalent to the conjunction of the statement asserting the existence of a 2-random relative to any given set and the pr…
We study the reverse mathematics of the principle stating that, for every property of finite character, every set has a maximal subset satisfying the property. In the context of set theory, this variant of Tukey's lemma is equivalent to the axiom of choice. We study its behavior in the context of second-order arithmetic, where it applies to sets of natural numbers only, and give a full characterization of its strength in terms of the quantifier structure of the formula defining the property. We then study the interaction between properties of finite character and finitary closure operators, an…
The Erdos-Moser theorem (EM) states that every infinite tournament has an infinite transitive subtournament. This principle plays an important role in the understanding of the computational strength of Ramsey's theorem for pairs (RT^2_2) by providing an alternate proof of RT^2_2 in terms of EM and the ascending descending sequence principle (ADS). In this paper, we study the computational weakness of EM and construct a standard model (omega-model) of simultaneously EM, weak König's lemma and the cohesiveness principle, which is not a model of the atomic model theorem. This separation answers a…
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…
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…
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) p…
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, a…
