In reverse mathematics, it is possible to have a curious situation where we know that an implication does not reverse, but appear to have no information on how to weaken the assumption while preserving the conclusion (other than reducing all the way to the tautology of assuming the conclusion). A main cause of this phenomenon is the proof of a $\Pi^1_2$ sentence from the theory $\mathbf{\Pi^{\textbf{1}}_{\textbf{1}}-CA_{\textbf{0}}}$. Using methods based on the functional interpretation, we introduce a family of weakenings of $\mathbf{\Pi^{\textbf{1}}_{\textbf{1}}-CA_{\textbf{0}}}$ (...) and use them to give new upper bounds for the Nash-Williams Theorem of wqo theory and Menger's Theorem for countable graphs. (shrink)

Hindman's Theorem is a prototypical example of a combinatorial theorem with a proof that uses the topology of the ultrafilters. We show how the methods of this proof, including topological arguments about ultrafilters, can be translated into second order arithmetic.

We investigate the uniform computational content of the open and clopen Ramsey theorems in the Weihrauch lattice. While they are known to be equivalent to $\mathrm {ATR_0}$ from the point of view of reverse mathematics, there is not a canonical way to phrase them as multivalued functions. We identify eight different multivalued functions and study their degree from the point of view of Weihrauch, strong Weihrauch, and arithmetic Weihrauch reducibility. In particular one of our functions turns out to be strictly (...) stronger than any previously studied multivalued functions arising from statements around $\mathrm {ATR}_0$. (shrink)

We investigate the strength of the existence of a non-principal ultrafilter over fragments of higher-order arithmetic. Let [Formula: see text] be the statement that a non-principal ultrafilter on ℕ exists and let [Formula: see text] be the higher-order extension of ACA0. We show that [Formula: see text] is [Formula: see text]-conservative over [Formula: see text] and thus that [Formula: see text] is conservative over PA. Moreover, we provide a program extraction method and show that from a proof of a strictly (...) [Formula: see text] statement ∀ f ∃ g A qf in [Formula: see text] a realizing term in Gödel's system T can be extracted. This means that one can extract a term t ∈ T, such that ∀ f A qf). (shrink)

We show that a theory of autonomous iterated Ramseyness based on second order arithmetic (SOA) is proof-theoretically equivalent to ${\Pi^1_2}$ -comprehension. The property of Ramsey is defined as follows. Let X be a set of real numbers, i.e. a set of infinite sets of natural numbers. We call a set H of natural numbers homogeneous for X if either all infinite subsets of H are in X or all infinite subsets of H are not in X. X has the property (...) of Ramsey if there exists a set which is homogeneous for X. The property of Ramsey is considered in reverse mathematics to compare the strength of subsystems of SOA. To characterize the system of ${\Pi^1_2}$ -comprehension in terms of Ramseyness we introduce a system of autonomous iterated Ramseyness, called R-calculus. We augment the language of SOA with additional set terms (called R-terms) ${R\vec{x}X\phi(\vec{x},X)}$ for each first order formula ${\phi(\vec{x},X)}$ (where φ may contain further R-terms). The R-calculus is a system which comprises comprehension for all first order formulas (which may contain R-terms or other set parameters) and defining axioms for the R-terms which claim that for each ${\vec{x}}$ , we can remove finitely many elements from the set ${R\vec{x}X\phi(\vec{x},X)}$ such that the remaining set is homogeneous for ${\{{X}{\phi(\vec{x},X)\}}}$ . We show that the R-calculus proves the same ${\Pi^1_1}$ -sentences as the system of ${\Pi^1_2}$ -comprehension. (shrink)

Given a family${\cal C}$of infinite subsets of${\Bbb N}$, we study when there is a Borel function$S:2^{\Bbb N} \to 2^{\Bbb N} $such that for every infinite$x \in 2^{\Bbb N} $,$S\left \in {\Cal C}$and$S\left \subseteq x$. We show that the family of homogeneous sets as given by the Nash-Williams’ theorem admits such a Borel selector. However, we also show that the analogous result for Galvin’s lemma is not true by proving that there is an$F_\sigma $tall ideal on${\Bbb N}$without a Borel selector. The (...) proof is not constructive since it is based on complexity considerations. We construct a${\bf{\Pi }}_2^1 $tall ideal on${\Bbb N}$without a tall closed subset. (shrink)