Combinatorial principles equivalent to weak induction

TL;DR

This paper explores the logical strength of two combinatorial principles, ERT and ECT, showing their equivalences to certain induction schemes and analyzing their computational complexity via Weihrauch degrees.

Contribution

It provides new proofs of ERT within RCA_0, establishes their equivalences to specific induction schemes in RCA_0*, and conducts a Weihrauch degree analysis of these principles.

Findings

ERT is equivalent to Σ₁ induction in RCA₀*

ECT is equivalent to Σ₂ induction in RCA₀*

Weihrauch analysis shows ERT and ECT correspond to specific computational degrees

Abstract

We consider two combinatorial principles, ${\sf{ERT}}$ and ${\sf{ECT}}$. Both are easily proved in ${\sf{RCA}}_0$ plus ${\Sigma^0_2}$ induction. We give two proofs of ${\sf{ERT}}$ in ${\sf{RCA}}_0$, using different methods to eliminate the use of ${\Sigma^0_2}$ induction. Working in the weakened base system ${\sf{RCA}}_0^*$, we prove that ${\sf{ERT}}$ is equivalent to ${\Sigma^0_1}$ induction and ${\sf{ECT}}$ is equivalent to ${\Sigma^0_2}$ induction. We conclude with a Weihrauch analysis of the principles, showing ${\sf{ERT}} {\equiv_{\rm W}} {\sf{LPO}}^* {<_{\rm W}}{{\sf{TC}}_{\mathbb N}}^* {\equiv_{\rm W}} {\sf{ECT}}$.

Equations

$$\exists b\forall i<k\forall n((i,n)\in f\to n\le b).$$

$$f^{\prime }(n)=\{\begin{array}{ll}\min \{m\mid (n,m)\in f\}& \text{if}n\in D\\ 0& \text{otherwise.}\end{array}$$

$$f=\{(m,n)\mid \theta (m,n)\wedge \forall y<n\neg \theta (m,y)\}.$$

$$f(n)=\{\begin{array}{ll}j& \text{if }j<k\wedge (j,n)\in g\\ k& \text{otherwise.}\end{array}$$

$$g(n)=(f(n),{\text{mod}}_j|\{i<n\mid f(i)=f(n)\}|).$$

$$T=\{j<k\mid \forall n\exists x(x>n\wedge f(x)=j)\}$$

$$\forall j<k\exists s\forall x((j\notin T\wedge x>s)\to f(x)\ne j).$$

$$\forall j<k\forall x((j\notin T\wedge x>b)\to f(x)\ne j).$$

$$T=\{j<k\mid \exists x(x\ge b\wedge f(x)=j)\}.$$

$$\forall n\ge b\exists m\ge b(m\ne n\wedge f(m)=f(n)).$$

$$A_i=\{n\mid \forall m\ge n(f(m)\ne i)\}.$$

$$c((s,i))=\{\begin{array}{ll}i& \text{if}i\ne 0\wedge e_i(s)=\min \{n\mid \forall t<s(e_i(t)\ne n)\}\\ 0& \text{otherwise.}\end{array}$$

$$\mathsf{min}\mathsf{ECT}{\le }_{\mathrm{W}}{\mathsf{C}}_{\max }^{\#}{\le }_{\mathrm{W}}{\mathsf{TC}}_{\mathbb{N}}^{\ast }\times {\mathsf{isInfinite}}^{\ast }.$$

Full text

In their logical analysis of vertex colorings of hypergraphs, Davis, Hirst, Pardo, and Ransom [davisetal] isolate the combinatorial principle ${\sf{ERT}}$, and relate it to the nonexistence of finite conflict-free colorings for a particular hypergraph. The principle asserts that for any finite coloring of the natural numbers $\mathbb{N}$ there is a tail of the coloring such that every color appearing in the tail appears at least twice in the tail. ${\sf{ERT}}$ stands for eventually repeating tail, and can be formulated as follows.

The principle ${\sf{ERT}}$ is an immediate consequence of the principle ${\sf{ECT}}$ introduced by Hirst [hirst]. ${\sf{ECT}}$ stands for eventually constant palette tail, and asserts that for any finite coloring of $\mathbb{N}$ there is a tail of the coloring such that the colors appearing in any final segment of the tail are exactly those appearing in the entire tail. A more formal version follows.

Both Davis et al. [davisetal] and Hirst [hirst] work in the usual framework of reverse mathematics. In particular, they prove equivalences over the subsystem of second order arithmetic ${\sf{RCA}}_{0}$. This axiom system includes basic natural number arithmetic axioms, an induction scheme restricted to $\Sigma^{0}_{1}$ formulas (denoted ${\sf I}\Sigma^{0}_{1}$), and a recursive comprehension axiom that essentially asserts that computable sets of natural numbers exist. See Simpson’s book [simpson] for more about ${\sf{RCA}}_{0}$ and reverse mathematics. Theorem 6 of Hirst [hirst] shows that over ${\sf{RCA}}_{0}$, ${\sf{ECT}}$ is equivalent to ${\sf I}\Sigma^{0}_{2}$, an induction scheme for $\Sigma^{0}_{2}$ formulas. ${\sf{RCA}}_{0}$ can prove that ${\sf{ECT}}$ implies ${\sf{ERT}}$, so ${\sf{RCA}}_{0}$ proves that ${\sf I}\Sigma^{0}_{2}$ implies ${\sf{ERT}}$. As we will see in the next section, ${\sf I}\Sigma^{0}_{2}$ is not necessary in this proof.

1. ${\sf{RCA}}_{0}$ proves ${\sf{ERT}}$

Davis et al. [davisetal] show that ${\sf I}\Sigma^{0}_{2}$ is not needed in the proof of ${\sf{ERT}}$ by deriving ${\sf{ERT}}$ from a restricted form of Ramsey’s theorem and applying a result of Chong, Slaman, and Yang [csy]. There, Ramsey’s theorem is restricted to stable colorings of pairs, that is to functions $f:[\mathbb{N}]^{2}\to k$ such that for all $x$, $\lim_{y\to\infty}f(x,y)$ exists. Stable Ramsey’s theorem for pairs and two colors is denoted by ${\sf{SRT}^{2}_{2}}$ and can be formalized as follows.

${\sf{SRT}^{2}_{2}}$.

If $f:[\mathbb{N}]^{2}\to 2$ is stable, then there is an infinite set $H\subset\mathbb{N}$ and a color $c\in\{0,1\}$ such that for all $(x,y)\in[H]^{2}$, $f(x,y)=c$.

The next result appears as Theorem 11 in Davis et al. [davisetal]. The ${\sf{RCA}}_{0}$ in parentheses indicates that the proof can be carried out in the formal system ${\sf{RCA}}_{0}$. For completeness, we give a minimal sketch of the proof.

Lemma 1**.**

$({\sf{RCA}}_{0})$* ${\sf{SRT}^{2}_{2}}$ implies ${\sf{ERT}}$.*

Proof.

Working in ${\sf{RCA}}_{0}$, let $f:\mathbb{N}\to k$ be a coloring of $\mathbb{N}$ as in the statement of ${\sf{ERT}}$. Define a coloring of pairs, $g:[\mathbb{N}]^{2}\to 2$ by $g(a,b)=1$ if and only if for some $x$ in the half open interval of natural numbers $[a,b)$, $f(x)$ appears exactly once in the range of $f$ restricted to $[a,b)$. Because $g$ is stable, by ${\sf{SRT}^{2}_{2}}$ there is an infinite homogeneous set $H$. An argument based on the first $3\cdot 2^{k-1}$ elements of $H$ shows that $g$ is identically equal to [math]. Consequently, the minimum element of $H$ satisfies the requirements of the bound $b$ in the statement of ${\sf{ERT}}$. (For a more complete proof, see Davis et al. [davisetal]). ∎

By Corollary 2.6 of Chong, Slaman, and Yang [csy], ${\sf{SRT}^{2}_{2}}$ cannot prove ${\sf I}\Sigma^{0}_{2}$, so neither can ${\sf{ERT}}$. Thus although ${\sf{RCA}}_{0}+{\sf I}\Sigma^{0}_{2}$ proves ${\sf{ERT}}$, the full strength of ${\sf I}\Sigma^{0}_{2}$ is not necessary. Using a recent conservation result of Patey and Yokoyama [py], together with an alternative formalization of ${\sf{ERT}}$, we can show that ${\sf{RCA}}_{0}$ proves ${\sf{ERT}}$, completely eliminating the use of ${\sf I}\Sigma^{0}_{2}$.

Lemma 2**.**

$({\sf{RCA}}_{0})$* The following are equivalent.*

1. (1)

${\sf{ERT}}$. 2. (2)

${\sf{ERT}}^{\prime}:$* If $f:\mathbb{N}\to k$ for some $k\in\mathbb{N}$, then there is a number $b\in\mathbb{N}$, a set $I\subset[0,k)$ consisting of the range of $f$ on $[b,\infty)$, and a witness set $\{(x_{i},y_{i})\mid i\in I\}$ such that for every $z\geq b$, we have $f(z)\in I$, $b\leq x_{f(z)}<y_{f(z)}$, and $f(z)=f(x_{f(z)})=f(y_{f(z)})$.*

Proof.

We will work in ${\sf{RCA}}_{0}$. Note that for any $f$, the number $b$ provided by ${\sf{ERT}}^{\prime}$ also satisfies the statement of ${\sf{ERT}}$. Thus ${\sf{ERT}}$ follows immediately from ${\sf{ERT}}^{\prime}$.

To prove the converse, let $f:\mathbb{N}\to k$ and apply ${\sf{ERT}}$ to obtain $b$. The set $I=\{j<k\mid\exists t(t\geq b\land f(t)=j)\}$ exists by bounded $\Sigma^{0}_{1}$ comprehension, a consequence of ${\sf{RCA}}_{0}$ [simpson]*Theorem II.3.9. For each $i\in I$, there are at least two distinct values $x_{i}\geq b$ and $y_{i}\geq b$ such that $f(x_{i})=f(y_{i})=i$. Picking the least such witness pair for each $i$, recursive comprehension proves the existence of the witness set $\{(x_{i},y_{i})\mid i\in I\}$. Routine arguments verify that $b$ and this witness set satisfy the requirements of ${\sf{ERT}}^{\prime}$. ∎

Applying the two lemmas and using a result of Patey and Yokoyama [py], we can easily prove ${\sf{ERT}}$ in ${\sf{RCA}}_{0}$, answering a question of Davis et al. [davisetal]. An alternative direct proof of Theorem 3 is included in the next section in the proof of Theorem 6.

Theorem 3**.**

${\sf{RCA}}_{0}$* proves ${\sf{ERT}}$.*

Proof.

$({\sf{RCA}}_{0})$ By Lemma 1, ${\sf{RCA}}_{0}+{\sf{SRT}^{2}_{2}}$ proves ${\sf{ERT}}$. Thus, by Lemma 2, ${\sf{RCA}}_{0}+{\sf{SRT}^{2}_{2}}$ proves ${\sf{ERT}}^{\prime}$. By Theorem 7.4 of Patey and Yokoyama [py], ${\sf{RCA}}_{0}+{\sf{SRT}^{2}_{2}}$ is a conservative extension of ${\sf{RCA}}_{0}$ for formulas of the form $\forall X\varphi(X)$, where $\varphi$ is $\Pi^{0}_{3}$. ${\sf{ERT}}^{\prime}$ has this form, so ${\sf{RCA}}_{0}$ proves ${\sf{ERT}}^{\prime}$. By Lemma 2, ${\sf{RCA}}_{0}$ proves ${\sf{ERT}}$. ∎

The conservation result of Patey and Yokoyama is a powerful tool for eliminating the use of $\Sigma^{0}_{2}$ induction in the proofs of combinatorial principles. Their result actually holds for Ramsey’s theorem for pairs and two colors, so it is not necessary to limit ourselves to stable colorings. The principle ${\sf{ERT}}^{\prime}$ can be formalized in the form $\forall X\varphi(X)$ where $\varphi$ is $\Sigma^{0}_{2}$. Clearly, we have made use of less than the full strength of this technique in our example. On the other hand, if ${\sf{ERT}}$ is directly formalized in the form $\forall X\theta(X)$, the formula $\theta$ is $\Sigma^{0}_{3}$, so Patey and Yokoyama’s result does not apply. Lemma 2 is a necessary step in the argument.

2. Reverse mathematics: ${\sf{ERT}}$ is ${\sf I}\Sigma^{0}_{1}$ and ${\sf{ECT}}$ is ${\sf I}\Sigma^{0}_{2}$

In this section, we prove that our combinatorial principles are equivalent to induction schemes over the weakened base system ${\sf{RCA}}_{0}^{*}$. The axioms of ${\sf{RCA}}_{0}^{*}$ are those of ${\sf{RCA}}_{0}$ less the $\Sigma^{0}_{1}$ induction scheme, with the addition of a $\Sigma^{0}_{0}$ induction scheme and function symbols and axioms for integer exponentiation. The subsystem is described in Chapter X of Simpson’s book [simpson]. The following lemma incorporates results from an early work of Simpson and Smith [ss]. Note the change in the base system at the beginning of the statement of the lemma.

Lemma 4**.**

$({\sf{RCA}}_{0}^{*})$* The following are equivalent.*

1. (1)

${\sf I}\Sigma^{0}_{1}$, the $\Sigma^{0}_{1}$ induction scheme. 2. (2)

The universe of total functions is closed under primitive recursion. 3. (3)

Bounded $\Sigma^{0}_{1}$ comprehension. 4. (4)

Bounded $\Pi^{0}_{1}$ comprehension.

Proof.

The equivalence of items (1), (2), and (3) are included in Lemma 2.5 of the article of Simpson and Smith [ss]. Recursive comprehension proves the existence of complements of sets, so items (3) and (4) are also equivalent. ∎

For our arguments, it is useful to formalize the concept of a partial function. Working in ${\sf{RCA}}_{0}^{*}$, we can define a code for a finite partial function as a set of ordered pairs $f\subset[0,k)\times\mathbb{N}$ such that for all $i$, $n$, and $m$, if $(i,n)\in f$ and $(i,m)\in f$, then $n=m$. Using this notion, we can state another equivalent form of ${\sf I}\Sigma^{0}_{1}$.

Lemma 5**.**

$({\sf{RCA}}_{0}^{*})$* The following are equivalent:*

1. (1)

${\sf I}\Sigma^{0}_{1}$. 2. (2)

Finite partial functions have bounded ranges. That is, if $f\subset k\times\mathbb{N}$ is a finite partial function, then

[TABLE]

Proof.

To prove (1) implies (2), working in ${\sf{RCA}}_{0}^{*}$, assume ${\sf I}\Sigma^{0}_{1}$ and let $f$ be a finite partial function contained in $k\times\mathbb{N}$. By Lemma 4, we may apply bounded $\Sigma^{0}_{1}$ comprehension and find the set $D=\{x<k\mid\exists y(x,y)\in f\}$. By recursive comprehension, there is a total function $f^{\prime}$ satisfying

[TABLE]

By Lemma 4, we may apply primitive recursion to find the summation function $g(n)=\sum_{i=0}^{n}f^{\prime}(i)$. The integer $g(k-1)$ is a suitable bound for the range of $f$.

To prove the converse, we will use (2) to prove bounded $\Sigma^{0}_{1}$ comprehension. Let $\theta(m,n)$ be a $\Sigma^{0}_{0}$ formula and fix a bound $k$. We will prove that the set $\{m<k\mid\exists n\theta(m,n)\}$ exists. Using recursive comprehension, we can find the set of pairs

[TABLE]

Note that $f$ is a partial function from $k$ into $\mathbb{N}$. By (2), there is a bound $b$ for the range of $f$. Thus, for all $m<k$, $\exists n\theta(m,n)$ if and only if $\exists n\leq b\,\theta(m,n)$. So $\{m<k\mid\exists n\theta(m,n)\}$ is identical to $\{m<k\mid\exists n\leq b\,\theta(m,n)\}$, and its existence follows from recursive comprehension. ∎

We can now show that ${\sf{ERT}}$ is equivalent to ${\sf I}\Sigma^{0}_{1}$ over ${\sf{RCA}}_{0}^{*}$. Because ${\sf{RCA}}_{0}^{*}$ plus ${\sf I}\Sigma^{0}_{1}$ is ${\sf{RCA}}_{0}$, this provides a direct proof of ${\sf{ERT}}$ in ${\sf{RCA}}_{0}$, without the use of conservation results. Following the proof of the theorem, we will comment on this as a technique for eliminating ${\sf I}\Sigma^{0}_{2}$ in proofs of combinatorial results.

Theorem 6**.**

$({\sf{RCA}}_{0}^{*})$* The following are equivalent.*

1. (1)

${\sf I}\Sigma^{0}_{1}$. 2. (2)

${\sf{ERT}}$. 3. (3)

$\forall j{\sf{ERT}}(j)$. Here ${\sf{ERT}}(j)$ generalizes ${\sf{ERT}}$, requiring that at or after the bound $b$, any value of $f$ that appears must appear at least $j$ times.

Proof.

To show that (1) implies (2), we could simply cite Theorem 3. We present a direct proof using sequential applications of bounded comprehension that will be adapted to prove Theorem 8 below. Working in ${\sf{RCA}}_{0}^{*}$, assume ${\sf I}\Sigma^{0}_{1}$. By Lemma 4, we may apply bounded $\Sigma^{0}_{1}$ comprehension. We will prove ${\sf{ERT}}$ for $f:\mathbb{N}\to k$. By bounded $\Sigma^{0}_{1}$ comprehension, we can find the set of (codes for) non-repeating finite sequences of values less than $k$ such that the colors appear in this order somewhere in the range of $f$. More formally, bounded $\Sigma^{0}_{1}$ comprehension proves the existence of a set $S$ of (codes for) sequences such that $\sigma\in S$ if and only if

• $\bullet$

${\rm{length}}(\sigma)<k$,

• $\bullet$

$\forall i<{\rm{length}}(\sigma)\,(\sigma(i)<k)$,

• $\bullet$

$\forall i<{\rm{length}}(\sigma)\,\forall j<{\rm{length}}(\sigma)\,(\sigma(i)=\sigma(j)\to i=j)$,

and there is a finite witness sequence $\tau$ such that

• $\bullet$

${\rm{length}}(\sigma)={\rm{length}}(\tau)$,

• $\bullet$

$\forall i<{\rm{length}}(\tau)\,\forall j<{\rm{length}}(\tau)\,(i<j\to\tau(i)<\tau(j))$,

• $\bullet$

$\forall i<{\rm{length}}(\tau)(f(\tau(i))=\sigma(i))$.

By Lemma 4, we may also use bounded $\Pi^{0}_{1}$ comprehension. Using $S$ as a parameter and applying bounded $\Pi^{0}_{1}$ comprehension, we can find a subset $T$ of $S$ consisting of the empty sequence and all those sequences $\sigma$ such that the first time the colors appear in the specified order, the last color never reappears. When selecting the first witness sequence, we assume that for sequences differing in a single entry, the sequence with the smaller entry appears first. Thus, $\sigma$ is in $T$ if and only if $\sigma$ is empty, or $\sigma\in S$ and for the first witness sequence $\tau$ for $\sigma$ and any $j>{\rm{length}}(\tau)-1$, $f(j)\neq\sigma({\rm{length}}(\tau)-1)$. $T$ is a subset of the finite set of non-repeating sequences of numbers less than $k$, so ${\sf{RCA}}_{0}^{*}$ can answer questions about whether or not sequences are in $T$. In particular, we can define a subset $T_{0}\subset T$ of sequences $\sigma$ such that no extension of $\sigma$ is in $T$ and every initial segment of $\sigma$ is in $T$. Suppose $\sigma_{0}\in T_{0}$. If $\sigma_{0}$ is empty, then every color in the range of $f$ appears at least twice, and $b=0$ is the desired bound for ${\sf{ERT}}$. If $\sigma_{0}$ is nonempty, let $\tau_{0}$ be the first witness sequence for $\sigma_{0}$, and define $b=\tau_{0}({\rm{length}}(\sigma_{0})-1)+1$. Because $\sigma_{0}$ is in $T$ and none of its extensions are, every color appearing at or after $b$ must appear at least twice. Summarizing, the bound $b$ satisfies the requirements of ${\sf{ERT}}$.

Next, we will show that (2) implies (1) by proving the contrapositive. Suppose ${\sf{RCA}}_{0}^{*}$ holds and ${\sf I}\Sigma^{0}_{1}$ fails. By Lemma 5, there is a finite partial function $g\subset k\times\mathbb{N}$ with an unbounded range. Define the function $f:\mathbb{N}\to k+1$ by

[TABLE]

The function $f$ exists by recursive comprehension, and for any $b$ there is an $n>b$ such that $f(n)<k$ and the value of $f(n)$ appears only once in the range of $f$. Thus no $b$ can be a bound for ${\sf{ERT}}$ applied to $f$, and ${\sf{ERT}}$ fails.

Because (2) is a special case of (3), to complete the proof of the theorem, it suffices to show in ${\sf{RCA}}_{0}^{*}$ that $\forall j{\sf{ERT}}(j)$ follows from ${\sf{ERT}}$. By our previous work, ${\sf I}\Sigma^{0}_{1}$ follows from ${\sf{ERT}}$, so we may work in ${\sf{RCA}}_{0}$. Fix $j$ and suppose $f:\mathbb{N}\to k$. Our goal is to find a $b$ such that every color appearing at or after $b$ appears at least $j$ times in the range of $f$ at or after $b$. Define $g:\mathbb{N}\to k\times j$ by setting

[TABLE]

Intuitively, if $f$ takes the value $i$ at locations $x_{0},x_{1},\dots x_{j}$ (and nowhere before or in between), then $g(x_{0})=(i,0)$, $g(x_{1})=(i,1),$ $\dots,$ $g(x_{j-1})=(i,j-1)$, and $g(x_{j})=(i,0)$. Using a bijection between $k\times j$ and the natural numbers less than $k\cdot j$, we can view $g$ as a function from $\mathbb{N}$ into $k\cdot j$. Let $b$ be a bound for ${\sf{ERT}}$ applied to $g$. Suppose color $i$ appears at or after $b$ in the range of $f$. Let $x_{0}$ be the first such location. Then for some $m<j$, $g(x_{0})=(i,m)$. Note that $x_{0}$ is the first location at or after $b$ where $g$ takes this value. By ${\sf{ERT}}$ for $g$, there is an $x_{1}>x_{0}$ such that $g(x_{1})=g(x_{0})$. By the definition of $g$, there are at least $j$ places in $[x_{0},x_{1})$ where $f$ takes the value $i$. Thus $b$ is a bound for ${\sf{ERT}}(j)$ for $f$. This completes the proof of (3) from (2) and the proof of the theorem. ∎

For use in the proof of Theorem 11, note that the set $T$ defined in the preceding proof can be used to compute the minimum bound satisfying ${\sf{ERT}}$. Because we are making a computability theoretic argument, we are not restricted to ${\sf{RCA}}_{0}^{*}$. If every color in the range of $f$ appears at least twice, then no sequences of length one appear in $T_{0}$, so $\sigma_{0}$ is the empty sequence and $b=0$ is the minimum bound. Otherwise, define finite sequences $\sigma$ and $\tau$ as follows. Let $\sigma(0)$ be the last appearing among colors that appear exactly once, and let $\tau(0)$ be the location where $\sigma(0)$ appears. Let $\sigma(i+1)$ be the last appearing among colors that appear exactly once after $\tau(i)$ if such a color exists, and let $\tau(i+1)$ be the last location where $\sigma(i)$ appears. If no such color exists, terminate the sequences. Routine verifications show that $\sigma\in T_{0}$ and that $\tau$ is the first witness for $\sigma$, so that $b=\tau({\rm{length}}(\sigma)-1)+1$ is a bound for ${\sf{ERT}}$. From the construction, if $b^{\prime}$ is any bound for ${\sf{ERT}}$, then $b^{\prime}>\tau(0)$, and for $i<{\rm{length}}(\sigma)$, if $b^{\prime}>\tau(i)$ then $b^{\prime}>\tau(i+1)$. Thus $b$ is minimal. Consequently, the minimum bound can be calculated by listing $T_{0}$, calculating the value $b$ for each sequence in $T_{0}$, and then selecting the minimum bound.

The existence of the set $T$ in the proof that (1) implies (2) above used an application of bounded $\Sigma^{0}_{1}$ comprehension followed by an application of bounded $\Pi^{0}_{1}$ comprehension. Naïvely concatenating the associated formulas to construct $T$ with a single application results in a use of bounded $\Sigma^{0}_{2}$ comprehension, a principle equivalent to ${\sf I}\Sigma^{0}_{2}$ [simpson]*Exercise II.3.13. Conversely, it may be possible to eliminate unnecessary uses of ${\sf I}\Sigma^{0}_{2}$ in proofs, particularly in the guise of bounded $\Sigma^{0}_{2}$ or bounded $\Pi^{0}_{2}$ comprehension, by using a sequence of applications of bounded $\Sigma^{0}_{1}$ or bounded $\Pi^{0}_{1}$ comprehension. In the case of the preceding proof, the sequential applications can be combined into a single application, as in the second part of the proof of Theorem 8 below.

We complete this section with a proof of the equivalence of ${\sf I}\Sigma^{0}_{2}$ and ${\sf{ECT}}$, showing that ${\sf{ERT}}$ is strictly weaker than ${\sf{ECT}}$ over ${\sf{RCA}}_{0}^{*}$. This result differs from those in the article of Hirst [hirst] in the use of the weaker base system ${\sf{RCA}}_{0}^{*}$. The arguments here sidestep the tree colorings used for [hirst]*Theorem 6 and in the alternative argument following [hirst]*Theorem 7, which is based on the conservation result of Corduan, Groszek, and Mileti [cgm].

Theorem 7**.**

$({\sf{RCA}}_{0}^{*})$* The following are equivalent.*

1. (1)

${\sf I}\Sigma^{0}_{2}$. 2. (2)

${\sf{ECT}}$.

Proof.

To prove that (1) implies (2), assume ${\sf I}\Sigma^{0}_{2}$ and fix $f:\mathbb{N}\to k$. Because ${\sf I}\Sigma^{0}_{2}$ implies ${\sf I}\Sigma^{0}_{1}$, we may work in ${\sf{RCA}}_{0}$. By bounded $\Pi^{0}_{2}$ comprehension, a consequence of ${\sf I}\Sigma^{0}_{2}$ ([simpson]*Exercise II.3.13, plus complementation via recursive comprehension), the set

[TABLE]

exists. If $j\notin T$, then after some point $j$ ceases to appear in the range of $f$. Formally,

[TABLE]

By the $\Pi^{0}_{1}$ bounding principle, a consequence of ${\sf I}\Sigma^{0}_{2}$ [simpson]*Exercise II.3.15, there is a $b$ such that

[TABLE]

In particular, if $j\notin T$ then for all $x\geq b$ we have $f(x)\neq j$. Summarizing, the range of $f$ at or after $b$ is exactly $T$, and every value of $T$ appears infinitely often in the the range. Thus $b$ satisfies the requirements of ${\sf{ECT}}$.

We will prove that (2) implies (1), by a two stage bootstrapping argument. For the first step, working in ${\sf{RCA}}_{0}^{*}$, note that ${\sf{ECT}}$ implies ${\sf{ERT}}$. By Theorem 6, we may deduce ${\sf I}\Sigma^{0}_{1}$, so from now on we can work in ${\sf{RCA}}_{0}$.

For the second step, we will use ${\sf{ECT}}$ to prove bounded $\Pi^{0}_{2}$ comprehension, and then deduce ${\sf I}\Sigma^{0}_{2}$. Fix $k$ and consider $T=\{j<k\mid\forall x\exists y\theta(j,x,y)\}$ where $\theta$ is a $\Sigma^{0}_{0}$ formula. Our goal is to prove the existence of $T$. Suppose $(j,x,y)$ is the $n^{\text{th}}$ triple in a bijective enumeration of $k\times\mathbb{N}\times\mathbb{N}$. Define $f(n)=j$ if $y$ is the first witness that $\forall s<x\,\exists t\leq y\,\theta(j,s,t)$, and let $f(n)=k$ otherwise. The function $f$ exists by recursive comprehension. For any $j<k$, $j$ appears infinitely often in the range of $f$ if and only if $\forall x\exists y\theta(j,x,y)$. Apply ${\sf{ECT}}$ to $f$ and obtain a bound $b$. Then

[TABLE]

By bounded $\Sigma^{0}_{1}$ comprehension, a consequence of ${\sf{RCA}}_{0}$ [simpson]*Theorem II.3.9, the set $T$ exists, proving bounded $\Pi^{0}_{2}$ comprehension. To complete the proof, recall that by the first step above, we may work in ${\sf{RCA}}_{0}$. By complementation, bounded $\Pi^{0}_{2}$ comprehension implies bounded $\Sigma^{0}_{2}$ comprehension. Applying Exercise II.3.13 of Simpson [simpson], $\Sigma^{0}_{2}$ induction follows from ${\sf{RCA}}_{0}$ and bounded $\Sigma^{0}_{2}$ comprehension. ∎

3. Weihrauch analysis

The goal of this section is to analyze ${\sf{ERT}}$ and ${\sf{ECT}}$ using Weihrauch reductions. Because ${\sf{ERT}}$ and ${\sf{ECT}}$ have number outputs rather than set outputs, Weihrauch reducibility yields meaningful results where other forms of computability-theoretic reducibility would not. We will consider Weihrauch problems defined by subsets of $\mathbb{N}^{\mathbb{N}}\times\mathbb{N}$. Each problem $P$ can be viewed as a multifunction mapping instances $I\in{\text{domain}}(P)$ into solutions $S$ with $(I,S)\in P$. A problem $P$ is Weihrauch reducible to a problem $Q$, written $P\leq_{\rm W}Q$, if instances of $P$ can be uniformly computably transformed into instances of $Q$ whose solutions can be uniformly computably transformed into solutions of the problem $P$. This last transformation may make use of the original instance of $P$. More formally, $P\leq_{\rm W}Q$ if there are computable functionals $\Phi$ and $\Psi$ such that for all $I\in{\text{domain}}(P)$, $\Phi(I)\in{\text{domain}}(Q)$, and for all $S$ such that $(\Phi(I),S)\in Q$, we have $(I,\Psi(I,S))\in P$. We write $P\equiv_{\rm W}Q$ if $P\leq_{\rm W}Q$ and $Q\leq_{\rm W}P$, and write $P<_{\rm W}Q$ if $P\leq_{\rm W}Q$ and $Q\not\leq_{\rm W}P$.

The relation $\equiv_{\rm W}$ is an equivalence relation on the Weihrauch problems. The equivalence classes are called Weihrauch degrees, and many have well-known representing problems. For example, many Weihrauch problems are known to be equivalent to the Weihrauch problem ${\sf{LPO}}$ (Limited Principle of Omniscience). This problem takes as an instance any $f\in\mathbb{N}^{\mathbb{N}}$, and outputs [math] if $\exists nf(n)=0$ and $1$ otherwise. For an introduction to Weihrauch reducibility and many Weihrauch degrees, see the article of Brattka and Gherardi [bg] and the survey of Brattka, Gherardi, and Pauly [bgp].

Many operators on Weihrauch problems preserve reducibility. For example, for a problem $P$, the problem $P^{n}$ is the result of $n$ parallel applications of $P$. The problem $P^{*}$ is the result of an arbitrary finite number of parallel applications of $P$. Thus, for each $n$, we have $P^{n}\leq_{\rm W}P^{*}$. Pauly introduces the concept of $P^{*}$ in [pauly] and in Theorem 6.5 shows that $P\leq_{\rm W}Q$ implies $P^{*}\leq_{\rm W}Q^{*}$. Thus $\cdot^{*}$ can be viewed as an operator that preserves Weihrauch reducibility.

We may view ${\sf{ERT}}$ as a Weihrauch problem, where the input is a number $k$ and a function $f:\mathbb{N}\to k$, and the solution is a value $b$ as provided by ${\sf{ERT}}$, that is,

[TABLE]

In a similar fashion, ${\sf{ECT}}$ can be viewed as a Weihrauch problem. Our goal is to find a known Weihrauch problems equivalent to ${\sf{ERT}}$ and to ${\sf{ECT}}$, and to separate ${\sf{ERT}}$ and ${\sf{ECT}}$ in the Weihrauch setting. As a first step, we can state the following theorem.

Theorem 8**.**

${\sf{ERT}}\equiv_{\rm W}{\sf{LPO}}^{*}$.

Proof.

First we show that ${\sf{LPO}}^{*}\leq_{\rm W}{\sf{ERT}}$. Given $k$ ${\sf{LPO}}$ instances $f_{0},\dots f_{k-1}$ we define a coloring $g:\mathbb{N}\to k+1$ as follows. For $i<k$, let $g(nk+i)=i$ if and only if $f_{i}(n)=0$ and $\forall m<n(f_{i}(m)\neq 0)$. Else, set $g(nk+i)=k$. Note that by construction, all colors but $k$ appear at most once in the range of $g$. Thus any solution to ${\sf{ERT}}$ for $g$ must be an upper bound for the first occurrence of [math] in the range of any $f_{i}$, which allows us to solve ${\sf{LPO}}$ for each $f_{i}$.

For the converse reduction, we can adapt the first part of the proof of Theorem 6, substituting ${\sf{LPO}}^{*}$ for the uses of bounded comprehension. Given $f:\mathbb{N}\to k$ we can use finitely many parallel applications of ${\sf{LPO}}$ to find the non-repeating sequences of colors in the set $S$. Simultaneously, we can use finitely many parallel applications of ${\sf{LPO}}$ to find those sequences that appear and whose last color reappears. Call the set of these sequences $T^{\prime}$. A sequence is in the set $T$ defined in the proof of Theorem 6 if and only if it is in $S$ and is not in $T^{\prime}$. Given the set $T$, we can find the bound $b$ satisfying ${\sf{ERT}}$ for $f$ by the construction in the proof of Theorem 6. This shows that ${\sf{ERT}}\leq_{\rm W}{\sf{LPO}}^{*}$. Summarizing, ${\sf{ERT}}\equiv_{\rm W}{\sf{LPO}}^{*}$. ∎

Next, we turn to the Weihrauch analysis of ${\sf{ECT}}$. The principle Discrete Choice, denoted ${\sf{C}}_{\mathbb{N}}$, takes as an input an enumeration of the complement of a nonempty set $A$ and outputs an element of $A$. The article of Neumann and Pauly [np] introduces and studies ${\sf{TC}}_{\mathbb{N}}$, the total continuation of ${\sf{C}}_{\mathbb{N}}$. ${\sf{TC}}_{\mathbb{N}}$ accepts the enumeration of the complement of any set $A$, empty or not, and outputs a number, which will be an element of $A$ if $A$ is nonempty. Clearly, ${\sf{C}}_{\mathbb{N}}\leq_{\rm W}{\sf{TC}}_{\mathbb{N}}$, and consequently ${\sf{C}}_{\mathbb{N}}\leq_{\rm W}{\sf{TC}}_{\mathbb{N}}^{*}$. Lemma 5 of Neumann and Pauly [np] includes ${\sf{LPO}}^{*}<_{\rm W}{\sf{C}}_{\mathbb{N}}$. Concatenating the relations, ${\sf{LPO}}^{*}<_{\rm W}{\sf{TC}}_{\mathbb{N}}^{*}$. The next theorem links ${\sf{TC}}_{\mathbb{N}}^{*}$ and ${\sf{ECT}}$.

Theorem 9**.**

${\sf{ECT}}\equiv_{\rm W}{\sf{TC}}_{\mathbb{N}}^{*}$.

Proof.

To see that ${\sf{ECT}}\leq_{\rm W}{\sf{TC}}_{\mathbb{N}}^{*}$, suppose the coloring $f:\mathbb{N}\to k$ is an instance of ${\sf{ECT}}$. Our goal is to use finitely many applications of ${\sf{TC}}_{\mathbb{N}}$ to find a value $b$ such that every color appearing at or after $b$ appears infinitely often in the range of $f$. For each $i<k$ construct an enumeration of the complement of the set

[TABLE]

Apply ${\sf{TC}}_{\mathbb{N}}$ to each of these sets to obtain numbers $b_{i}$ such that if the color $i$ appears only finitely often, then it no longer appears after $b_{i}$. The number $b=1+\max\{b_{i}\mid i<k\}$ is a solution to the ${\sf{ECT}}$ instance.

For the converse direction, suppose $A_{i}$ for $1\leq i<k$ is a finite list of ${\sf{TC}}_{\mathbb{N}}$ instances, where for each $i$, $e_{i}$ enumerates the complement of $A_{i}$. Fix a bijective pairing function $(\cdot,\cdot):\mathbb{N}\times k\to\mathbb{N}$, and define the coloring $c:\mathbb{N}\to k$ by

[TABLE]

Apply ${\sf{ECT}}$ to $c$ to find a bound $b$. If some color $i\neq 0$ appears infinitely often in the range of $c$, then $A_{i}=\emptyset$. Otherwise, if $i$ never appears after $b$ and $s$ is sufficiently large that $(s,i)\geq b$, then $\min\{n\mid\forall t<s(e_{i}(t)\neq n)\}$ is in $A_{i}$. In either case, $\min\{n\mid\forall t<s(e_{i}(t)\neq n)\}$ is a valid output for ${\sf{TC}}_{\mathbb{N}}$ applied to the input $A_{i}$. ∎

Summarizing, we have shown that ${\sf{ERT}}\equiv_{\rm W}{\sf{LPO}}^{*}$, ${\sf{LPO}}^{*}<_{\rm W}{\sf{TC}}_{\mathbb{N}}^{*}$, and ${\sf{TC}}_{\mathbb{N}}^{*}\equiv_{\rm W}{\sf{ECT}}$, so ${\sf{ERT}}<_{\rm W}{\sf{ECT}}$. We have captured the strength of ${\sf{ERT}}$ and ${\sf{ECT}}$ in terms of known Weihrauch degrees, and shown that ${\sf{ERT}}$ is strictly weaker than ${\sf{ECT}}$ in the Weihrauch degrees.

Both Theorem 8 and Theorem 9 fail for strong Weihrauch reducibility. In strong reducibility, the solution to the input problem must be computed from any solution of the transformed problem without further reference to the original input. Using the notation from the first paragraph of this section, $P\leq_{\rm sW}Q$ if there are computable functionals $\Phi$ and $\Psi$ such that for all $I\in{\text{domain}}(P)$, $\Phi(I)\in{\text{domain}}(Q)$, and for all $S$ such that $(\Phi(I),S)\in Q$, we have $(I,\Psi(S))\in P$.

As an example using familiar problems, we will show that ${\sf{LPO}}^{*}<_{\rm sW}{\sf{TC}}_{\mathbb{N}}^{*}$. To see that ${\sf{LPO}}\leq_{\rm sW}{\sf{TC}}_{\mathbb{N}}$, given an instance $f$ of ${\sf{LPO}}$, construct an instance $g$ of ${\sf{TC}}_{\mathbb{N}}$ by setting $g(n)=n+1$ if $f(n)\neq 0$ and $g(n)=0$ otherwise. If the solution for $g$ is positive, then the solution for $f$ is [math]. If the solution for $g$ is [math], then the solution for $f$ is $1$. Similarly, sequences of ${\sf{LPO}}$ problems can be transformed to sequences of ${\sf{TC}}_{\mathbb{N}}$ problems, so ${\sf{LPO}}^{*}\leq_{\rm sW}{\sf{TC}}_{\mathbb{N}}^{*}$. We know ${\sf{TC}}_{\mathbb{N}}^{*}\not\leq_{\rm W}{\sf{LPO}}^{*}$, so ${\sf{TC}}_{\mathbb{N}}^{*}\not\leq_{\rm sW}{\sf{LPO}}^{*}$, and thus ${\sf{LPO}}^{*}<_{\rm sW}{\sf{TC}}_{\mathbb{N}}^{*}$. The next theorem summarizes strong reducibility relations for ${\sf{ERT}}$ and ${\sf{ECT}}$.

Theorem 10**.**

${\sf{ERT}}<_{\rm sW}{\sf{ECT}}<_{\rm sW}{\sf{TC}}_{\mathbb{N}}^{*}$, ${\sf{LPO}}\not\leq_{\rm sW}{\sf{ECT}}$, and ${\sf{ERT}}\not\leq_{\rm sW}{\sf{LPO}}^{*}$.

Proof.

Identity functionals witness ${\sf{ERT}}\leq_{\rm sW}{\sf{ECT}}$. We know ${\sf{ECT}}\not\leq_{\rm W}{\sf{ERT}}$, so ${\sf{ECT}}\not\leq_{\rm sW}{\sf{ERT}}$ and thus ${\sf{ERT}}<_{\rm sW}{\sf{ECT}}$.

The first paragraph of the proof of Theorem 9 shows that ${\sf{ECT}}\leq_{\rm sW}{\sf{TC}}_{\mathbb{N}}^{*}$. The failure of the converse relation and ${\sf{ECT}}<_{\rm sW}{\sf{TC}}_{\mathbb{N}}^{*}$ both follow from ${\sf{LPO}}\not\leq_{\rm sW}{\sf{ECT}}$, which we prove next.

To see that ${\sf{LPO}}\not\leq_{\rm sW}{\sf{ECT}}$, suppose by contradiction that $\Phi$ and $\Psi$ witness ${\sf{LPO}}\leq_{\rm sW}{\sf{ECT}}$. Suppose $f_{1}$ and $f_{2}$ are ${\sf{LPO}}$ problems with distinct solutions. Let $\Phi(f_{1})=g_{1}$ and $\Phi(f_{2})=g_{2}$ be the associated ${\sf{ECT}}$ problems. Let $b_{1}$ be a solution for $g_{1}$ and $b_{2}$ be a solution for $g_{2}$. Then $b=\max\{b_{1},b_{2}\}$ is a solution for both $g_{1}$ and $g_{2}$. Then $\Psi(b)$ is a solution for both $f_{1}$ and $f_{2}$, yielding a contradiction. Thus ${\sf{LPO}}\not\leq_{\rm sW}{\sf{ECT}}$. This argument is an example of the general principle that no multifunction of the form $f:X\rightrightarrows\mathbb{N}$ where all $f(x)$ are upwards closed can compute a non-trivial multifunction $g:X\rightrightarrows k$ for finite $k$.

To see that ${\sf{ERT}}\not\leq_{\rm sW}{\sf{LPO}}^{*}$, we again argue by contradiction, supposing that $\Phi$ and $\Psi$ witness ${\sf{ERT}}\leq_{\rm sW}{\sf{LPO}}^{*}$. Let $f_{1}$ be the instance of ${\sf{ECT}}$ consisting of a two-coloring that is constantly zero. Suppose $\Phi(f_{1})=(g_{1},\dots,g_{n})$ is a sequence of $n$ instances of ${\sf{LPO}}$. The computation of $\Phi(f_{1})$ uses only a finite initial segment of $f_{1}$. Denote the length of this segment by $k$. The ${\sf{LPO}}$ problems $g_{1},\dots,g_{n}$ have solutions $s_{1},\dots,s_{n}$. Thus $\Psi(s_{1},\dots,s_{n})$ computes a bound $m$ satisfying ${\sf{ERT}}$ for $f_{1}$. Now consider the ${\sf{ERT}}$ problem $f_{2}$, consisting of a two-coloring that contains $k+m$ zeros, followed by a single one, followed by an infinite string of zeros. Because $f_{2}$ and $f_{1}$ agree on the first $k$ values, $\Phi(f_{2})=\Phi(f_{1})=(g_{1},\dots,g_{n})$. These ${\sf{LPO}}$ problems are the same as before, and so still have the solutions $s_{1},\dots,s_{n}$. Thus $\Psi(s_{1},\dots,s_{n})=m$ should be a bound satisfying ${\sf{ERT}}$ for $f_{2}$. However, by the construction of $f_{2}$, any bound for $f_{2}$ must be at least $k+m+1$, which is strictly larger than $m$. Thus $\Phi$ and $\Psi$ cannot be witnesses of ${\sf{ERT}}\leq_{\rm sW}{\sf{LPO}}^{*}$, and we have shown that ${\sf{ERT}}\not\leq_{\rm sW}{\sf{LPO}}^{*}$. ∎

Minor alterations in the formulations of ${\sf{ERT}}$ and ${\sf{ECT}}$ can result in interesting variations in their Weihrauch strengths. For example, let ${\sf{min}{\sf{ERT}}}$ denote the principle that outputs the minimum bound satisfying ${\sf{ERT}}$. Define ${\sf{min}{\sf{ECT}}}$ similarly.

Theorem 11**.**

${\sf{ERT}}\equiv_{\rm W}{\sf{min}{\sf{ERT}}}$* and ${\sf{RCA}}_{0}^{*}$ proves ${\sf{ERT}}\leftrightarrow{\sf{min}{\sf{ERT}}}$.*

Proof.

Every solution of ${\sf{min}{\sf{ERT}}}$ is a solution of ${\sf{ERT}}$, so ${\sf{ERT}}\leq_{\rm W}{\sf{min}{\sf{ERT}}}$. For the converse, apply the second paragraph of the proof of Theorem 8, using ${\sf{LPO}}^{*}$ to find the set $T$. By the note following the proof of Theorem 6, $T$ can be used to calculate the minimum bound. Thus ${\sf{min}{\sf{ERT}}}\leq_{\rm W}{\sf{LPO}}^{*}$. By Theorem 8, ${\sf{LPO}}^{*}\leq_{\rm W}{\sf{ERT}}$, so ${\sf{min}{\sf{ERT}}}\leq_{\rm W}{\sf{ERT}}$.

For the reverse mathematics result, ${\sf{RCA}}_{0}^{*}$ proves ${\sf{min}{\sf{ERT}}}$ implies ${\sf{ERT}}$ trivially. To prove the converse, assume ${\sf{ERT}}$ and let $f:\mathbb{N}\to k$. By ${\sf{ERT}}$, we can find a bound $b$. By Theorem 6, ${\sf{ERT}}$ implies $\Sigma^{0}_{1}$ induction, so by Lemma 4 we can use bounded $\Sigma^{0}_{1}$ comprehension to find $Y=\{c<k\mid\exists x(x\geq b\land f(x)=c\}$, the range of $f$ on $[b,\infty)$. By the $\Sigma^{0}_{0}$ least element principle, there is a least $n\leq b$ such that for all $t\in[n,b]$, either $f(t)\in Y$ or $f(t)$ appears at least twice in $[n,b]$. This least $n$ satisfies ${\sf{min}{\sf{ERT}}}$. ∎

In contrast to Theorem 11, we will prove below that ${\sf{ECT}}<_{\rm W}{\sf{min}{\sf{ECT}}}$. Our proof uses the following characterization of ${\sf{min}{\sf{ECT}}}$ in terms of ${\sf{TC}}_{\mathbb{N}}$ and ${\sf{isInfinite}}$. The principle ${\sf{isInfinite}}$ takes an infinite binary string as input, outputs $1$ if it has infinitely many ones, and outputs [math] otherwise. The notation $P\times Q$ denotes the principle corresponding to solving $P$ and $Q$ in parallel.

Theorem 12**.**

${\sf{min}{\sf{ECT}}}\equiv_{\rm W}{\sf{TC}}_{\mathbb{N}}^{*}\times{\sf{isInfinite}}^{*}$.

Proof.

To see that ${\sf{min}{\sf{ECT}}}\leq_{\rm W}{\sf{TC}}_{\mathbb{N}}^{*}\times{\sf{isInfinite}}^{*}$, let $f:\mathbb{N}\to k$ be an instance of ${\sf{min}{\sf{ECT}}}$. For each $j<k$, we can use one instance of ${\sf{isInfinite}}$ to determine if $j$ appears infinitely many times in the range of $f$, and one instance of ${\sf{TC}}_{\mathbb{N}}$ to find the last occurrence of $j$ in the case that $j$ appears only finitely many times. Adding one to the maximum of the positions for the values that do not appear infinitely many times yields the desired output for ${\sf{min}{\sf{ECT}}}$.

The converse relation takes a few steps. By Theorem 9, ${\sf{TC}}_{\mathbb{N}}^{*}\equiv_{\rm W}{\sf{ECT}}$. Trivially, ${\sf{ECT}}\leq_{\rm W}{\sf{min}{\sf{ECT}}}$, so ${\sf{TC}}_{\mathbb{N}}^{*}\leq_{\rm W}{\sf{min}{\sf{ECT}}}$.

To see that ${\sf{isInfinite}}\leq_{\rm W}{\sf{min}{\sf{ECT}}}$, let $p$ denote an infinite binary sequence. Let $r$ be the sequence consisting of a $1$ followed by the result of alternating [math] with digits from $p$. Then ${\sf{min}{\sf{ECT}}}(r)$ is [math] if and only if $1$ appears infinitely many times in $p$.

Next, we show that ${\sf{min}{\sf{ECT}}}$ is idempotent, or to be more precise, that ${\sf{min}{\sf{ECT}}}\times{\sf{min}{\sf{ECT}}}\leq_{\rm W}{\sf{min}{\sf{ECT}}}$. Let $\langle\cdot,\cdot\rangle:\mathbb{N}\times\mathbb{N}\to\mathbb{N}$ be a bijective map such that if $m_{0}\leq m_{1}$ and $n_{0}\leq n_{1}$, then $\langle m_{0},n_{0}\rangle\leq\langle m_{1},n_{1}\rangle$. Let $p$ and $q$ be instances of ${\sf{min}{\sf{ECT}}}$. Replace $p(0)$ with a color not appearing in the range of $p$. This increases the value of ${\sf{min}{\sf{ECT}}}$ by one only in the case that every color appears infinitely often in the original sequence. We can now assume that at least one color appears only finitely many times in $p$. Make the same adjustment and assumption for $q$. Define the coloring $r$ by $r(\langle n,m\rangle)=\langle p(n),q(m)\rangle$. If $n_{0}$ is the last time some color $c_{0}$ appears in $p$, and $n_{1}$ is the last time that some color $c_{1}$ appears in $q$, then $\langle n_{0},n_{1}\rangle$ is the last time that $\langle c_{0},c_{1}\rangle$ appears in $r$. Conversely, if $\langle c_{0},c_{1}\rangle$ appears for the last time at position $\langle n_{0},n_{1}\rangle$, then $c_{0}$ must appear last in $p$ at $n_{0}$, and $c_{1}$ must appear last in $q$ at $n_{1}$. Thus, solutions for $p$ and $q$ can be extracted from the solution for $r$.

Iterated applications of the idempotence of ${\sf{min}{\sf{ECT}}}$ (or an application of Proposition 4.4 of [bgp]) show that ${\sf{min}{\sf{ECT}}}^{*}\leq_{\rm W}{\sf{min}{\sf{ECT}}}$. Because ${\sf{isInfinite}}\leq_{\rm W}{\sf{min}{\sf{ECT}}}$, we have ${\sf{isInfinite}}^{*}\leq_{\rm W}{\sf{min}{\sf{ECT}}}^{*}\leq_{\rm W}{\sf{min}{\sf{ECT}}}$. We have already shown that ${\sf{TC}}_{\mathbb{N}}^{*}\leq_{\rm W}{\sf{min}{\sf{ECT}}}$, so ${\sf{TC}}_{\mathbb{N}}^{*}\times{\sf{isInfinite}}^{*}\leq_{\rm W}{\sf{min}{\sf{ECT}}}\times{\sf{min}{\sf{ECT}}}\leq_{\rm W}{\sf{min}{\sf{ECT}}}$, completing the proof of the theorem. ∎

The next result assists in separating ${\sf{ECT}}$ and ${\sf{min}{\sf{ECT}}}$.

Theorem 13**.**

${\sf{isInfinite}}\not\leq_{\rm W}{\sf{TC}}_{\mathbb{N}}^{*}$.

Proof.

Suppose by way of contradiction that $\Phi$ and $\Psi$ witness ${\sf{isInfinite}}\leq_{\rm W}{\sf{TC}}_{\mathbb{N}}^{*}$. The function mapping sequences $p$ to the number of instances of ${\sf{TC}}_{\mathbb{N}}$ in $\Phi(p)$ is computable and therefore continuous. Let $\sigma_{0}$ and $n$ be such that $\Phi(p)$ consists of $n$ instances of ${\sf{TC}}_{\mathbb{N}}$ for all $p\succcurlyeq\sigma_{0}$, that is for all $p$ extending $\sigma_{0}$. Denote the ranges of these instances by $\Phi(p)_{1},\dots,\Phi(p)_{n}$. For $i\leq n$ and $m\in\mathbb{N}$, define $C_{m,i}=\{\sigma\succcurlyeq\sigma_{0}\mid m\in\Phi(\sigma)_{i}\}$. Let $\sigma_{1}$ be an extension of $\sigma_{0}$ such that for each $i\in[1,n]$, either every $C_{m,i}$ is dense below $\sigma_{1}$, or there is an $m_{i}$ such that $C_{m_{i},i}$ contains no extension of $\sigma_{1}$. Let $F$ be the set of all $i$ such that $m_{i}$ is defined.

Let $p$ consist of $\sigma_{1}$ followed by an infinite sequence of zeros. The sequence $p$ has finitely many ones. There is a solution $(a_{1},\dots,a_{n})$ of $\Phi(p)$ such that $a_{i}=m_{i}$ for all $i\in F$. Then $\Psi(a_{1},\dots,a_{n},p)$ returns [math], with a computation that depends only on $a_{1},\dots,a_{n}$ and a finite initial segment $\sigma_{2}$ of $p$. Let $g\succ\sigma_{2}$ be 1-generic. If $i\notin F$, then for every $m$, $C_{m,i}$ is dense below $\sigma_{2}$, so $\Phi(g)_{i}=\mathbb{N}$. Thus, $(a_{1},\dots,a_{n})$ is a solution of $\Phi(g)$. But $\Psi(a_{1},\dots,a_{n},g)=\Psi(a_{1},\dots,a_{n},p)=0$ and $g$ has infinitely many ones, yielding the desired contradiction. ∎

Theorem 14**.**

${\sf{ECT}}<_{\rm W}{\sf{min}{\sf{ECT}}}$* and ${\sf{RCA}}_{0}^{*}$ proves ${\sf{ECT}}\leftrightarrow{\sf{min}{\sf{ECT}}}$.*

Proof.

Trivially, ${\sf{ECT}}\leq_{\rm W}{\sf{min}{\sf{ECT}}}$. To prove the strict inequality, suppose by contradiction that ${\sf{min}{\sf{ECT}}}\leq_{\rm W}{\sf{ECT}}$. By Theorem 12, ${\sf{isInfinite}}\leq_{\rm W}{\sf{min}{\sf{ECT}}}$, so by Theorem 9, ${\sf{isInfinite}}\leq_{\rm W}{\sf{TC}}_{\mathbb{N}}^{*}$, contradicting Theorem 13.

Shifting focus to reverse mathematics, trivially ${\sf{RCA}}_{0}^{*}$ proves that ${\sf{min}{\sf{ECT}}}$ implies ${\sf{ECT}}$. For the converse, assuming ${\sf{ECT}}$, by Theorem 7, we may use $\Sigma^{0}_{2}$ induction. By the $\Pi^{0}_{1}$ least element principle (a consequence of $\Sigma^{0}_{1}$ induction), a minimal bound can be found in the first part of the proof of Theorem 7. Thus, over ${\sf{RCA}}_{0}^{*}$, ${\sf{ECT}}$ is equivalent to ${\sf{min}{\sf{ECT}}}$. ∎

Theorem 14 demonstrates the ability of Weihrauch reductions to make finer distinctions in this setting.

Our final result links ${\sf{min}{\sf{ECT}}}$ to principles considered by Hirst and Mummert [hm]. The principle ${\sf{C}^{\#}_{\rm{max}}}$ takes as inputs a size $n$ and the enumeration of the complement of a collection of finite subsets of $\mathbb{N}$, each of size at most $n$, and outputs an element of the collection of maximum cardinality.

Theorem 15**.**

${\sf{min}{\sf{ECT}}}\equiv_{\rm W}{\sf{C}^{\#}_{\rm{max}}}$.

Proof.

From Theorem 12 we know ${\sf{min}{\sf{ECT}}}\equiv_{\rm W}{\sf{TC}}_{\mathbb{N}}^{*}\times{\sf{isInfinite}}^{*}$, so it suffices to show that

[TABLE]

For the first reduction, suppose $f:\mathbb{N}\to k$ is an instance of ${\sf{min}{\sf{ECT}}}$. Consider the set $A$ of all finite sets $F\subset k\times\mathbb{N}$ such that for each $j<k$, if $(j,n)\in F$ then $n$ is the maximum natural number such that $f(j)=n$. Here we are identifying pairs with their integer codes, so $F$ can be viewed as a subset of $\mathbb{N}$. The set $A$ is $\Pi^{0}_{1}$ definable using $f$ as a parameter, and its complement can be enumerated by a function uniformly computable from $f$. Use this enumeration and the size $k$ as the input for ${\sf{C}^{\#}_{\rm{max}}}$, and let $F_{0}$ be the resulting maximal output set. Adding $1$ to the maximum of the second coordinates of the elements of $F_{0}$ yields the desired bound for ${\sf{min}{\sf{ECT}}}$.

To prove the final reduction, it is useful to note that ${\sf{TC}}_{\mathbb{N}}$ can be used to count the numbers of ones in a binary string. Using a bijective pairing function, given a sequence $p:\mathbb{N}\to 2$, we can define an enumeration $q$ of the (codes for) pairs that omits at most one pair, so that the first coordinate of that omitted pair corresponds to the number of ones in the range of $p$, provided that number is finite. Calculation of $q$ can be viewed as a moving marker process. Place a marker on $(0,0)$ and then alternate enumerating unmarked pairs and calculating values of $p$ until a $1$ appears in the range of $p$. Move the marker to the first non-enumerated pair with an initial coordinate of $1$, enumerate $(0,0)$, and continue enumerating unmarked pairs and calculating values of $p$ until the next $1$ appears in the range of $p$. Iterate. If there are infinitely many ones in the range of $p$, then $q$ will enumerate all pairs. If only finitely many ones appear, ${\sf{TC}}_{\mathbb{N}}$ applied to $q$ will find a pair with the desired first coordinate.

To prove that ${\sf{C}^{\#}_{\rm{max}}}\leq_{\rm W}{\sf{TC}}_{\mathbb{N}}^{*}\times{\sf{isInfinite}}^{*}$, let $f:\mathbb{N}\to\mathbb{N}^{<\mathbb{N}}$ enumerate the complement of a set $A$ of finite subsets of $\mathbb{N}$, each of size less than $k$. For each positive $i<k$, let $e_{i}$ be an enumeration of all the subsets of $\mathbb{N}$ of size exactly $i$. For each positive $i<k$, define the instance $p_{i}$ of ${\sf{isInfinite}}$ as follows. Set $p_{i}(n)=1$ if there is a $t\leq n$ such that $f(t)=e_{i}(c_{t})$ where $c_{t}=|\{j<n\mid p_{i}(j)=1\}|$, and set $p_{i}(n)=0$ otherwise. Thus $f$ enumerates all sets of size $i$ if and only if the range of $p_{i}$ contains infinitely many ones, and the range of $p_{i}$ contains a total of $n$ ones if and only if $e_{i}(n)$ is the first set enumerated by $e_{i}$ that is in $A$. For each $p_{i}$, let $q_{i}$ be the associated instance of ${\sf{TC}}_{\mathbb{N}}$ that counts the ones in the range of $p_{i}$. Given the solutions to ${\sf{isInfinite}}$ for each $p_{i}$ and to ${\sf{TC}}_{\mathbb{N}}$ for each $q_{i}$ for all $i<k$, we can find the maximum $j$ such that ${\sf{isInfinite}}$ fails for $p_{j}$. If $n$ is the output from ${\sf{TC}}_{\mathbb{N}}$ for $q_{j}$, then $e_{j}(n)$ is a maximal element of $A$, solving the instance ${\sf{C}^{\#}_{\rm{max}}}$ corresponding to $f$. ∎

Hirst and Mummert [hm] showed that ${\sf{C}^{\#}_{\rm{max}}}$ is Weihrauch equivalent and provably equivalent over ${\sf{RCA}}_{0}$ to several principles formalizing calculation of bases for bounded dimension matroids and vector spaces, and finding connected component decompositions of graphs with finitely many components. Thus ${\sf{min}{\sf{ECT}}}$ is Weihrauch equivalent to all these principles, ${\sf{ECT}}$ is strictly Weihrauch weaker, and all of them are provably equivalent over ${\sf{RCA}}_{0}$.

Acknowledgements

Discussions contributing to this work occurred at the Workshop on Ramsey Theory and Computability, organized by Peter Cholak and held July 9-13 of 2018 at the Rome Notre Dame Global Gateway. Further discussions occurred at Dagstuhl Seminar 18361, organized by Vasco Brattka, Damir Dzhafarov, Alberto Marcone, and Arno Pauly, and held September 2-7 of 2018 at Schloss Dagstuhl, the Leibniz-Zentrum für Informatik. Denis Hirschfeldt was partially supported by grant DMS-1600543 from the National Science Foundation of the United States. Jeffry Hirst’s travel was supported by a SAFE grant from the College of Arts and Sciences, a grant from the Office of International Education and Development, and a Board of Trustees travel grant, all from Appalachian State University. Yokoyama was partially supported by JSPS KAKENHI (grant numbers 16K17640 and 15H03634), JSPS Core-to-Core Program (A. Advanced Research Networks) and JAIST Research Grant 2018 (Houga).

{bibsection}

[Bibliography] BrattkaVascoGherardiGuidoEffective choice and boundedness principles in computable analysisBull. Symbolic Logic172011173–117ISSN 1079-8986Review MathReviewsDocument@article{bg, author = {Brattka, Vasco}, author = {Gherardi, Guido}, title = {Effective choice and boundedness principles in computable analysis}, journal = {Bull. Symbolic Logic}, volume = {17}, date = {2011}, number = {1}, pages = {73–117}, issn = {1079-8986}, review = {\MR{2760117}}, doi = {10.2178/bsl/1294186663}} BrattkaVascoGherardiGuidoPaulyArnoWeihrauch complexity in computable analysis201750+xiarXiv:1707.03202@article{bgp, author = {Brattka, Vasco}, author = {Gherardi, Guido}, author = {Pauly, Arno}, title = {Weihrauch Complexity in Computable Analysis}, year = {2017}, pages = {50+xi}, eprint = {arXiv:1707.03202}} ChongC. T.SlamanTheodore A.YangYueThe metamathematics of stable ramsey’s theorem for pairsJ. Amer. Math. Soc.2720143863–892ISSN 0894-0347Review MathReviews@article{csy, author = {Chong, C. T.}, author = {Slaman, Theodore A.}, author = {Yang, Yue}, title = {The metamathematics of stable Ramsey's theorem for pairs}, journal = {J. Amer. Math. Soc.}, volume = {27}, date = {2014}, number = {3}, pages = {863–892}, issn = {0894-0347}, review = {\MR{3194495}}} CorduanJaredGroszekMarcia J.MiletiJoseph R.Reverse mathematics and ramsey’s property for treesJ. Symbolic Logic7520103945–954ISSN 0022-4812Review MathReviewsDocument@article{cgm, author = {Corduan, Jared}, author = {Groszek, Marcia J.}, author = {Mileti, Joseph R.}, title = {Reverse mathematics and Ramsey's property for trees}, journal = {J. Symbolic Logic}, volume = {75}, date = {2010}, number = {3}, pages = {945–954}, issn = {0022-4812}, review = {\MR{2723776}}, doi = {10.2178/jsl/1278682209}} DavisCalebHirstJeffryPardoJakeRansomTimReverse mathematics and colorings of hypergraphsNovember 29, 2018Archive for Mathematical LogicDocument@article{davisetal, author = {Davis, Caleb}, author = {Hirst, Jeffry}, author = {Pardo, Jake}, author = {Ransom, Tim}, title = {Reverse mathematics and colorings of hypergraphs}, date = {November 29, 2018}, journal = {Archive for Mathematical Logic}, doi = {10.1007/s00153-018-0654-z}} HirstJeffry L.Disguising induction: proofs of the pigeonhole principle for treestitle={Foundational adventures}, series={Tributes}, volume={22}, publisher={Coll. Publ., London}, 2014113–123Review MathReviews@article{hirst, author = {Hirst, Jeffry L.}, title = {Disguising induction: proofs of the pigeonhole principle for trees}, conference = {title={Foundational adventures}, }, book = {series={Tributes}, volume={22}, publisher={Coll. Publ., London}, }, date = {2014}, pages = {113–123}, review = {\MR{3241956}}} HirstJeffry L.MummertCarlReverse mathematics of matroidstitle={Computability and complexity}, series={Lecture Notes in Comput. Sci.}, volume={10010}, publisher={Springer, Cham}, 2017143–159Review MathReviews@article{hm, author = {Hirst, Jeffry L.}, author = {Mummert, Carl}, title = {Reverse mathematics of matroids}, conference = {title={Computability and complexity}, }, book = {series={Lecture Notes in Comput. Sci.}, volume={10010}, publisher={Springer, Cham}, }, date = {2017}, pages = {143–159}, review = {\MR{3629720}}} NeumannEikePaulyArnoA topological view on algebraic computation modelsJ. Complexity4420181–22ISSN 0885-064XReview MathReviewsDocument@article{np, author = {Neumann, Eike}, author = {Pauly, Arno}, title = {A topological view on algebraic computation models}, journal = {J. Complexity}, volume = {44}, date = {2018}, pages = {1–22}, issn = {0885-064X}, review = {\MR{3724808}}, doi = {10.1016/j.jco.2017.08.003}} PateyLudovicYokoyamaKeitaThe proof-theoretic strength of ramsey’s theorem for pairs and two colorsAdv. Math.33020181034–1070ISSN 0001-8708Review MathReviewsDocument@article{py, author = {Patey, Ludovic}, author = {Yokoyama, Keita}, title = {The proof-theoretic strength of Ramsey's theorem for pairs and two colors}, journal = {Adv. Math.}, volume = {330}, date = {2018}, pages = {1034–1070}, issn = {0001-8708}, review = {\MR{3787563}}, doi = {10.1016/j.aim.2018.03.035}} PaulyArnoOn the (semi)lattices induced by continuous reducibilitiesMLQ Math. Log. Q.5620105488–502ISSN 0942-5616Review MathReviewsDocument@article{pauly, author = {Pauly, Arno}, title = {On the (semi)lattices induced by continuous reducibilities}, journal = {MLQ Math. Log. Q.}, volume = {56}, date = {2010}, number = {5}, pages = {488–502}, issn = {0942-5616}, review = {\MR{2742884}}, doi = {10.1002/malq.200910104}} SimpsonStephen G.Subsystems of second order arithmeticPerspectives in Logic2Cambridge University Press, Cambridge; Association for Symbolic Logic, Poughkeepsie, NY2009xvi+444ISBN 978-0-521-88439-6Review MathReviewsDocument@book{simpson, author = {Simpson, Stephen G.}, title = {Subsystems of second order arithmetic}, series = {Perspectives in Logic}, edition = {2}, publisher = {Cambridge University Press, Cambridge; Association for Symbolic Logic, Poughkeepsie, NY}, date = {2009}, pages = {xvi+444}, isbn = {978-0-521-88439-6}, review = {\MR{2517689}}, doi = {10.1017/CBO9780511581007}} SimpsonStephen G.SmithRick L.Factorization of polynomials and $\Sigma^{0}_{1}$ inductionSpecial issue: second Southeast Asian logic conference (Bangkok, 1984)Ann. Pure Appl. Logic3119862-3289–306ISSN 0168-0072Review MathReviewsDocument@article{ss, author = {Simpson, Stephen G.}, author = {Smith, Rick L.}, title = {Factorization of polynomials and $\Sigma^0_1$ induction}, note = {Special issue: second Southeast Asian logic conference (Bangkok, 1984)}, journal = {Ann. Pure Appl. Logic}, volume = {31}, date = {1986}, number = {2-3}, pages = {289–306}, issn = {0168-0072}, review = {\MR{854297}}, doi = {10.1016/0168-0072(86)90074-6}}

• • Caleb Davis
• Department of Mathematical Sciences, Appalachian State University
• ASU Box 32092, Boone, NC 28608 USA
• davisc3@appstate.edu
• • Denis R. Hirschfeldt
• Department of Mathematics, The University of Chicago
• 5734 S. University Ave., Chicago, IL 60637 USA
• drh@math.uchicago.edu
• • Jeffry Hirst
• Department of Mathematical Sciences, Appalachian State University
• ASU Box 32092, Boone, NC 28608 USA
• hirstjl@appstate.edu
• • Jake Pardo
• Department of Mathematical Sciences, Appalachian State University
• ASU Box 32092, Boone, NC 28608 USA
• jpardo@alumni.nd.edu
• • Arno Pauly
• Department of Computer Science, Swansea University
• Singleton Park, Swansea SA2 8PP United Kingdom
• arno.m.pauly@gmail.com
• • Keita Yokoyama
• School of Information Science
• Japan Advanced Institute of Science and Technology
• 1-1 Asahidai, Nomi, Ishikawa 923-1292 Japan
• y-keita@jaist.ac.jp