# Reverse mathematics and Weihrauch analysis motivated by finite complexity
theory

Zack BeMent, Jeffry Hirst, and Asuka Wallace Corresponding author: Jeffry
Hirst<EMAIL_ADDRESS>
Authors’ pre-peer-review draft.

(May 4, 2021)

###### Abstract

We extend a study by Lempp and Hirst of infinite versions of some problems
from finite complexity theory, using an intuitionistic version of reverse
mathematics and techniques of Weihrauch analysis.

An early article of Hirst and Lempp [hl] was motivated by the following
example. The problem of determining if a finite graph has a Hamiltonian path
is NP complete, while the problem for Eulerian paths is in the class P. In
reverse mathematics, the problem of selecting which infinite graphs in an
infinite sequence have Hamiltonian paths is equivalent to
${\Pi^{1}_{1}{\text{-}}{\sf{CA}}_{0}}$, while the corresponding problem for
Eulerian graphs is equivalent to ${\sf ACA}_{0}$. While very evocative, Hirst
and Lempp showed that this parallel does not generally hold. In conjunction
with an AMS special session in honor of Lempp’s birthday, we revisited these
early results using the tools of Weihrauch analysis in two ways.

In the next section we concentrate on formalized Weihrauch reductions for
graph theoretic problems. This approach is limited to problems that can be
expressed with particularly simple formulas, having certain subformulas that
are $\exists$-free. The process yields both reverse mathematical and Weihrauch
reducibility results from a single argument. More importantly, it facilitates
the use of techniques from Weihrauch analysis, like parallelization, in
reverse mathematics proofs. Additionally, the intuitionistic formal systems
used admit proof mining [kbook], so terms corresponding to the reduction
functionals could be extracted from formal proofs. If we view the proofs as a
form of verification, formal Weihrauch reduction could offer a framework for
finding verified extensions of a trusted library of routines.

The final section addresses Weihrauch analysis of stronger results, with
parallelizations at the ${\Pi^{1}_{1}{\text{-}}{\sf{CA}}_{0}}$ level. The
formulas describing the problems are too complicated for formal analysis
techniques, so we turn to traditional Weihrauch analysis. The results extend
the currently small catalog of Weihrauch problems at this level, for example
like those in [leaf]. Weihrauch analysis at the level of
${\Pi^{1}_{1}{\text{-}}{\sf{CA}}_{0}}$ appears to parallel familiar reverse
mathematics closely, in contrast to recent results related to ${\sf ATR}_{0}$
by Kihara, Marcone, and Pauly [kmp].

##  1 Formalized Weihrauch analysis

The following development of formalized Weihrauch reducibility draws from work
of Hirst and Mummert [hm]. Like them, we work in $i{\sf RCA}_{0}^{\omega}$,
Kohlenbach’s [k2001] higher order axiomatization for reverse mathematics,
restricted to intuitionistic logic. Informally, we may view $i{\sf
RCA}_{0}^{\omega}$ as an axiomatization of intuitionistic arithmetic that can
prove the existence of computable functions and computable functionals. For
more details of the axiomatization, see [hm].

We formalize a Weihrauch problem with a formula $\forall x(p_{1}(x)\to\exists
y\,p_{2}(x,y))$ where $p_{1}(x)$ indicates that $x$ is an accepted input and
$p_{2}(x,y)$ indicates that $y$ is a solution of $x$. Here $y$ may be a
function, set, or number, depending on the problem. For total problems, that
is, those problems accepting all sets as inputs, we can use the more simple
representation $\forall x\exists y\,p(x,y)$.

Some of the results connecting provability and formalized Weihrauch
reducibility are restricted to a family of formulas called $\Gamma_{1}$ by
Troelstra [troelstra]. A formula is $\exists$-free if it is built from atomic
formulas using only universal quantification and the connectives $\land$ and
$\to$. (Troelstra includes $\bot$ as an atomic formula, so $\neg P$
abbreviates $P\to\bot$.) The collection $\Gamma_{1}$ consists of those
formulas defined inductively by the following:

  * $\bullet$

All atomic formulas are elements of $\Gamma_{1}$.

  * $\bullet$

If $A$ and $B$ are in $\Gamma_{1}$, then so are $A\land B$, $A\lor B$,
$\forall xA$, and $\exists xA$.

  * $\bullet$

If $A$ is $\exists$-free and $B$ is in $\Gamma_{1}$ then $\exists xA\to B$ is
in $\Gamma_{1}$, where $\exists x$ denotes a block of zero or more existential
quantifiers.

######  Definition.

Suppose ${\sf P}{\rm:}\forall x(p_{1}(x)\to\exists y\,p_{2}(x,y))$ and ${\sf
Q}{\rm:}\forall u(q_{1}(u)\to\exists v\,q_{2}(u,v))$ are problems. The
reduction prenex formula for ${\sf Q}\leq_{W}{\sf P}$ is the formula:

$S^{\sf P}_{\sf Q}:\forall u\exists x\forall y\exists
v(q_{1}(u)\to(p_{1}(x)\land(p_{2}(x,y)\to q_{2}(u,v))))$

If the problems are total, we can write $\sf P$ as $\forall x\exists
y\,p(x,y)$, $\sf Q$ as $\forall u\exists v\,q(u,v)$ and $S^{\sf P}_{\sf Q}$ as
$\forall u\exists x\forall y\exists v(p(x,y)\to q(u,v))$.

The implication $S^{\sf P}_{\sf Q}\to({\sf P}\to{\sf Q})$ is provable in
intuitionistic predicate calculus, though the proof of the converse requires
classical logic. If the constituent formulas $p_{1}$, $p_{2}$, $q_{1}$, and
$q_{2}$ are all $\exists$-free, then the matrix of $S^{\sf P}_{\sf Q}$ is also
$\exists$-free and $S^{\sf P}_{\sf Q}$ is in $\Gamma_{1}$. This also holds for
total problems.

If $\sf P$ and $\sf Q$ are Weihrauch problems, we can formalize ${\sf
Q}\leq_{W}{\sf P}$ by asserting the existence of Skolem functions for the
existential quantifiers of $S^{\sf P}_{\sf Q}$. Using $\sf P$ and $\sf Q$ as
in the definition, the relation ${\sf Q}\leq_{W}{\sf P}$ can be translated
into the language of $i{\sf RCA}_{0}^{\omega}$ as:

$\exists\Phi\exists\Psi\forall u\forall
y(q_{1}(u)\to(p_{1}(\Phi(u))\land(p_{2}(\Phi(u),y)\to q_{2}(u,\Psi(y)))))$

Here the functionals $\Phi$ and $\Psi$ are of type $1\to 1$, which is our
primary motivation for working in higher order subsystems.

Using the preceding notation, we can present the following slightly modified
version of Theorem 1 of Hirst and Mummert [hm].

######  Theorem 1.

Suppose $\sf P$ and $\sf Q$ are problems and the reduction prenex formula
$S^{\sf P}_{\sf Q}$ is in $\Gamma_{1}$. Then $i{\sf RCA}_{0}^{\omega}\vdash
S^{\sf P}_{\sf Q}$ if and only if $i{\sf RCA}_{0}^{\omega}\vdash{\sf
Q}\leq_{W}{\sf P}$.

###### Proof.

The result follows from the application of Kohlenbach’s [kbook] proof mining
technology to extract terms corresponding to the Skolem functions. Only one
modification to the proof of Theorem 1 of Hirst and Mummert [hm] is needed.
The hypothesis of their theorem specifies that the matrix of $S^{\sf P}_{\sf
Q}$ is in $\Gamma_{1}$, which by the definition of $\Gamma_{1}$ is equivalent
to $S^{\sf P}_{\sf Q}\in\Gamma_{1}$. ∎

The following theorem is the intuitionistic analog of a conservation result of
Kohlenbach [k2001].

######  Theorem 2.

The system $i{\sf RCA}_{0}^{\omega}$ is conservative over $i{\sf RCA}_{0}$ for
second order formulas.

###### Proof.

Kohlenbach’s conservation result for ${\sf RCA}_{0}^{\omega}$ over ${\sf
RCA}_{0}$ appears as Proposition 3.1 in his article on higher order reverse
mathematics [k2001]. Kohlenbach’s proof is based on the formalization of the
extensional model of the hereditarily continuous functionals (ECF) as
presented in Section 2.6.5 of Troelstra’s book [troelstra]. The arguments of
Troelstra (e.g. 2.6.12 and 2.6.20 of [troelstra]) are carried out in
intutionistic systems. Similarly, Kohlenbach’s proof holds for $i{\sf
RCA}_{0}^{\omega}$ and $i{\sf RCA}_{0}$. For other related discussion, see
Theorem 2.7 and Theorem 2.8 of Hirst and Mummert [hmunif]. ∎

###  1.1 Local graph coloring

The following encoding of graphs is useful in exploring graph coloring
problems. We can view a countable infinite graph as having $\mathbb{N}$ as its
vertex set. Fix a primitive recursive bijective pairing function, $p$, mapping
$\mathbb{N}$ onto $\\{(a,b)\mid a<b\\}$, the subset of
$\mathbb{N}\times\mathbb{N}$ consisting of increasing pairs. Both $p$ and
$p^{-1}$ can be defined in such a way that $i{\sf RCA}_{0}^{\omega}$ proves
their existence and salient properties. Using this pairing function, any
function $e:\mathbb{N}\to\mathbb{N}$ can be viewed as a characteristic
function for the edge set of a graph $G$. If $e(n)\neq 0$ then the edge $p(n)$
is in $G$, and if $e(n)=0$ then $p(n)$ is not in $G$. We will conflate $G$
with the set of codes for the edges of $G$ and write $(a,b)\in G$ as a
shorthand for $e(p^{-1}(a,b))\neq 0$.

For any graph $G$ and any $m$, let $G_{m}$ denote the finite subgraph with
vertices $\\{0,\dots,m\\}$ and edge set $\\{(a,b)\mid a<b\leq m\land(a,b)\in
G\\}$. We say that $G_{m}$ has a $k$-coloring if there is a finite function
$f:m\to k$ such that for all $a<b\leq m$, $(a,b)\in G$ implies $f(a)\neq
f(b)$. Informally, vertices connect by an edge must have distinct colors. The
existence of $k$-colorings for (initial) finite subgraphs can be formulated as
a problem.

###### LG$k$

(Local $k$-coloring for graphs): Fix $k$. For a graph $G$ (encoded by a
characteristic function for its edge set), there is a value ${\sf LG}{k}(G)$
such that ${\sf LG}{k}(G)=0$ implies that for every $m$ the subgraph $G_{m}$
has a $k$-coloring, and ${\sf LG}{k}(G)=m>0$ implies that $G_{m}$ has no
$k$-coloring and $G_{m-1}$ has a $k$-coloring.

Let $c(G,m)$ denote a primitive recursive function such that $c(G,m)=1$ if
$G_{m}$ has a $k$-coloring and $c(G,m)=0$ if $G_{m}$ has no $k$-coloring.
Using this function, we can formalize the predicate ${\sf LG}{k}(G)=n$ as the
following $\exists$-free formula,

$\begin{split}(n=0\to\forall m(c(G,m)=1))\land&\\\
(n>1\to(c(G,n)=&0\land\forall t(t<n\to c(G,t)=1)))\end{split}$

and note that ${\sf LG}{k}$ is a total problem of the form $\forall G\exists
n({\sf LG}{k}(G)=n)$. We will compare ${\sf LG}{k}$ to a version of the
limited principle of omniscience.

###### LPO

(Limited principle of omniscience): For every $p:\mathbb{N}\to\mathbb{N}$
there is a value ${\sf{LPO}}(p)$ such that ${\sf{LPO}}(p)=0$ implies that
$\forall k~{}p(k)>0$, and ${\sf{LPO}}(p)=m>0$ implies that $p(m-1)=0$ and for
all $t<(m-1)$, $p(t)>0$.

We can formalize the predicate ${\sf{LPO}}(p)=n$ as the following
$\exists$-free formula,

$(n=0\to\forall k(p(k)>0))\land(n>0\to(p(n-1)=0\land\forall t(t<(n-1)\to
p(t)>0)))$

and note that ${\sf{LPO}}$ is a total problem of the form $\forall p\exists
n({\sf{LPO}}(p)=n)$. This version of ${\sf{LPO}}$ differs from that presented
in the survey by Brattka, Gherardi, and Pauly [bgp]. It is Weihrauch
equivalent to their version, but not strongly Weihrauch equivalent, as the
range of their version includes only $\\{0,1\\}$ and the range of this version
includes all of $\mathbb{N}$. However, for our purposes it is desirable to
have the underlying predicate be $\exists$-free.

######  Lemma 3.

$(i{\sf RCA}_{0}^{\omega})$ For each $k\geq 1$, both $S^{{\sf
LG}{k}}_{\sf{LPO}}$ and $S^{\sf{LPO}}_{{\sf LG}{k}}$ hold.

###### Proof.

Because both ${\sf{LPO}}$ and ${\sf LG}{k}$ are total, we can use the simple
form of the reduction prenex formula. Thus $S^{{\sf LG}{k}}_{\sf{LPO}}$ is

$\forall p\exists G\forall y\exists v({\sf LG}{k}(G)=y\to{\sf{LPO}}(p)=v).$

To prove this in $i{\sf RCA}_{0}^{\omega}$, fix an instance $p$ of
${\sf{LPO}}$. Define the graph $G$ as follows. For each $m$, if $p(m)=0$, add
the edges $\\{(s,t)\mid m\leq s<t\leq m+k\\}$ to $G$. These edges form a
complete subgraph on $k+1$ vertices, precluding any $k$-coloring of $G_{m+k}$.
If $p(m)\neq 0$, add no new edges to $G$. By this construction, if ${\sf
LG}{k}(G)=0$, then for all $m$, $p(m)>0$, so ${\sf{LPO}}(p)=0$. On the other
hand, if ${\sf LG}{k}(G)=m>0$, then $m=n+k$ for some $n\geq 0$, and $p(n)=0$,
so ${\sf{LPO}}(p)=n+1=m-k+1$.

To show that $S^{{\sf{LPO}}}_{{\sf LG}{k}}$, fix a graph $G$. Define an
instance $p$ of ${\sf{LPO}}$ as follows. For each $m$, if the subgraph $G_{m}$
has a $k$-coloring, let $p(m)=1$. If $G_{m}$ has no $k$-coloring, let
$p(m)=0$. The truncated subtraction ${\sf{LPO}}(p)\frac{\cdot}{~{}~{}}1$
yields a correct output for ${\sf LG}{k}(G)$. ∎

By formalizing the transitivity of Weihrauch reduction we can extract
additional results from the preceding lemma.

######  Lemma 4.

$(i{\sf RCA}_{0}^{\omega})$ If ${\sf P}\leq_{W}{\sf Q}$ and ${\sf
Q}\leq_{W}{\sf R}$, then ${\sf P}\leq_{W}{\sf R}$.

###### Proof.

This is a formalization of the well-known property for Weihrauch reductions.
The system $i{\sf RCA}_{0}^{\omega}$ can prove that compositions of given
functionals exist, so the usual proof holds. ∎

######  Theorem 5.

$(i{\sf RCA}_{0}^{\omega})$ For any $j\geq k\geq 1$, ${\sf{LPO}}\equiv_{W}{\sf
LG}{k}\equiv_{W}{\sf LG}{j}$.

###### Proof.

By our formalization of ${\sf{LPO}}$ and ${\sf LG}{k}$, the corresponding
predicates are $\exists$-free. Consequently, both $S^{{\sf LG}{k}}_{\sf{LPO}}$
and $S^{{\sf{LPO}}}_{{\sf LG}{k}}$ are in $\Gamma_{1}$. Applying Theorem 1 to
the implications of Lemma 3 yields proofs in $i{\sf RCA}_{0}^{\omega}$ that
${\sf{LPO}}\leq_{W}{\sf LG}{k}$, ${\sf LG}{k}\leq_{W}{\sf{LPO}}$, and so
${\sf{LPO}}\equiv_{W}{\sf LG}{k}$. This holds for all $j$ and $k$, so by Lemma
4 we have ${\sf LG}{k}\equiv_{W}{\sf LG}{j}$. ∎

One noteworthy consequence of the preceding theorem is the provability of the
Weihrauch equivalence of ${\sf LG}{2}$ and ${\sf LG}{3}$ in $i{\sf
RCA}_{0}^{\omega}$. The finite combinatorial analogs of these problems are
2-colorability and 3-colorability of finite graphs, which are respectively
polynomial time computable and NP complete. As was the case in the traditional
reverse mathematics and computability theoretic analysis of Hirst and Lempp
[hl], formal Weihrauch analysis of the related infinite problems does not
distinguish between these problems. The current setting does allow us to apply
techniques of Weihrauch analysis, like the application of Lemma 4 in the
preceding proof to obtain formal equivalences, and then to translate these
into proofs of implications in weak subsystems, as in the following corollary.

######  Corollary 6.

$(i{\sf RCA}_{0}^{\omega})$ For every pair of problems $\sf P$ and $\sf Q$
from the list in Theorem 5, $S^{\sf P}_{\sf Q}$ holds. Furthermore, the
implication ${\sf P}\to{\sf Q}$ holds.

###### Proof.

As noted above, the formulas $S^{\sf P}_{\sf Q}$ of Theorem 5 are in
$\Gamma_{1}$. Applying the reverse implication Theorem 1 to the equivalences
of Theorem 5 proves $S^{\sf P}_{\sf Q}$. To justify the final sentence, note
that these are total problems and can be written as $\Pi^{1}_{1}$ formulas.
Over intuitionistic predicate calculus, $S^{\sf P}_{\sf Q}$ implies ${\sf
P}\to{\sf Q}$. ∎

If $\sf P$ is a problem, the parallelization of $\sf P$, denoted by
$\widehat{\sf P}$ is the problem that accepts as input any infinite sequence
of inputs for $\sf P$, and outputs the associated infinite sequence of
solutions for the input instances. The following lemma is a formalization of a
portion of part 3 of Proposition 3.6 of Brattka, Gherardi, and Pauly [bgp].

######  Lemma 7.

$(i{\sf RCA}_{0}^{\omega})$ ${\sf P}\leq_{W}{\sf Q}$ implies
$\widehat{\sf{P}}\leq_{W}\widehat{\sf{Q}}$.

###### Proof.

Suppose that $\Phi$ and $\Psi$ are the functionals witnessing ${\sf
P}\leq_{W}{\sf Q}$. If $\vec{u}=\langle u_{i}\rangle_{i\in\mathbb{N}}$ is an
input for $\widehat{\sf Q}$, define $\hat{\Phi}$ by
$\hat{\Phi}(\vec{u})=\langle\Phi(u_{i})\rangle_{i\in\mathbb{N}}$. Define
$\hat{\Psi}$ similarly. Note that $i{\sf RCA}_{0}^{\omega}$ suffices to prove
the existence of $\hat{\Phi}$ and $\hat{\Psi}$, and also proves that they
witness $\widehat{\sf{P}}\leq_{W}\widehat{\sf{Q}}$. ∎

######  Theorem 8.

$(i{\sf RCA}_{0}^{\omega})$ For every $k\geq 1$,
$\widehat{\sf{LPO}}\equiv_{W}\widehat{{\sf LG}{k}}$.

###### Proof.

Apply Lemma 7 to Theorem 5. ∎

If $\langle f_{i}\rangle_{i\in\mathbb{N}}$ is a sequence of input functions
for $\widehat{\sf{LPO}}$, we can define a type 1 function on (codes of pairs
of) natural numbers by $f(i,n)=f_{i}(n)$ and think of $f$ as a type 1 input
for $\widehat{\sf{LPO}}$. This modification allows us to think of
$\widehat{\sf{LPO}}$ as a $\Pi^{1}_{2}$ formula of second order arithmetic.
Similarly, we will conflate $\widehat{{\sf LG}{k}}$ with its second order
analog.

######  Corollary 9.

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

  1. (1)

${\sf ACA}_{0}$.

  2. (2)

$\widehat{{\sf{LPO}}}$

  3. (3)

$\widehat{{\sf LG}{k}}$, where $k\geq 1$.

###### Proof.

The equivalence of parts (2) and (3) follows from the application of Theorem 1
to the Weihrauch reductions included in Theorem 8, and the fact that $S^{\sf
P}_{\sf Q}\to({\sf P}\to{\sf Q})$. To show that (1) implies (2), let $\langle
f_{i}\rangle_{i\in\mathbb{N}}$ be an input for $\widehat{{\sf{LPO}}}$.
Arithmetical comprehension asserts the existence of the set $\\{i\mid\forall
n\,f_{i}(n)\neq 0\\}$ and the corresponding characteristic function, which is
a solution of the instance of $\widehat{{\sf{LPO}}}$.

To show that (2) implies (1), we adapt the familiar application of Lemma
III.1.3 of Simpson [simpson]. In $i{\sf RCA}_{0}$ it suffices to find the
range of an arbitrary function that is injective, except for possibly
repeatedly taking the value $0$. (This broader class of almost injective
functions avoids a use of classical logic in the proof of Lemma II.3.7, used
by Simpson [simpson] to prove the reversal.) Let $f$ be such a function.
Define the sequence of functions $\langle f_{i}\rangle_{i\in\mathbb{N}}$ by
$f_{i}(m)=1$ if $\forall t<m(f(t)\neq i)$ and $f_{i}(m)=0$ otherwise. The
solution to the $\widehat{{\sf{LPO}}}$ problem $\langle
f_{i}\rangle_{i\in\mathbb{N}}$ is the characteristic function of the range of
$f$.

Finally, the formulas of Corollary 9 are all second order, so by Theorem 2 the
equivalences are provable in the second order system $i{\sf RCA}_{0}$. ∎

Summarizing, we used higher order formalized Weihrauch techniques in Lemma 7
and extracted traditional second order reverse mathematics results in
Corollary 9.

###  1.2 Colorings as outputs

We can reformulate the graph coloring problems so that the outputs are
infinite graph colorings. We will continue to use the notation of the previous
subsection. In particular, $G_{m}$ denotes the finite subgraph of $G$
consisting of the first $m+1$ vertices and their edges in $G$.

###### GC$k$

($k$-coloring of graphs): If $e:\mathbb{N}\to\mathbb{N}$ codes the edge set
for a graph $G$ and every finite subgraph $G_{m}$ has a $k$-coloring, then
there is a function $f:\mathbb{N}\to k$ that is a $k$-coloring of $G$.

The predicate asserting that $G_{m}$ is $k$-colorable can be written using
bounded quantifiers, with $G$, $k$, and $m$ as parameters. The system $i{\sf
RCA}_{0}^{\omega}$ proves the existence of the primitive recursive
characteristic functional for this predicate, so the assertion that every
$G_{m}$ has a $k$-coloring can be formalized with a $\exists$-free formula.
Note that $f$ is a $k$-coloring of $G$ if and only if for each $i\neq j$, if
$(i,j)$ is an edge in $G$ then $f(i)\neq f(j)$, which is also $\exists$-free.
Thus we can write an $\exists$-free formula ${\sf{GC}}k(G,f)$ asserting that
$f$ is the solution to the ${\sf{GC}}k$ problem for $G$.

In our study of problems involving infinite trees, we will use the the
following encoding. Fix a suitable bijective coding function ${\sf seq}$
mapping $\mathbb{N}$ onto $2^{<\mathbb{N}}$, the set of finite sequences of
zeros and ones. Any function $t:\mathbb{N}\to\mathbb{N}$ can be viewed as a
code for a binary tree $T$ using the following convention. The finite sequence
${\sf seq}(n)$ is in $T$ if and only if $t(n)>0$ and for every initial segment
$\sigma$ of ${\sf seq}(n)$, $t({\sf seq}^{-1}(\sigma))>0$. Informally, the
function $t$ is the characteristic function for a set that includes the
sequences of $T$ and omits the immediate successors of any leaves of $T$.
Using this encoding, we have the following formalization of Weak Königs’s
Lemma as a total problem.

###### WKL

(Weak König’s Lemma): If $T$ is a binary tree and for every $m$ there is a
sequence $\sigma\in T$ of length $m$, then there is a function $p$ that codes
an infinite path through $T$.

In the previous formalization, $p$ can be viewed as a code for a subtree $P$
of $T$ such that each node in $P$ has precisely one immediate successor. Using
our standard techniques for representing primitive recursive functionals, it
is easy to formalize the assertion that for every $m$ the tree $T$ contains a
binary sequence of length $m$ as an $\exists$-free formula. Note that the
bound on the labels is essential for this. The claim that $p$ is an infinite
path is a universal statement, so we can write an $\exists$-free formula
${\sf{WKL}}(T,f)$ asserting that $f$ is a solution to the $\sf{WKL}$ problem
for $T$.

For values of $n$ greater than $2$, we can use a bijective coding ${\sf
seq}_{n}$ of sequences of numbers less than $n$, and formulate a corresponding
version of ${\sf WKL}$.

###### WKL$n$

(Weak König’s Lemma for trees in $n^{<\mathbb{N}}$): If $T$ is a tree with
nodes labeled with numbers less than $n$, and for every $m$ there is a
sequence $\sigma\in T$ of length $m$, then there is a function $p$ that codes
an infinite path through $T$.

Note that ${\sf WKL}$ and ${\sf WKL}{2}$ denote the same problem. As with
${\sf WKL}$, we can formalize ${\sf WKL}{2}$ in the language of $i{\sf
RCA}_{0}^{\omega}$ with an $\exists$-free formula.

######  Lemma 10.

$(i{\sf RCA}_{0})$ For each $n\geq 2$, $S^{{\sf WKL}}_{{\sf WKL}n}$ and
$S^{{\sf WKL}n}_{{\sf WKL}}$ hold.

###### Proof.

For $n\geq 2$, every binary tree is an $n$-ary tree, so $S^{{\sf WKL}n}_{{\sf
WKL}}$ holds trivially. To prove $S^{{\sf WKL}}_{{\sf WKL}n}$, let $T$ be an
$n$-ary tree. Any sequence of $m$ values less than or equal to $n$ can be
mapped to a binary sequence of length $m\cdot n$ in the manner of the
following example. Consider $\langle 2,0,3\rangle$ as a sequence of numbers
less than or equal to $3$. Replace each value $k$ with a block of length $3$
consisting of $k$ ones padded on the right with zeros. In our example $\langle
2,0,3\rangle$ becomes $\langle 1,1,0,\,\,0,0,0,\,\,1,1,1\rangle$. This process
transforms any $n$-ary tree $T$ into a binary tree that is well-founded if and
only if $T$ is. Furthermore, summing successive length $n$ blocks of any
infinite path through the binary tree yields a path through $T$. ∎

We will use the following formalization of ${\sf LLPO}$, which is defined for
all functions from $\mathbb{N}$ into $\mathbb{N}$. Naïvely, if a function $p$
has a positive value, then ${\sf LLPO}$ returns the flip of the parity of that
first positive value.

###### LLPO

(Lesser limited principle of omniscience): For any $p:\mathbb{N}\to\mathbb{N}$
there is a value ${\sf LLPO}(p)$ such that ${\sf LLPO}(p)=0$ implies if
$p(j)\neq 0$ and $\forall t<j(p(j)=0)$ then $j$ is odd, and ${\sf LLPO}(0)\neq
0$ implies ${\sf LLPO}(p)=1$ and if $p(j)\neq 0$ and $\forall t<j(p(j)=0)$
then $j$ is even.

Our definition is chosen so that for functions $p$ with ranges that are non-
zero in at most one place, the value of ${\sf LLPO}(p)$ matches the definition
of Brattka, Gherardi, and Pauly [bgp]*§7.2. By mapping functions from
$\mathbb{N}$ to $\mathbb{N}$ to the characteristic function for the least
element of their domain taking a positive value, routine verification shows
that our total version of ${\sf LLPO}$ is strongly Weihrauch equivalent to
their version.

The predicate “$j$ is odd” can be formalized by $\forall m(j\neq 2m)$.
Similarly, “$j$ is even” can be formalized by $\forall m(j\neq 2m+1)$.
Consequently, ${\sf LLPO}(p)=n$ can be formalized by the $\exists$-free
formula:

$\displaystyle(n=0\to\forall j([p(j)\neq 0\land\forall t(t<j\to
p(t)=0)]\to\forall m(j\neq 2m)))\land$ $\displaystyle(n\neq
0\to(n=1\land\forall j([p(j)\neq 0\land\forall t(t<j\to p(t)=0)]\to\forall
m(j\neq 2m+1))))$

The problem ${\sf LLPO}$ can be parallelized, resulting in a problem that is
Weihrauch equivalent to ${\sf WKL}$, as noted in part of Theorem 7.23 of
Brattka, Gherardi, and Pauly [bgp]. The following results lead to a
formalization of a fragment of their theorem, and its connection to graph
colorings.

######  Lemma 11.

$(i{\sf RCA}_{0})$ $S^{\sf\widehat{\sf LLPO}}_{\sf{\sf WKL}}$ holds.

###### Proof.

To prove $S^{\widehat{\sf LLPO}}_{{\sf WKL}}$, suppose $T$ is a binary tree.
For every $\sigma\in 2^{<\mathbb{N}}$, define the instance $p_{\sigma}$ of
${\sf LLPO}$ as follows. If $\sigma\notin T$, then for each $n$, $p(n)=0$. For
$\sigma\in T$, let $p_{\sigma}(0)=p_{\sigma}(1)=0$. For $n>0$, define
$p_{\sigma}(2n)$ and $p_{\sigma}(2n+1)$ as follows. If
$\sigma{{}^{\smallfrown}}0$ has an extension of length $n$ in $T$ and
$\sigma{{}^{\smallfrown}}1$ has no extension of length $n$ in $T$, let
$p_{\sigma}(2n)=0$ and $p_{\sigma}(2n+1)=1$. If $\sigma{{}^{\smallfrown}}1$
has an extension of length $n$ in $T$ and $\sigma{{}^{\smallfrown}}0$ has no
extension of length $n$ in $T$, let $p_{\sigma}(2n)=1$ and
$p_{\sigma}(2n+1)=0$. Otherwise, let $p_{\sigma}(2n)=p_{\sigma}(2n+1)=0$.

If $\sigma{{}^{\smallfrown}}0$ extends to an infinite path, but
$\sigma{{}^{\smallfrown}}1$ does not, then there is a first $n>0$ such that
$\sigma{{}^{\smallfrown}}1$ has no extensions of length $n$. In this case,
${\sf LLPO}(p_{\sigma})=0$. Similarly, if $\sigma{{}^{\smallfrown}}1$ extends
to an infinite path but $\sigma{{}^{\smallfrown}}0$ does not, ${\sf
LLPO}(p_{\sigma})=1$. Thus, if $T$ is infinite, the sequence constructed by
setting $\sigma(0)={\sf LLPO}(\langle\,\rangle)$ and
$\sigma(n+1)=\sigma(n){{}^{\smallfrown}}{\sf LLPO}(\sigma(n))$ for $n\geq 0$
is an infinite path through $T$. ∎

######  Lemma 12.

$(i{\sf RCA}_{0})$ $S^{{\sf GC}{2}}_{\widehat{\sf LLPO}}$.

###### Proof.

Suppose $p_{i}$ is an instance of ${\sf LLPO}$. Construct a subgraph $G_{i}$
with vertices $u_{i}$ and $\\{v_{i,0},v_{i,1},\dots\\}$ as follows. For all
$k$, include the edge $(v_{i,k},v_{i,k+1})$. If $j$ is the least natural
number such that $p_{i}(j)\neq 0$, add the edge $(u_{i},v_{i,j})$. For any
2-coloring of $G_{i}$, if $u_{i}$ and $v_{i,0}$ differ in color, then $1$ is a
correct output for ${\sf LLPO}$. If $u_{i}$ and $v_{i,0}$ agree in color, then
$0$ is a correct output. For a sequence of instances of ${\sf LLPO}$, let $G$
consist of the disjoint union of the graphs for each sequence. Any two
coloring of $G$ yields a solution to the instance of $\widehat{\sf LLPO}$. ∎

######  Lemma 13.

$(i{\sf RCA}_{0})$ For $n\geq 2$, $S^{{\sf GC}{n}}_{{\sf GC}{2}}$.

###### Proof.

Suppose $G$ is a locally $2$-colorable graph. For $n>2$, create a single copy
of the complete graph on $n-2$ vertices, and connect each of its vertices to
every vertex of $G$. The new graph is locally $n$-colorable, and the
restriction of any $n$-coloring to the vertices of $G$ yields a $2$-coloring
of $G$. ∎

######  Lemma 14.

$(i{\sf RCA}_{0})$ For $n\geq 2$, $S^{{\sf WKL}{n}}_{{\sf GC}{n}}$ holds.

###### Proof.

For any locally $n$-colorable graph $G$, $i{\sf RCA}_{0}$ can prove that the
tree of sequences corresponding to $n$-colorings of the finite subgraphs
$G_{m}$ is an instance of ${\sf WKL}{n}$. ∎

We can concatenate the lemmas to yield our main theorem on Weihrauch
equivalences related to graph colorings.

######  Theorem 15.

$(i{\sf RCA}_{0}^{\omega})$ For $n\geq 2$, we have:

${\sf WKL}{n}\equiv_{W}{\sf WKL}\equiv_{W}\widehat{\sf LLPO}\equiv_{W}{\sf
GC}{n}\equiv_{W}{\sf GC}{2}$

###### Proof.

Applying Theorem 1 to Lemma 10 and Lemma 11, we have ${\sf WKL}{n}\leq_{W}{\sf
WKL}\leq_{W}\widehat{{\sf LLPO}}$. Applying Theorem 1 to Lemma 12, Lemma 13,
and Lemma 14 yields $\widehat{{\sf LLPO}}\leq_{W}{\sf GC}{2}\leq_{W}{\sf
GC}{n}\leq_{W}{\sf WKL}{n}$. The theorem follows by transitivity as provided
by Lemma 4. ∎

Given the formal Weihrauch reductions, we can extract the reverse mathematics
consequences.

######  Corollary 16.

$(i{\sf RCA}_{0})$ The formula $S^{\sf P}_{\sf Q}$ holds for every problem
$\sf P$ and problem $\sf Q$ appearing in Theorem 15. Furthermore the
implication ${\sf P}\to{\sf Q}$ holds.

###### Proof.

Imitate the proof of Corollary 6. ∎

######  Corollary 17.

$(i{\sf RCA}_{0})$ For $k\geq 2$, the following are equivalent:

  1. (1)

${\sf WKL}$.

  2. (2)

$\widehat{\sf LLPO}$.

  3. (3)

${\sf WKL}{k}$

  4. (4)

${\sf GC}{k}$.

###### Proof.

Immediate from Corollary 16. ∎

Parallelization of ${\sf GC}{k}$ results in a Weihrauch equivalent problem.
This arises from the well-known idempotence of the parallelization operator,
which can be verified in the formal setting.

######  Lemma 18.

$(i{\sf RCA}_{0}^{\omega})$ The hat operator is idempotent, that is, for any
problem $\sf P$, $\widehat{\sf P}\equiv_{W}\widehat{\widehat{\sf P}}$.
Consequently, for $k\geq 2$, ${\sf GC}{k}\equiv_{W}\widehat{{\sf GC}{k}}$.

###### Proof.

In $i{\sf RCA}_{0}^{\omega}$, we can use the bijective pairing function to
match each pair $(i,j)$ with an integer code. Given a sequence of sequences of
problems $\langle\langle p_{i,j}\mid j\in\mathbb{N}\rangle
i\in\mathbb{N}\rangle$, we match each problem with an element of the sequence
$\langle p_{(i,j)}\mid(i,j)\in\mathbb{N}\rangle$. Thus $\widehat{\widehat{\sf
P}}\leq_{W}\widehat{\sf P}$. The reverse reduction is trivial.

From Theorem 15 we know that ${\sf GC}{k}\equiv_{W}\widehat{\sf LLPO}$. By
Lemma 7, $\widehat{{\sf GC}{k}}\equiv_{W}\widehat{\widehat{\sf LLPO}}$. From
the preceding paragraph, $\widehat{\widehat{\sf LLPO}}\equiv_{W}\widehat{\sf
LLPO}$, so the desired equivalence follows by transitivity. ∎

In combination with Theorem 15 we see that $\widehat{{\sf
GC}{2}}\equiv_{W}\widehat{{\sf GC}{3}}$. These problems correspond to reverse
mathematical statements about infinite sequences of 2-colorings and
3-colorings reminiscent of those of Hirst and Lempp [hl]. The corresponding
reverse mathematical results can be extracted in the usual fashion, yielding
the following corollary.

######  Corollary 19.

$(i{\sf RCA}_{0})$ For $k\geq 2$, ${\sf WKL}$ is equivalent to the assertion
that for any sequence ${\langle G_{i}\rangle}_{i\in\mathbb{N}}$ of infinite
locally $k$-colorable graphs, there is a function
$f:\mathbb{N}\times\mathbb{N}\to\mathbb{N}$ such that for each $i$, the
function $f(i,n)$ is a $k$-coloring of $G_{i}$.

The $k$-coloring problem defined at the beginning of this subsection does not
accept inputs which are not locally $k$-colorable. The following alternative
definition extends the possible inputs to all graphs.

###### TGC$k$

(Total $k$-coloring of graphs): Given a graph $G$, there is a function
$f:\mathbb{N}\to\mathbb{N}$ such that $f(0)=0$ implies $f$ is a $k$-coloring
of $G$ and $f(0)>0$ implies $G_{f(0)}$ has no $k$-coloring.

The predicate asserting that $f$ solves ${\sf TGC}{k}$ for $G$ can be
formalized as a $\exists$-free formula in the parameters $k$, $f$, and $G$.
Altering the problem affects the Weihrauch analysis.

######  Theorem 20.

$(i{\sf RCA}_{0}^{\omega})$ For $k\geq 2$, ${\sf{LPO}}\leq_{W}{\sf
TGC}{k}\leq_{W}\widehat{\sf{LPO}}$.

###### Proof.

For the first reduction, fix $k$ and suppose $p$ is an instance of
${\sf{LPO}}$. Let $G$ be the graph which is completely disconnected except for
a completely connected subgraph on the vertices $\\{m,m+1,\dots,m+k\\}$ if
$p(m)=0$ and $\forall t<m(p(m)\neq 0)$, if such an $m$ exists. The
characteristic function for the edges of $G$ is uniformly computable from $p$.
Suppose $f$ is a solution of ${\sf TGC}{k}$ for $G$. Then $f(0)=0$ if and only
if $\forall k(p(k)\neq 0)$. Also, if there is a least $m$ such that $p(m)=0$,
then $G_{m+k}$ is the first initial subgraph of $G$ with no $k$-coloring. In
this case, $f(0)=m+k$ and the solution to the ${\sf{LPO}}$ problem $p$ is
obtained by subtracting the fixed value $k$.

For the second reduction, suppose $G$ is a graph. Let $p_{0}(n)=1$ if for all
$t\leq n$ the initial subgraph $G_{k}$ has a $k$-coloring, and let
$p_{0}(n)=0$ otherwise. For $i>0$, define $p_{i}$ as follows. Let
$\sigma_{1},\sigma_{2},\dots$ be the finite sequences in $k^{<\mathbb{N}}$
that start with $0$ and occur in the tree of initial segments of $k$ colorings
of $G$. If there are only finitely many such sequences, pad the list with
copies of the empty sequence. Let $p_{i}(m)=1$ if $\sigma_{i}$ extends to a
$k$-coloring of $G_{m}$, and let $p_{i}(m)=0$ otherwise. Given a solution to
the $\widehat{\sf{LPO}}$ problem $\langle p_{i}\rangle_{i\in\mathbb{N}}$, we
can compute a solution $f$ to ${\sf TGC}{k}$ for $G$ as follows. Let
$f(0)={\sf{LPO}}(p_{0})$. If $f(0)>0$, let $f(n)=0$ for all $n>0$. Otherwise,
use the values of ${\sf{LPO}}(p_{n})$ for $n>0$ to enumerate the nodes in a
path through the tree of partial colorings and assign the values of $f$ to
match the nodes in the path. This enumeration is computable because if
${\sf{LPO}}(p_{n})=0$, then the tree of partial $k$-colorings extending
$\sigma_{n}$ is infinite, and there is a least $m$ such that there is a $j<k$
with $\sigma_{m}=\sigma_{n}^{\frown}j$ and ${\sf{LPO}}(p_{m})=0$. ∎

######  Corollary 21.

$(i{\sf RCA}_{0}^{\omega})$ For $k\geq 2$, $\widehat{{\sf
TGC}{k}}\equiv_{W}\widehat{\sf{LPO}}$ and $\widehat{{\sf
GC}{k}}\equiv_{W}\widehat{\sf LLPO}$.

###### Proof.

Apply parallelization and idempotence to the reductions in Corollary 21 and
Corollary 17. ∎

Because the associated predicates are $\exists$-free, the Weihrauch results of
Corollary 21 can be converted to a reverse mathematics result after the
fashion of Corollary 19.

######  Corollary 22.

$(i{\sf RCA}_{0})$ For $k\geq 2$, ${\sf ACA}_{0}$ is equivalent to the
assertion that for any sequence ${\langle G_{i}\rangle}_{i\in\mathbb{N}}$ of
graphs, there is a function $f:\mathbb{N}\times\mathbb{N}\to\mathbb{N}$ such
that for each $i$, either $f(i,0)=m>0$ and the $m^{\text{th}}$ initial
subgraph of $G_{i}$ is not $k$-colorable or $f(i,0)=0$ and the function
$f(i,n)$ is a $k$-coloring of $G_{i}$.

The previous corollary again demonstrates the use of formal Weihrauch
techniques to derive reverse mathematical results. We close this section by
illustrating a limitation of the formal approach. In traditional Weihrauch
analysis, we can show that ${\sf P}\not\leq_{W}{\sf Q}$ by showing that there
are no computable functionals witnessing the reduction. The formal setting
does not distinguish between computable witnesses and other functionals, so
there is no analogous argument. Consequently, results about strict Weihrauch
reducibility are not amenable to formalization in $i{\sf RCA}_{0}^{\omega}$.

######  Corollary 23.

For $k\geq 2$, $i{\sf RCA}_{0}^{\omega}$ proves ${\sf GC}{k}\leq_{W}{\sf
TGC}{k}$. In the non-formal setting, ${\sf GC}{k}<_{W}{\sf TGC}{k}$.

###### Proof.

$i{\sf RCA}_{0}^{\omega}$ proves that ${\sf GC}{k}\leq_{W}{\sf TGC}{k}$ using
the identity functionals as witnesses. To prove the strict inequality of the
second sentence, we may use classical logic and results from the Weihrauch
reducibility literature. Suppose by way of contradiction that ${\sf
TGC}{k}\leq_{W}{\sf GC}{k}$. Parallelization preserves the reduction. By
Corollary 21 and transitivity, $\widehat{\sf{LPO}}\leq_{W}\widehat{\sf LLPO}$,
contradicting widely known results (e.g. Theorems 7.23, 7.40, and 7.42 in
[bgp]).∎

##  2 Weihrauch analysis related to ${\Pi^{1}_{1}{\text{-}}{\sf{CA}}_{0}}$

In this section, we apply more traditional techniques of Weihrauch analysis to
problems from [hl]. The underlying formulas are not $\exists$-free, so the
techniques of the preceding section are not applicable. The problems are all
related to ${\Pi^{1}_{1}{\text{-}}{\sf{CA}}_{0}}$. The first is based on Lemma
VI.1.1 of Simpson [simpson].

###### ${\sf WF}$

(Well founded trees): Given a tree $T$ in $\mathbb{N}^{<\mathbb{N}}$ as input,
output $0$ if $T$ contains an infinite path and $1$ if it does not.

The next two problems are based on principles included in Theorem 3.4 of Hirst
and Lempp [hl].

###### ${\sf S}$

(Isomorphic subgraph): Given inputs of graphs $G$ and $H$, output $1$ if $H$
is isomorphic to a subgraph of $G$ and $0$ if it is not.

Let $L$ denote the linear graph with vertex set $V=\\{v_{i}\mid
i\in\mathbb{N}\\}$ and edges $E=\\{(v_{i},v_{i+1})\mid i\in\mathbb{N}\\}$.

###### ${\sf S}_{L}$

($L$ as a subgraph): Given a graph $G$ as input, output $1$ if $L$ is
isomorphic to a subgraph of $G$ and $0$ if it is not.

######  Theorem 24.

${\sf WF}\equiv_{sW}{\sf S}_{L}\equiv_{sW}{\sf S}$.

###### Proof.

First we will show that ${\sf WF}\leq_{sW}{\sf S}_{L}$. Any tree $T$ in
$\mathbb{N}^{<\mathbb{N}}$ can uniformly be converted to a corresponding
graph, with the nodes of the tree as vertices and edges between neighboring
nodes. Note that the tree $T$ contains an infinite path if and only if the
linear graph $L$ is isomorphic to a subgraph of the graph of $T$. The output
$1-{\sf S}_{L}(T)$ is equal to ${\sf WF}(T)$, so the post-processing does not
depend on $T$ and the reduction is strong.

The problem ${\sf S}_{L}$ is a special case of $\sf S$, so it only remains to
show that ${\sf S}\leq_{sW}{\sf WF}$. Suppose $G$ and $H$ are input graphs
with vertices $\\{g_{i}\mid i\in\mathbb{N}\\}$ and $\\{h_{i}\mid
i\in\mathbb{N}\\}$. We can uniformly compute the tree $T$ of initial segments
of isomorphisms between $H$ and subgraphs of $G$, where nodes correspond to
sequences $g_{i_{0}},\dots,g_{i_{n}}$ such that the pairing of nodes
$g_{i_{j}}$ and $h_{j}$ for $j\leq n$ is an isomorphism of the induced
subgraph of $H$ with a subgraph of $G$. Any infinite path through $T$ is an
isomorphism between $H$ and a subgraph of $G$. Thus $1-{\sf WF}(T)$ is equal
to ${\sf S}(G,H)$, yielding the final strong Weihrauch reduction. ∎

Theorem 3.4 of [hl] discusses sequences of graphs and trees. Similar Weihrauch
reductions follow by parallelization.

######  Corollary 25.

$\widehat{\sf{WF}}\equiv_{sW}\widehat{\sf S}_{L}\equiv_{sW}\widehat{\sf S}$.

###### Proof.

As noted in Proposition 3.6 part 3 of [bgp], parallelization is a strong
closure operation with respect to strong Weihrauch reducibility. The
parallelized equivalences follow immediately from the equivalences in Theorem
24. ∎

The proof of Theorem 3.4 of [hl] indicates that an instance of
$\widehat{\sf{WF}}$ can be related to isomorphic subgraph problems for a
single target graph $G$. Let $L_{n}$ denote the linear graph $L$ with a cycle
of size $n+3$ appended to the first vertex. For example, $L_{0}$ is a copy of
$L$ with a triangle attached as a tag to the first vertex.

###### ${\sf S}_{\vec{L}}$

(Tagged linear subgraphs of a fixed graph): Given a graph $G$ as input, output
a function $s:\mathbb{N}\to 2$ such that $s(n)=1$ if and only if $L_{n}$ is a
subgraph of $G$.

######  Theorem 26.

$\widehat{\sf{WF}}\equiv_{sW}{\sf S}_{\vec{L}}$.

###### Proof.

Note that an input $G$ for ${\sf S}_{\vec{L}}$ corresponds exactly to the
input ${\langle G,L_{i}\rangle}_{i\in\mathbb{N}}$ for $\widehat{\sf S}$. Thus
${\sf S}_{\vec{L}}\leq_{sW}{\widehat{\sf S}}\equiv_{sW}\widehat{\sf{WF}}$. To
show that $\widehat{\sf{WF}}\leq_{sW}{\sf S}_{\vec{L}}$, we adapt the reversal
from Theorem 3.4 of [hl]. Let ${\langle T_{i}\rangle}_{i\in\mathbb{N}}$ be an
input for $\widehat{\sf{WF}}$. For each $i$, let $G_{i}$ be the graph of
$T_{i}$ with a cycle of size $i+3$ attached to the root node. The graph $G$
consisting of the disjoint union of the $G_{i}$ graphs is uniformly computable
from ${\langle T_{i}\rangle}_{i\in\mathbb{N}}$. Note that $L_{i}$ is
isomorphic to a subgraph of $G$ if and only if $L_{i}$ is isomorphic to a
subgraph of $G_{i}$, which occurs exactly when $T_{i}$ is not well founded. If
$s:\mathbb{N}\to 2$ is a solution to ${\sf S}_{\vec{L}}$ for this graph $G$,
then $w(n)=1-s(n)$ is a solution of $\widehat{\sf{WF}}$ for ${\langle
T_{i}\rangle}_{i\in\mathbb{N}}$, completing the proof that
$\widehat{\sf{WF}}\leq_{sW}{\sf S}_{\vec{L}}$. ∎

Many other graphs could be substituted for the linear graph $L$ in the
preceding discussion. However, not all graphs yield the same results. For
example, while ${\sf S}_{L}\equiv_{sW}{\sf WF}$, finite graphs yield a weaker
Weihrauch problem.

######  Theorem 27.

Suppose that $F$ is a finite graph with at least two vertices. Then ${\sf
S}_{F}\equiv_{W}{\sf{LPO}}$.

###### Proof.

We will prove the result for the version of ${\sf{LPO}}$ from section §1.1.
For other versions of ${\sf{LPO}}$, the result can be strengthened to strong
Weihrauch reduction. Fix a finite graph $F$. To show that ${\sf
S}_{F}\leq_{W}{\sf{LPO}}$, let $G$ be an input graph and construct an input
for ${\sf{LPO}}$ as follows. For each $n$, if $F$ is not isomorphic to a
subgraph of $G$ restricted to the first $n$ vertices of $G$, set $p(n)=1$. If
$F$ is isomorphic to such a subgraph, set $p(n)=0$. Thus ${\sf S}_{F}(G)=1$ if
and only if ${\sf{LPO}}(p)>0$.

To prove that ${\sf{LPO}}\leq_{W}{\sf S}_{F}$, we will consider two cases.
First suppose that $F$ is a finite graph with $j$ vertices and at least one
edge. Let $p$ be an instance of ${\sf{LPO}}$. Let $G$ be the graph with
vertices $\\{v_{i}\mid i\in\mathbb{N}\\}$, and with edges corresponding to a
copy of $F$ on vertices $v_{m},\dots,v_{m+j-1}$ if $m$ is the least value such
that $p(m)=0$. If no such $m$ exists, then $G$ is completely disconnected.
Note that each edge of $G$ depends only on an initial segment of the values of
$p$, so $G$ is uniformly computable from $p$. If ${\sf S}_{F}(G)=0$, output
$0$ for ${\sf{LPO}}(p)$. If ${\sf S}_{F}(G)=1$, then the search for the least
$m$ such that $p(m)=0$ will succeed and the appropriate value of
${\sf{LPO}}(p)$ can be output.

The case when $F$ is completely disconnected is similar, using complementary
graphs. All possible edges are added to $G$ until a zero of $p$ is discovered,
at which point no additional edges are added. ∎

The fact that ${\sf S}_{F}\equiv_{W}{\sf{LPO}}$ and ${\sf S}_{L}\equiv_{W}{\sf
WF}$ motivates the following question: Is there a graph $H$ such that
${\sf{LPO}}<_{W}{\sf S}_{H}<_{W}{\sf WF}$? Arno Pauly says yes, if we switch
from isomorphism to subgraph embedding (SE). For the graph $H$ consisting of
infinitely many copies of K3, ${\sf SE}_{H}\equiv_{\sf W}{\sf{LPO}}^{\prime}$
[pauly]. Switching to embeddings does not change Theorem 24, for example. Reed
Solomon has asked what other reductions differ in strength for various notions
of embedding.

We can also consider the problem ${\sf S}^{G}$ for a fixed graph $G$, asking
whether or not an input graph is isomorphic to a subgraph of $G$. For the
complete graph $K$ and the totally disconnected graph $D$ it is easy to show
that ${\sf S}^{K}$ and ${\sf S}^{D}$ are both Weihrauch equivalent to
${\sf{LPO}}$. Theorem 3.2 of [hl] shows that there is a computable graph $G$
such that the set of indices of computable graphs that are isomorphic to a
subgraph of $G$ is $\Sigma^{1}_{1}$ complete. This prompts us to ask: Is there
a graph $G$ such that ${\sf S}^{G}\equiv_{sW}{\sf WF}$? Indeed, is there even
a graph $G$ such that ${\sf{LPO}}<_{W}{\sf S}^{G}$?

Theorem 2.6 of [hl] shows a connection between sequential versions of the
following problems. For a graph $G$ with vertex set $V$, we say
$c:V\to\mathbb{N}$ is a coloring of $G$ if whenever $(v_{1},v_{2})$ is an edge
of $G$, $c(v_{1})\neq c(v_{2})$.

###### $\sf{RC}$

(Repeated color): Given a graph $G$ as an input, output $1$ if there is a
coloring of $G$ that uses one color infinitely often and output $0$ if there
is no such coloring.

###### $\sf{D}$

(Disconnected subgraph): Given a graph $G$ as an input, output $1$ if $G$ has
an infinite completely disconnected subgraph and output $0$ otherwise.

######  Theorem 28.

${\sf RC}\equiv_{sW}{\sf D}\equiv_{sW}{\sf WF}$.

###### Proof.

Any graph $G$ has a coloring as required by $\sf RC$ if and only if it has a
subgraph as in $\sf D$. Thus ${\sf RC}\equiv_{sW}{\sf D}$. Overloading
notation and using $D$ to denote the totally disconnected graph, we have ${\sf
D}\equiv_{sW}{\sf S}_{D}$. The problem ${\sf S}_{D}$ is a special case of
${\sf S}$, so ${\sf D}\leq_{sW}{\sf S}\equiv_{sW}{\sf WF}$.

To show that ${\sf WF}\leq_{sW}{\sf S}_{D}$, given a tree $T$ as input, define
a graph $G$ as follows. The vertices of $G$ will consist of the nodes of $T$.
A pair $(v_{1},v_{2})$ is an edge in $G$ if and only if the corresponding
nodes of $T$ are incomparable. (Nodes of $T$ are comparable if one extends the
other in the tree.) $G$ is uniformly computable from $T$. The completely
disconnected graph $D$ is isomorphic to a subgraph of $G$ if and only if $T$
contains an infinite collection of pairwise comparable nodes, that is, if and
only if $T$ is not well founded. For $T$ and $G$ as described above, ${\sf
WF}(T)=1-{\sf S}_{D}(G)$, so ${\sf WF}\leq_{sW}{\sf S}_{D}$, as desired. ∎

Appending a triangle to each tree node in the previous construction yields a
proof that ${\sf WF}$ is Weihrauch equivalent to ${\sf S}_{G}$ for the graph
$G$ consisting of infinitely many disconnected triangles. (This was proven
independently by Arno Pauly [pauly].) Thus the graph from Pauly’s embedding
observation does not answer our question about isomorphic subgraphs.
Parallelizing the previous theorem yields Weihrauch equivalences mirroring the
reverse mathematics of Theorem 2.6 of [hl].

######  Corollary 29.

$\widehat{\sf RC}\equiv_{sW}\widehat{\sf D}\equiv_{sW}\widehat{\sf{WF}}$.

###### Proof.

Immediate from Theorem 28 by Proposition 3.6 part 3 of [bgp]. ∎

The application of Weihrauch analysis to the problems of this section yields
no new insights into the corresponding finite complexity theoretic
relationships. However, it does raise some new Weihrauch analysis questions.
Analyzing infinite versions of other statements from finite complexity theory
might lead to additional interesting Weihrauch reductions.

[Bibliography]

BrattkaVascoGherardiGuidoPaulyArnoWeihrauch complexity in computable
analysis20181–61available at arXiv:1808.03202v4@article{bgp, author =
{Brattka, Vasco}, author = {Gherardi, Guido}, author = {Pauly, Arno}, title =
{Weihrauch Complexity in computable analysis}, date = {2018}, pages = {1–61},
note = {available at arXiv:1808.03202v4}} DoraisFrançois G.Classical
consequences of continuous choice principles from intuitionistic analysisNotre
Dame J. Form. Log.552014125–39ISSN 0029-4527Review
MathReviewsDocument@article{dorais, author = {Dorais, Fran{\c{c}}ois G.},
title = {Classical consequences of continuous choice principles from
intuitionistic analysis}, journal = {Notre Dame J. Form. Log.}, volume = {55},
date = {2014}, number = {1}, pages = {25–39}, issn = {0029-4527}, review =
{\MR{3161410}}, doi = {10.1215/00294527-2377860}} DoraisFrançois
G.DzhafarovDamir D.HirstJeffry L.MiletiJoseph R.ShaferPaulOn uniform
relationships between combinatorial problemsTrans.
AMS20143681321–1359Document@article{doraisetal, author = {Dorais, Fran{\c
c}ois G.}, author = {Dzhafarov, Damir D.}, author = {Hirst, Jeffry L.}, author
= { Mileti, Joseph R.}, author = {Shafer, Paul}, title = {On uniform
relationships between combinatorial problems}, journal = {Trans.\ AMS}, year =
{2014}, volume = {368}, pages = {1321–1359}, doi = {10.1090/tran/6465}}
HirstJeffry L.LemppSteffenInfinite versions of some problems from finite
complexity theoryNotre Dame J. Form. Log.3719964545–553ISSN 0029-4527Review
MathReviewsDocument@article{hl, author = {Hirst, Jeffry L.}, author = {Lempp,
Steffen}, title = {Infinite versions of some problems from finite complexity
theory}, journal = {Notre Dame J. Form. Log.}, volume = {37}, date = {1996},
number = {4}, pages = {545–553}, issn = {0029-4527}, review = {\MR{1446228}},
doi = {10.1305/ndjfl/1040046141}} HirstJeffry L.MummertCarlReverse mathematics
and uniformity in proofs without excluded middleNotre Dame J. Form.
Log.5220112149–162ISSN 0029-4527Review MathReviewsDocument@article{hmunif,
author = {Hirst, Jeffry L.}, author = {Mummert, Carl}, title = {Reverse
mathematics and uniformity in proofs without excluded middle}, journal =
{Notre Dame J. Form. Log.}, volume = {52}, date = {2011}, number = {2}, pages
= {149–162}, issn = {0029-4527}, review = {\MR{2794648}}, doi =
{10.1215/00294527-1306163}} HirstJeffry L.MummertCarlUsing ramsey’s theorem
onceArch. Math. Logic20191–10ISSN 0933-5846Document@article{hm, author =
{Hirst, Jeffry L.}, author = {Mummert, Carl}, title = {Using Ramsey's theorem
once}, journal = {Arch. Math. Logic}, date = {2019}, pages = {1–10}, issn =
{0933-5846}, doi = {10.1007/s00153-019-00664-z}} HirstJeffry L.Leaf
managementComputability920203-4309–314ISSN 2211-3568Review
MathReviewsDocument@article{leaf, author = {Hirst, Jeffry L.}, title = {Leaf
management}, journal = {Computability}, volume = {9}, date = {2020}, number =
{3-4}, pages = {309–314}, issn = {2211-3568}, review = {\MR{4133717}}, doi =
{10.3233/com-180243}} KiharaTakayukiMarconeAlbertoPaulyArnoSearching for an
analogue of ${\sf ATR}_{0}$ in the weihrauch latticeJ. Symb.
Log.85202031006–1043ISSN 0022-4812Review MathReviewsDocument@article{kmp,
author = {Kihara, Takayuki}, author = {Marcone, Alberto}, author = {Pauly,
Arno}, title = {Searching for an analogue of $\atr$ in the Weihrauch lattice},
journal = {J. Symb. Log.}, volume = {85}, date = {2020}, number = {3}, pages =
{1006–1043}, issn = {0022-4812}, review = {\MR{4231614}}, doi =
{10.1017/jsl.2020.12}} KohlenbachUlrichHigher order reverse
mathematicstitle={Reverse mathematics 2001}, series={Lect. Notes Log.},
volume={21}, publisher={Assoc. Symb. Log., La Jolla, CA}, 2005281–295Review
MathReviews@article{k2001, author = {Kohlenbach, Ulrich}, title = {Higher
order reverse mathematics}, conference = {title={Reverse mathematics 2001}, },
book = {series={Lect. Notes Log.}, volume={21}, publisher={Assoc. Symb. Log.,
La Jolla, CA}, }, date = {2005}, pages = {281–295}, review = {\MR{2185441}}}
KohlenbachUlrichApplied proof theory: proof interpretations and their use in
mathematicsSpringer Monographs in MathematicsSpringer-Verlag,
Berlin2008xx+532ISBN 978-3-540-77532-4Review MathReviews@book{kbook, author =
{Kohlenbach, Ulrich}, title = {Applied proof theory: proof interpretations and
their use in mathematics}, series = {Springer Monographs in Mathematics},
publisher = {Springer-Verlag, Berlin}, date = {2008}, pages = {xx+532}, isbn =
{978-3-540-77532-4}, review = {\MR{2445721}}} PaulyArnoPersonal
communication2021@miscellaneous{pauly, author = {Pauly, Arno}, title =
{Personal communication}, date = {2021}} SimpsonStephen G.Subsystems of second
order arithmeticPerspectives in Logic2Cambridge University Press, Cambridge;
Assoc. Symb. Log., 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; Assoc.
Symb. Log., Poughkeepsie, NY}, date = {2009}, pages = {xvi+444}, isbn =
{978-0-521-88439-6}, review = {\MR{2517689 (2010e:03073)}}, doi =
{10.1017/CBO9780511581007}} TroelstraA. S.Metamathematical investigation of
intuitionistic arithmetic and analysisLect. Notes in Math.344Springer,
Berlin1973xvii+485ISBN 0-387-06491-5@book{troelstra, author = {Troelstra,
A.~S.}, title = {Metamathematical investigation of intuitionistic arithmetic
and analysis}, series = {Lect. Notes in Math.}, volume = {344}, publisher =
{Springer, Berlin}, date = {1973}, pages = {xvii+485}, isbn = {0-387-06491-5}}