1.1 The setup

Our intended domain of discourse is a second-order model of arithmetic, $\mathcal {N}= (N,\mathcal {P},+,\times ,<,0,1)$ , where $\mathcal {P} \subseteq 2^N$ (a family of subsets of $N$ ). Our logical symbols are those of arithmetic and equality. We use a two-sorted logic with integers $x \in N$ , integer variables $v$ which range over integers, sets $X\in \mathcal {P}$ , set variables $Y$ which range over sets, and the membership relation $x \in X$ . Our model need not be standard (i.e., $N$ may not be $\omega $ ), and $\mathcal {P}$ is most likely a proper subset of $2^N$ . Elements of $N$ will be called integers, and elements $X\in \mathcal {P}$ will be called sets.

We say that a formula is $\Sigma ^0_0$ , $\Pi ^0_0$ , or $\Delta ^0_0$ if all of its quantifiers range over integer variables and are bounded (i.e., $\forall v < t$ or $\exists v < t$ ). Number and set parameters are allowed in our formulas; for simplicity, we suppress these parameters in our notation hereafter. We also establish the convention that $\theta $ always denotes a $\Delta ^0_0$ formula. A formula is $\Sigma ^0_{n+1}$ if and only if (iff) it consists of a block of existential quantifiers followed by a formula in $\Pi ^0_n$ , and a formula is $\Pi ^0_{n+1}$ iff it consists of a block of universal quantifiers followed by a formula in $\Sigma ^0_n$ . A $\Delta ^0_{n+1}$ formula is one equivalent in $\mathcal {N}$ to both a $\Sigma ^0_{n+1}$ and a $\Pi ^0_{n+1}$ formula. At this point, we make no claims about what formulas might or might not be equivalent in $\mathcal {N}$ to $\Delta ^0_0$ , $\Sigma ^0_n$ , or $\Pi ^0_n$ formulas. An arithmetic formula is one which is $\Sigma ^0_{n}$ or $\Pi ^0_{n}$ for some $n$ .

Induction for a property or set $P \subseteq \mathbb {N}$ is the statement that if $P(0)$ holds, and $P(n)$ implies $P(n+1)$ for all $n$ , then $P(n)$ holds for all $n$ . If $\mathcal {N}$ is standard, then induction holds for all possible $P$ . If $\Gamma $ is a collection of subsets of $\mathbb {N}$ , we write $\mathrm {I}\Gamma $ to denote the scheme stating that induction holds for all sets in $\Gamma $ . Typical choices for $\Gamma $ are the classes of $\Delta ^0_0$ , $\Sigma ^0_n$ , or $\Pi ^0_n$ definable sets. For example, $\mathrm {I}\Delta ^0_0$ is the induction scheme for the sets $\{ x \in \mathbb {N} \mid \mathcal {N} \models \theta (x)\}$ , where $\theta $ is a $\Delta ^0_0$ formula (where again, set parameters are allowed in $\theta $ ). Arithmetic induction is induction for all arithmetically definable sets.

We need $\mathcal {N}$ to realize some fragment $F$ of true second-order arithmetic, i.e., the theory of the structure $(\omega , 2^{\omega }, +, \times , <, 0, 1)$ . $F$ must include $P^-$ , Peano Arithmetic without induction, and $\mathrm {I}\Delta ^0_0$ . A set $X$ in $\mathcal {N}$ is finite iff there is an integer $n \in \mathbb {N}$ such that for all $x \in X$ , $x \leq n$ . In Section 1.5, we need to code finite objects as integers via some sort of Gödel coding. For this purpose, we require exponentiation to be total. The details of showing that exponentiation is definable in $P^- + \mathrm {I}\Delta ^0_0$ are nontrivial, and we encourage the interested reader to explore Section 3 of Chapter V in Hájek and Pudlák [Reference Hájek and Pudlák12]. However, $P^- + \mathrm {I}\Delta ^0_0$ is not enough to show that exponentiation is total (i.e., that for all $x$ and $y$ , there is a $z$ such that $x^y=z$ ). $F$ must include at least the assertion that exponentiation is total, or something stronger like $\mathrm {I}\Sigma ^0_1$ ( $\mathrm {I}\Sigma ^0_1$ can show that exponentiation is total).

Informally, $\mathcal {P}$ should be closed under Turing reducibility. We formalize this via $\Delta ^0_1$ -comprehension ( $\Delta ^0_1\text {-CA}$ ). $\Delta ^0_1\text {-CA}$ states that if a formula $\varphi (x)$ is equivalent in $\mathcal {N}$ to both a $\Sigma ^0_1$ formula and a $\Pi ^0_1$ formula, then $\{ x \in \mathbb {N} \mid \mathcal {N} \models \varphi (x) \} \in \mathcal {P}$ . Thus, $F$ must include $\Delta ^0_1\text {-CA}$ , implying that at a minimum, $\mathcal {P}$ must contain the computable sets. We should point out that throughout this article, we discuss definable sets (i.e., sets of the form $\{ x \in \mathbb {N} \mid \mathcal {N} \models \varphi (x) \}$ ). However, unless $\varphi $ is equivalent to a $\Delta ^0_1$ formula, these sets need not reside in $\mathcal {P}$ . Note that there can be set parameters in $\varphi $ drawn from $\mathcal {P}$ . A definable partial function $f$ is one whose graph $G = \{ (x,y) \mid y = f(x) \}$ is a definable relation. We also assume that if $(x,y) \in G$ and $(x,z) \in G$ , then $y=z$ . Hereafter, $\mathcal {N}$ must be a model of $F$ ; this theory $F$ is also called $\mathrm {RCA}_0^*$ .

Our reference for all things related to first-order arithmetic is Kaye [Reference Kaye17], though another excellent choice is Hájek and Pudlák [Reference Hájek and Pudlák12]. For second-order arithmetic, we cite Simpson [Reference Simpson23] or Dzhafarov and Mummert [Reference Dzhafarov and Mummert9].

1.2 Bounding

The bounding scheme for a property $P$ states that the following statement $\Theta (n)$ holds for all $n$ :

$$ \begin{align*} \forall i < n \exists & b_i \bigg[ {P}(i,b_i) \bigg]\implies \\ \exists b \forall i < n \exists &b_i < b \bigg[ {P}(i,b_i) \bigg]. \end{align*} $$

Clearly, $\Theta (0)$ holds trivially, and if $\Theta (n)$ holds with witness $b$ , then $\max \{ b, b_n \}$ witnesses that $\Theta (n+1)$ holds. Thus, a sufficient level of induction implies bounding. It is instructive to state bounding explicitly for the $\Sigma ^0_2$ formula $\exists a \forall c \theta (i,b_i,a,c)$ : the following holds for all $n$ :

(1) $$ \begin{align}\begin{aligned} \forall i < n \exists & b_i \bigg[ \exists a \forall c \theta(i,b_i,a,c) \bigg]\implies \\ \exists b \forall i < n \exists &b_i < b \bigg[\exists a \forall c \theta(i,b_i,a,c) \bigg]. \end{aligned} \end{align} $$

The bounding scheme $\mathrm {B}\Sigma ^0_n$ is the bounding scheme restricted to $\Sigma ^0_n$ formulas. For any $n$ , $\mathrm {B}\Sigma ^0_n$ can be used to show that every formula is equivalent in $\mathcal {N}$ to one in Prenex Normal Form, where the bounded quantifiers are in the interior of the formula. This fact will be needed twice, once each in the proof of Theorem 9 and Lemma 10.

Kirby and Paris [Reference Kirby and Paris18] showed that for all $n$ , in $\mathcal {N}$ , $\mathrm {I}\Sigma ^0_{n+1}$ strictly implies $\mathrm {B}\Sigma ^0_{n}$ , which in turn strictly implies $\mathrm {I}\Sigma ^0_{n}$ . $\mathrm {B}\Sigma ^0_n$ , for $n\geq 2$ , is equivalent to a $\Pi ^0_{n+2}$ sentence (see [Reference Hájek and Pudlák12]).

1.3 Ramsey’s theorem

The Infinite Pigeonhole Principle states that if one has infinitely many pigeons and computably puts them into finitely many pigeonholes, at least one pigeonhole will have infinitely many pigeons. Formally, the Infinite $\Gamma $ -Pigeonhole Principle asserts that if $C$ is a $\Gamma $ -definable (in $\mathcal {N}$ ) partial coloring ( $C$ is a function whose graph is $\Gamma $ -definable) from $\mathbb {N}$ to some integer $k$ and $X$ is an infinite subset of the domain of $C$ , then there is an $x<k$ where $C^{-1}(x) \cap X$ is an infinite set in $\mathcal {N}$ . We will consider the Infinite Pigeonhole Principle as the Infinite $\Sigma ^0_1$ -Pigeonhole Principle. We denote this principle by $\mathrm {RT}^1_{< \infty }$ . Readers might expect us to consider the Infinite $\Delta ^0_1$ -Pigeonhole Principle, but we shall see that a solution to the Infinite $\Sigma ^0_1$ -Pigeonhole Principle implies one for the Infinite $\Delta ^0_1$ -Pigeonhole Principle. This will be discussed further in Sections 1.5 and 1.7. The Infinite Pigeonhole Principle is conceptually distinct from the finite Pigeonhole Principle, which states that if $m>n$ are integers and $f$ is a function from $m$ to $n$ , then there is an $x<n$ where $|f^{-1}(x)| \geq 2$ .

Let $[X]^n = \{ Y \subset X \mid |Y| = n \}$ , where $X$ is $\mathcal {N}$ -infinite. $\mathrm {RT}^n_k$ states that for every $k$ -coloring $C$ of $[X]^n$ , there is a homogeneous set $H$ such that $C$ is constant on $[H]^n$ . $\mathrm {RT}^n_{<\infty }$ is $\mathrm {RT}^n_k$ for all $k$ . A $k$ -coloring $C(x,s)$ is stable if $\lim _s C(x,s)$ exists. $\mathrm {SRT}^2_k$ is $\mathrm {RT}^2_k$ restricted to stable colorings.

1.4 Hirst’s theorems

The following results of Hirst are our main interest. These results were originally established in his 1987 doctoral dissertation [Reference Hirst15].

These results have had a lasting impact on reverse mathematics and are highly deserving of reflection. Our goal is to reprove and recast these results using Weihrauch reducibilities. We will see that there are still some interesting unexplored issues and subtleties about these results. While we expose some of these nuances, others remain open for future study. First, some basic computability theory inside $\mathcal {N}$ and a brief discussion of Weihrauch reductions are needed.

1.5 Computability theory

We are going to work inside $\mathcal {N}$ . Kleene’s $T$ -predicate, $T(e,x,s)$ , holds iff $s$ is the computation history of a halting run of the $e$ th Turing machine with input $x$ . Using course-of-values recursion, $s$ codes the sequence of configurations of the $e$ th Turing machine with input $x$ for each stage in the run. This relies on the fact that exponentiation is total and Gödel coding is available (for the reader wishing to learn more about course-of-values recursion and Gödel coding in our fragment $F$ , we direct them to Hájek and Pudlák [Reference Hájek and Pudlák12]). Kleene [Reference Kleene19] showed that the $T$ -predicate, $T(e,x,s)$ , is a primitive recursive relation. By Bennett [Reference Bennett2] (see Chapter I, Section 3(c) of [Reference Hájek and Pudlák12]), this relation is $\Delta ^0_0$ -definable in $\mathcal {N}$ . If we have $\mathcal {N} \models \mathrm {I}\Sigma ^0_1$ , then in $\mathcal {N}$ all the primitive recursive functions are total, but that is not necessary here.

$K = \{ e \mid \exists s T(e,e,s) \}$ is a $\Sigma ^0_1$ set. It is also $\Sigma ^0_1$ -complete, i.e., for all $\Sigma ^0_1$ formulas $\chi (x)$ , there is a computable total one-to-one function $f$ such that $\chi (x)$ iff $f(x) \in K$ . Let us denote $x \in W_{e,s}$ iff $\exists t< s T(e,x,t)$ . This is equivalent to the standard definition of a c.e. set. Hence “ $x\in W_{e,s}$ ” is equivalent to a $\Delta ^0_0$ formula $\varphi (x,s)$ . Every $\Delta ^0_0$ formula $\theta (x,s)$ is equivalent to “ $x\in W_{e,s}$ ” for some $e$ . The c.e. sets are the $\Sigma ^0_1$ -definable sets in $\mathcal {N}$ . For a set to be computable, both it and its complement need to be $\Sigma ^0_1$ -definable sets. So this set is $\Delta ^0_1$ . We will frequently equate computable objects with $\Delta ^0_1$ -definable objects. We consider a Turing functional $\Theta (X)$ as a $\Delta ^0_1$ -definable formula with a free variable $X$ .

One theorem we will need several times is that every infinite c.e. set uniformly contains an infinite computable subset. For example, consider a $\Sigma ^0_1$ -definable (in $\mathcal {N}$ ) partial coloring $C$ from $\mathbb {N}$ to some integer $n$ . The domain of $C$ is a c.e. set; if its domain contains an $\mathcal {N}$ -infinite subset, then it contains a computable $\mathcal {N}$ -infinite subset $X$ . We can always assume that we are working with this computable subset of the domain when the domain is infinite. This subset can be obtained uniformly from the coloring.

The index set $\mathrm {FIN} = \{ e \mid W_e \text { is finite} \} = \{ e \mid \exists b \forall s> b (W_{e,b} = W_{e,s})\}$ is $\Sigma ^0_2$ -complete. For all $\theta $ , there is a computable total one-to-one function $f$ such that:

(2) $$ \begin{align}\begin{aligned} \exists b_i \exists a \forall c & \theta(i,b_i,a,c) \text{ iff} \\ f(i) &\in \mathrm{FIN} \text{ iff}\\ \exists b_i \forall s>b_i &(W_{f(i),b_i} = W_{f(i),s}). \end{aligned}\end{align} $$

$\mathrm {COF} = \{ e \mid W_e \text { is cofinite} \} = \{ e \mid \exists k \forall x> k \exists s (x \in W_{e,s})\}$ is $\Sigma ^0_3$ -complete. Unfortunately, there are no similar “nice” index sets available for $\Sigma _n$ when $n>3$ .

A good computability reference is Soare [Reference Soare24], but there are plenty of newer references available. For working carefully in $\mathcal {N}$ , a good start is Simpson [Reference Simpson23].

1.6 Problems

We will consider the $\mathcal {N}$ -arithmetical formula $\mathcal {A}(I,S)$ asserting that $S$ is a solution of some instance $I$ of some fixed solvable problem $\mathcal {A}$ . There are no parameters in $\mathcal {A}$ other than the free variables $I$ and $S$ . A primary example is ${\mathrm {RT}}^2_2(C,H)$ , which says that $C$ is a $2$ -coloring of all pairs in some $\mathcal {N}$ -infinite set $X \subseteq \mathbb {N}$ and $H \subseteq X$ is a homogeneous $\mathcal {N}$ -infinite set. So $C$ is the instance and $H$ is the solution. In what follows, we recast some of our relevant arithmetic statements as problems. We will have to be careful to identify the instances and solutions of our problems.

Given a problem $\mathcal {A}(I,S)$ , we say that $\mathcal {N}$ realizes $\mathcal {A}$ iff $\mathcal {N}$ realizes that for all $I$ there is an $S$ such that $\mathcal {A}(I,S)$ . We assume that if $I$ is not an instance of the problem $\mathcal {A}$ (say, not a coloring, etc.), then $S = \emptyset $ . This is a reasonable assumption since determining whether $I$ is an instance of any of our problems is always arithmetic.

1.7 Weihrauch reducibility over $\mathcal {N}$

A Weihrauch reduction is the gold standard in showing one problem uniformly computes (or implies) another. If $\mathcal {N}$ is the standard model, this definition is the standard definition. This reduction, though not explicitly named, was in use in this fashion by Hirst and others long before it was named. For example, the reduction used to show that $\mathrm {SRT}^2_2$ follows from $\mathrm {RT}^2_2$ is a strong Weihrauch reduction with the needed functionals being the identity: $\mathrm {SRT}^2_2 \leq _{sW} \mathrm {RT}^2_2$ . Other examples will follow.

We are going to use Weihrauch reducibility as a replacement for a proof from $F$ . If $\mathcal {A}_0 \leq _W \mathcal {A}_1$ in $\mathcal {N}$ , then $\mathcal {N}$ realizes $\mathcal {A}_0$ . This implies that $F$ , our fragment of arithmetic, proves that $\mathcal {A}_1$ implies $\mathcal {A}_0$ . If $\mathcal {N}$ does not realize $\mathcal {A}_1$ , the Weihrauch reduction (and resulting proof) might be meaningless. Hence, the second clause in our above definition is necessary.

There is similar work in Reitzes [Reference Reitzes22] and Dzhafarovet al. [Reference Dzhafarov, Hirschfeldt and Reitzes8], where a proof of $\mathcal {A}_1 \Rightarrow \mathcal {A}_0$ in $\mathrm {RCA}_0$ is used to provide a winning strategy for a certain related game. There is one important difference between our definition and the ones considered in [Reference Dzhafarov, Hirschfeldt and Reitzes8, Reference Reitzes22] in that we assume that $\mathcal {N}$ realizes $\mathcal {A}_1$ . We can weaken that statement to $\forall I_0 \exists S_1 ( \mathcal {A}_1(\Phi (I_0),S_1))$ if necessary. Concretely, in [Reference Dzhafarov, Hirschfeldt and Reitzes8], they call the above reduction $\leq _W^{\mathrm {RCA}_0^*}$ and discuss $\mathrm {B}\Sigma ^0_2$ in Sections 6 and 7.

The Infinite $\Delta ^0_1$ -Pigeonhole Principle is strongly Weihrauch reducible to the Infinite $\Sigma ^0_1$ -Pigeonhole Principle via the identity functionals. Every $\Sigma ^0_1$ partial coloring has a $\Sigma ^0_1$ domain. Every infinite $\Sigma ^0_1$ set has an infinite $\Delta ^0_1$ set $X$ . Hence, the Infinite $\Sigma ^0_1$ -Pigeonhole Principle is strongly Weihrauch reducible to the Infinite $\Delta ^0_1$ -Pigeonhole Principle, where $\Phi $ restricts the given instance $C_0$ to the set $X$ and $\Psi $ is the identity functional (all of the above is in $\mathcal {N}$ ).

Given a problem $\mathcal {A}$ , if there is a Turing functional $\Xi $ such that $\mathcal {N}$ realizes $\forall I \mathcal {A}(I,\Xi (I))$ , then $\mathcal {A}$ is Weihrauch below every problem. We will call $\mathcal {A}$ Weihrauch trivial or just trivial in $\mathcal {N}$ . If a problem $\mathcal {A}_0$ is Weihrauch below a trivial problem $\mathcal {A}$ , it is also trivial, witnessed by $\Psi (I_0,\Xi (\Phi (I_0)))$ .

One of our main themes is to view Weihrauch reductions as a proof-theoretic tool. While we do not systematically investigate the general Weihrauch degree structure over $\mathcal {N}$ , in Section 4 we explore the Weihrauch reductions between a number of principles or problems logically equivalent to $\mathrm {B}\Sigma ^0_2$ . There are other places within the article where it is possible to make the same diversion, but in those cases we have found restraint. Good references for the Weihrauch reducibilities (over the standard model) and related material are Hirschfeldt and Jockusch [Reference Hirschfeldt and Jockusch14] and Dzhafarov and Mummert [Reference Dzhafarov and Mummert9].