Reverse mathematics and Weihrauch analysis motivated by finite complexity theory

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.

Keywords

Reverse mathematics Weihrauch isomorphic subgraph LPO ACA

An early article of Hirst and Lempp [5] 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 $Π_{1}^{1} - {CA}_{0}$ , while the corresponding problem for Eulerian graphs is equivalent to ${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 ∃-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 [11], 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 $Π_{1}^{1} - {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 [4]. Weihrauch analysis at the level of $Π_{1}^{1} - {CA}_{0}$ appears to parallel familiar reverse mathematics closely, in contrast to recent results related to ${ATR}_{0}$ by Kihara, Marcone, and Pauly [9].

1. Formalized Weihrauch analysis

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

Imitating Dorais et al. [2,3], 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 $Γ_{1}$ by Troelstra [14]. A formula is ∃-free if it is built from atomic formulas using only universal quantification and the connectives ∧ and →. (Troelstra includes ⊥ as an atomic formula, so $\neg P$ abbreviates $P \to ⊥$ .) The collection $Γ_{1}$ consists of those formulas defined inductively by the following:

All atomic formulas are elements of $Γ_{1}$ .

If A and B are in $Γ_{1}$ , then so are $A \land B$ , $A \lor B$ , $\forall x A$ , and $\exists x A$ .

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

Definition.
Suppose $P : \forall x (p_{1} (x) \to \exists y p_{2} (x, y))$ and $Q : \forall u (q_{1} (u) \to \exists v q_{2} (u, v))$ are problems. The reduction prenex formula for $Q ⩽_{W} P$ is the formula: $\begin{matrix} S_{Q}^{P} : \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)))) \end{matrix}$ If the problems are total, we can write $P$ as $\forall x \exists y p (x, y)$ , $Q$ as $\forall u \exists v q (u, v)$ and $S_{Q}^{P}$ as $\forall u \exists x \forall y \exists v (p (x, y) \to q (u, v))$ .

The implication $S_{Q}^{P} \to (P \to 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 ∃-free, then the matrix of $S_{Q}^{P}$ is also ∃-free and $S_{Q}^{P}$ is in $Γ_{1}$ . This also holds for total problems.

If $P$ and $Q$ are Weihrauch problems, we can formalize $Q ⩽_{W} P$ by asserting the existence of Skolem functions for the existential quantifiers of $S_{Q}^{P}$ . Using $P$ and $Q$ as in the definition, the relation $Q ⩽_{W} P$ can be translated into the language of $i {RCA}_{0}^{ω}$ as: $\begin{matrix} \exists Φ \exists Ψ \forall u \forall y (q_{1} (u) \to (p_{1} (Φ (u)) \land (p_{2} (Φ (u), y) \to q_{2} (u, Ψ (u, y))))) \end{matrix}$ Here the functionals Φ and Ψ 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 [7].
Theorem 1.
Suppose $P$ and $Q$ are problems and the reduction prenex formula $S_{Q}^{P}$ is in $Γ_{1}$ . Then $i {RCA}_{0}^{ω} ⊢ S_{Q}^{P}$ if and only if $i {RCA}_{0}^{ω} ⊢ Q ⩽_{W} P$ .
Proof.
The result follows from the application of Kohlenbach’s [11] proof mining technology to extract terms corresponding to the Skolem functions. Only one modification to the proof of Theorem 1 of Hirst and Mummert [7] is needed. The hypothesis of their theorem specifies that the matrix of $S_{Q}^{P}$ is in $Γ_{1}$ , which by the definition of $Γ_{1}$ is equivalent to $S_{Q}^{P} \in Γ_{1}$ . □

The following theorem is the intuitionistic analog of a conservation result of Kohlenbach [10]. Theorem 2.
The system $i {RCA}_{0}^{ω}$ is conservative over $i {RCA}_{0}$ for second order formulas.
Proof.
Kohlenbach’s conservation result for ${RCA}_{0}^{ω}$ over ${RCA}_{0}$ appears as Proposition 3.1 in his article on higher order reverse mathematics [10]. 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 [14]. The arguments of Troelstra (e.g. 2.6.12 and 2.6.20 of [14]) are carried out in intutionistic systems. Similarly, Kohlenbach’s proof holds for $i {RCA}_{0}^{ω}$ and $i {RCA}_{0}$ . For other related discussion, see Theorem 2.7 and Theorem 2.8 of Hirst and Mummert [6]. □

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 $N$ as its vertex set. Fix a primitive recursive bijective pairing function, p, mapping $N$ onto ${(a, b) ∣ a < b}$ , the subset of $N \times N$ consisting of increasing pairs. Both p and $p^{- 1}$ can be defined in such a way that $i {RCA}_{0}^{ω}$ proves their existence and salient properties. Using this pairing function, any function $e : N \to 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) ∣ a < b ⩽ 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 ⩽ 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 $LG k (G)$ such that $LG k (G) = 0$ implies that for every m the subgraph $G_{m}$ has a k-coloring, and $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 $LG k (G) = n$ as the following ∃-free formula, $\begin{matrix} (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{matrix}$ and note that $LG k$ is a total problem of the form $\forall G \exists n (LG k (G) = n)$ . We will compare $LG k$ to a version of the limited principle of omniscience.

$LPO$ (Limited principle of omniscience).

For every $p : N \to N$ there is a value $LPO (p)$ such that $LPO (p) = 0$ implies that $\forall k p (k) > 0$ , and $LPO (p) = m > 0$ implies that $p (m - 1) = 0$ and for all $t < (m - 1)$ , $p (t) > 0$ .

We can formalize the predicate $LPO (p) = n$ as the following ∃-free formula, $\begin{matrix} (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))) \end{matrix}$ and note that $LPO$ is a total problem of the form $\forall p \exists n (LPO (p) = n)$ . This version of $LPO$ differs from that presented in the survey by Brattka, Gherardi, and Pauly [1]. 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 $N$ . However, for our purposes it is desirable to have the underlying predicate be ∃-free.

Lemma 3 ( $i {RCA}_{0}^{ω}$ ).

For each $k ⩾ 1$ , both $S_{LPO}^{LG k}$ and $S_{LG k}^{LPO}$ hold.

Proof.
Because both $LPO$ and $LG k$ are total, we can use the simple form of the reduction prenex formula. Thus $S_{LPO}^{LG k}$ is $\forall p \exists G \forall y \exists v (LG k (G) = y \to LPO (p) = v)$ . To prove this in $i {RCA}_{0}^{ω}$ , fix an instance p of $LPO$ . Define the graph G as follows. For each m, if $p (m) = 0$ , add the edges ${(s, t) ∣ m ⩽ s < t ⩽ 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 $LG k (G) = 0$ , then for all m, $p (m) > 0$ , so $LPO (p) = 0$ . On the other hand, if $LG k (G) = m > 0$ , then $m = n + k$ for some $n ⩾ 0$ , and $p (n) = 0$ , so $LPO (p) = n + 1 = m - k + 1$ .

To show that $S_{LG k}^{LPO}$ , fix a graph G. Define an instance p of $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 $LPO (p) \frac{\cdot}{} 1$ yields a correct output for $LG k (G)$ . □

By formalizing the transitivity of Weihrauch reduction we can extract additional results from the preceding lemma.
Lemma 4 ( $i {RCA}_{0}^{ω}$ ).

If $P ⩽_{W} Q$ and $Q ⩽_{W} R$ , then $P ⩽_{W} R$ .

Proof.
This is a formalization of the well-known property for Weihrauch reductions. The system $i {RCA}_{0}^{ω}$ can prove that compositions of given functionals exist, so the usual proof holds. □
Theorem 5 ( $i {RCA}_{0}^{ω}$ ).

For any $j ⩾ k ⩾ 1$ , $LPO \equiv_{W} LG k \equiv_{W} LG j$ .

Proof.
By our formalization of $LPO$ and $LG k$ , the corresponding predicates are ∃-free. Consequently, both $S_{LPO}^{LG k}$ and $S_{LG k}^{LPO}$ are in $Γ_{1}$ . Applying Theorem 1 to the implications of Lemma 3 yields proofs in $i {RCA}_{0}^{ω}$ that $LPO ⩽_{W} LG k$ , $LG k ⩽_{W} LPO$ , and so $LPO \equiv_{W} LG k$ . This holds for all j and k, so by Lemma 4 we have $LG k \equiv_{W} LG j$ . □

One noteworthy consequence of the preceding theorem is the provability of the Weihrauch equivalence of $LG 2$ and $LG 3$ in $i {RCA}_{0}^{ω}$ . 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 [5], 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 {RCA}_{0}^{ω}$ ).

For every pair of problems $P$ and $Q$ from the list in Theorem 5 , $S_{Q}^{P}$ holds. Furthermore, the implication $P \to Q$ holds.

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

If $P$ is a problem, the parallelization of $P$ , denoted by $\hat{P}$ is the problem that accepts as input any infinite sequence of inputs for $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 [1].
Lemma 7 ( $i {RCA}_{0}^{ω}$ ).

$P ⩽_{W} Q$ implies $\hat{P} ⩽_{W} \hat{Q}$ .

Proof.
Suppose that Φ and Ψ are the functionals witnessing $P ⩽_{W} Q$ . If $\vec{u} = {⟨ u_{i} ⟩}_{i \in N}$ is an input for $\hat{P}$ , define $\hat{Φ}$ by $\hat{Φ} (\vec{u}) = {⟨ Φ (u_{i}) ⟩}_{i \in N}$ . Define $\hat{Ψ}$ similarly. Note that $i {RCA}_{0}^{ω}$ suffices to prove the existence of $\hat{Φ}$ and $\hat{Ψ}$ , and also proves that they witness $\hat{P} ⩽_{W} \hat{Q}$ . □
Theorem 8 ( $i {RCA}_{0}^{ω}$ ).

For every $k ⩾ 1$ , $\hat{LPO} \equiv_{W} \hat{LG k}$ .

Proof.
Apply Lemma 7 to Theorem 5. □

If ${⟨ f_{i} ⟩}_{i \in N}$ is a sequence of input functions for $\hat{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 $\hat{LPO}$ . This modification allows us to think of $\hat{LPO}$ as a $Π_{2}^{1}$ formula of second order arithmetic. Similarly, we will conflate $\hat{LG k}$ with its second order analog.
Corollary 9 ( $i {RCA}_{0}$ ).

The following are equivalent:

${ACA}_{0}$ .

$\hat{LPO}$ .

$\hat{LG k}$ , where $k ⩾ 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_{Q}^{P} \to (P \to Q)$ . To show that (1) implies (2), let ${⟨ f_{i} ⟩}_{i \in N}$ be an input for $\hat{LPO}$ . Arithmetical comprehension asserts the existence of the set ${i ∣ \forall n f_{i} (n) \neq 0}$ and the corresponding characteristic function, which is a solution of the instance of $\hat{LPO}$ .

To show that (2) implies (1), we adapt the familiar application of Lemma III.1.3 of Simpson [13]. In $i {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 [13] to prove the reversal.) Let f be such a function. Define the sequence of functions ${⟨ f_{i} ⟩}_{i \in N}$ by $f_{i} (m) = 1$ if $\forall t < m (f (t) \neq i)$ and $f_{i} (m) = 0$ otherwise. The solution to the $\hat{LPO}$ problem ${⟨ f_{i} ⟩}_{i \in 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 {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 : N \to 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 : 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 {RCA}_{0}^{ω}$ 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 an ∃-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 ∃-free. Thus we can write an ∃-free formula $GC k (G, f)$ asserting that f is the solution to the $GC k$ problem for G.

In our study of problems involving infinite trees, we will use the following encoding. Fix a suitable bijective coding function $seq$ mapping $N$ onto $2^{< N}$ , the set of finite sequences of zeros and ones. Any function $t : N \to N$ can be viewed as a code for a binary tree T using the following convention. The finite sequence $seq (n)$ is in T if and only if $t (n) > 0$ and for every initial segment σ of $seq (n)$ , $t ({seq}^{- 1} (σ)) > 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 $σ \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 ∃-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 ∃-free formula $WKL (T, f)$ asserting that f is a solution to the $WKL$ problem for T.

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

$WKL n$ (Weak König’s Lemma for trees in $n^{< N}$ ).

If T is a tree with nodes labeled with numbers less than n, and for every m there is a sequence $σ \in T$ of length m, then there is a function p that codes an infinite path through T.

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

Lemma 10 ( $i {RCA}_{0}$ ).

For each $n ⩾ 2$ , $S_{WKL n}^{WKL}$ and $S_{WKL}^{WKL n}$ hold.

Proof.
For $n ⩾ 2$ , every binary tree is an n-ary tree, so $S_{WKL}^{WKL n}$ holds trivially. To prove $S_{WKL n}^{WKL}$ , 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 $⟨ 2, 0, 3 ⟩$ 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 $⟨ 2, 0, 3 ⟩$ becomes $⟨ 1, 1, 0, 0, 0, 0, 1, 1, 1 ⟩$ . 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 $LLPO$ , which is defined for all functions from $N$ into $N$ . Naïvely, if a function p has a positive value, then $LLPO$ returns the flip of the parity of that first positive value.
$LLPO$ (Lesser limited principle of omniscience).

For any $p : N \to N$ there is a value $LLPO (p)$ such that $LLPO (p) = 0$ implies if $p (j) \neq 0$ and $\forall t < j (p (j) = 0)$ then j is odd, and $LLPO (p) \neq 0$ implies $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 $LLPO (p)$ matches the definition of Brattka, Gherardi, and Pauly [1]*§7.2. By mapping functions from $N$ to $N$ to the characteristic function for the least element of their domain taking a positive value, routine verification shows that our total version of $LLPO$ is strongly Weihrauch equivalent to their version.

The predicate “j is odd” can be formalized by $\forall m (j \neq 2 m)$ . Similarly, “j is even” can be formalized by $\forall m (j \neq 2 m + 1)$ . Consequently, $LLPO (p) = n$ can be formalized by the ∃-free formula: $\begin{array}{l} (n = 0 \to \forall j ([p (j) \neq 0 \land \forall t (t < j \to p (t) = 0)] \to \forall m (j \neq 2 m))) \\ \land (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 2 m + 1)))) \end{array}$

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

Lemma 11 ( $i {RCA}_{0}$ ).

$S_{WKL}^{\hat{LLPO}}$ holds.

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

If $σ^{⌢} 0$ extends to an infinite path, but $σ^{⌢} 1$ does not, then there is a first $n > 0$ such that $σ^{⌢} 1$ has no extensions of length n. In this case, $LLPO (p_{σ}) = 0$ . Similarly, if $σ^{⌢} 1$ extends to an infinite path but $σ^{⌢} 0$ does not, $LLPO (p_{σ}) = 1$ . If both $σ^{⌢} 0$ and $σ^{⌢} 1$ extend to infinite paths, then $p_{σ}$ is the zero sequence and $LLPO (p_{σ})$ may be 0 or 1. Thus, if T is infinite, the sequence constructed by setting $σ (0) = LLPO (⟨ ⟩)$ and $σ (n + 1) = σ {(n)}^{⌢} LLPO (σ (n))$ for $n ⩾ 0$ is an infinite path through T. □
Lemma 12 ( $i {RCA}_{0}$ ).

$S_{\hat{LLPO}}^{GC 2}$ .

Proof.
Suppose $p_{i}$ is an instance of $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 $LLPO$ . If $u_{i}$ and $v_{i, 0}$ agree in color, then 0 is a correct output. For a sequence of instances of $LLPO$ , let G consist of the disjoint union of the graphs for each sequence. Any 2-coloring of G yields a solution to the instance of $\hat{LLPO}$ . □
Lemma 13 ( $i {RCA}_{0}$ ).

For $n ⩾ 2$ , $S_{GC 2}^{GC n}$ .

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 {RCA}_{0}$ ).

For $n ⩾ 2$ , $S_{GC n}^{WKL n}$ holds.

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

We can concatenate the lemmas to yield our main theorem on Weihrauch equivalences related to graph colorings.
Theorem 15 ( $i {RCA}_{0}^{ω}$ ).

For $n ⩾ 2$ , we have: $\begin{matrix} WKL n \equiv_{W} WKL \equiv_{W} \hat{LLPO} \equiv_{W} GC n \equiv_{W} GC 2 . \end{matrix}$

Proof.
Applying Theorem 1 to Lemma 10 and Lemma 11, we have $WKL n ⩽_{W} WKL ⩽_{W} \hat{LLPO}$ . Applying Theorem 1 to Lemma 12, Lemma 13, and Lemma 14 yields $\hat{LLPO} ⩽_{W} GC 2 ⩽_{W} GC n ⩽_{W} 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 {RCA}_{0}$ ).

The formula $S_{Q}^{P}$ holds for every problem $P$ and problem $Q$ appearing in Theorem 15 . Furthermore the implication $P \to Q$ holds.

Proof.
Imitate the proof of Corollary 6. □
Corollary 17 ( $i {RCA}_{0}$ ).

For $k ⩾ 2$ , the following are equivalent:

$WKL$ .

$\hat{LLPO}$ .

$WKL k$ .

$GC k$ .

Proof.
Immediate from Corollary 16. □

Parallelization of $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 {RCA}_{0}^{ω}$ ).

The hat operator is idempotent, that is, for any problem $P$ , $\hat{P} \equiv_{W} \hat{\hat{P}}$ . Consequently, for $k ⩾ 2$ , $GC k \equiv_{W} \hat{GC k}$ .

Proof.
In $i {RCA}_{0}^{ω}$ , we can use the bijective pairing function to match each pair $(i, j)$ with an integer code. Given a sequence of sequences of problems $⟨ ⟨ p_{i, j} ∣ j \in N ⟩ i \in N ⟩$ , we match each problem with an element of the sequence $⟨ p_{(i, j)} ∣ (i, j) \in N ⟩$ . Thus $\hat{\hat{P}} ⩽_{W} \hat{P}$ . The reverse reduction is trivial.

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

In combination with Theorem 15 we see that $\hat{GC 2} \equiv_{W} \hat{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 [5]. The corresponding reverse mathematical results can be extracted in the usual fashion, yielding the following corollary.
Corollary 19 ( $i {RCA}_{0}$ ).

For $k ⩾ 2$ , $WKL$ is equivalent to the assertion that for any sequence ${⟨ G_{i} ⟩}_{i \in N}$ of infinite locally k-colorable graphs, there is a function $f : N \times N \to 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 : N \to 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 $TGC k$ for G can be formalized as an ∃-free formula in the parameters k, f, and G. Altering the problem affects the Weihrauch analysis.

Theorem 20 ( $i {RCA}_{0}^{ω}$ ).

For $k ⩾ 2$ , $LPO ⩽_{W} TGC k ⩽_{W} \hat{LPO}$ .

Proof.
For the first reduction, fix k and suppose p is an instance of $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 $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 $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 ⩽ n$ the initial subgraph $G_{t}$ has a k-coloring, and let $p_{0} (n) = 0$ otherwise. For $i > 0$ , define $p_{i}$ as follows. Let $σ_{1}, σ_{2}, \dots$ be the finite sequences in $k^{< 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 $σ_{i}$ extends to a k-coloring of $G_{m}$ , and let $p_{i} (m) = 0$ otherwise. Given a solution to the $\hat{LPO}$ problem ${⟨ p_{i} ⟩}_{i \in N}$ , we can compute a solution f to $TGC k$ for G as follows. Let $f (0) = LPO (p_{0})$ . If $f (0) > 0$ , let $f (n) = 0$ for all $n > 0$ . Otherwise, use the values of $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 $LPO (p_{n}) = 0$ , then the tree of partial k-colorings extending $σ_{n}$ is infinite, and there is a least m such that there is a $j < k$ with $σ_{m} = σ_{n}^{⌢} j$ and $LPO (p_{m}) = 0$ . □
Corollary 21 ( $i {RCA}_{0}^{ω}$ ).

For $k ⩾ 2$ , $\hat{TGC k} \equiv_{W} \hat{LPO}$ and $\hat{GC k} \equiv_{W} \hat{LLPO}$ .

Proof.
Apply parallelization and idempotence to the reductions in Theorem 15 and Theorem 20. □

Because the associated predicates are ∃-free, the Weihrauch results of Corollary 21 can be converted to a reverse mathematics result after the fashion of Corollary 19.
Corollary 22 ( $i {RCA}_{0}$ ).

For $k ⩾ 2$ , ${ACA}_{0}$ is equivalent to the assertion that for any sequence ${⟨ G_{i} ⟩}_{i \in N}$ of graphs, there is a function $f : N \times N \to N$ such that for each i, either $f (i, 0) = m > 0$ and the $m^{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 $P {⩽̸}_{W} 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 {RCA}_{0}^{ω}$ .

Corollary 23.
For $k ⩾ 2$ , $i {RCA}_{0}^{ω}$ proves $GC k ⩽_{W} TGC k$ . In the non-formal setting, $GC k <_{W} TGC k$ .
Proof.
$i {RCA}_{0}^{ω}$ proves that $GC k ⩽_{W} 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 computability and Weihrauch reducibility literature. Suppose by way of contradiction that $TGC k ⩽_{W} GC k$ . Parallelization preserves the reduction, so $\hat{TGC k} ⩽_{W} \hat{GC k}$ . By Theorem 15 and Lemma 18, $\hat{GC k} \equiv_{W} WKL$ , so $\hat{TGC k} ⩽_{W} WKL$ . We will use a computable instance of $\hat{TGC k}$ to contradict known computability theory. Let $g : N \to N$ be a computable function whose range computes $0^{'}$ . For each n, let $G_{n}$ be the graph that is completely disconnected unless $g (m) = n$ , in which case we include the complete graph on the $k + 1$ vertices corresponding to $m, m + 1, \dots, m + k$ . The graph $G_{n}$ is not k-colorable if and only if n is in the range of g. Because g is computable, the sequence ${⟨ G_{i} ⟩}_{i \in N}$ is a computable instance of $\hat{TGC k}$ . Every solution computes $0^{'}$ . Applying the functionals witnessing $\hat{TGC k} ⩽_{W} WKL$ , we can find a computable infinite binary tree such that every infinite path computes $0^{'}$ , contradicting the Jockusch–Soare low basis theorem, Theorem 2.1 of [8]. □

2. Weihrauch analysis related to $Π_{1}^{1} - {CA}_{0}$

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

$WF$ (Well founded trees).

Given a tree T in $N^{< 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 [5].

$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} ∣ i \in N}$ and edges $E = {(v_{i}, v_{i + 1}) ∣ i \in N}$ .

$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.
$WF \equiv_{s W} S_{L} \equiv_{s W} S$ .
Proof.
First we will show that $WF ⩽_{s W} S_{L}$ . Any tree T in $N^{< 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 - S_{L} (T)$ is equal to $WF (T)$ , so the post-processing does not depend on T and the reduction is strong.

The problem $S_{L}$ is a special case of $S$ , so it only remains to show that $S ⩽_{s W} WF$ . Suppose G and H are input graphs with vertices ${g_{i} ∣ i \in N}$ and ${h_{i} ∣ i \in 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 ⩽ 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 - WF (T)$ is equal to $S (G, H)$ , yielding the final strong Weihrauch reduction. □

Theorem 3.4 of [5] discusses sequences of graphs and trees. Similar Weihrauch reductions follow by parallelization.
Corollary 25.
$\hat{WF} \equiv_{s W} {\hat{S}}_{L} \equiv_{s W} \hat{S}$ .
Proof.
As noted in Proposition 3.6 part 3 of [1], 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 [5] indicates that an instance of $\hat{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.
$S_{\vec{L}}$ (Tagged linear subgraphs of a fixed graph).

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

Theorem 26.
$\hat{WF} \equiv_{s W} S_{\vec{L}}$ .
Proof.
Note that an input G for $S_{\vec{L}}$ corresponds exactly to the input ${⟨ G, L_{i} ⟩}_{i \in N}$ for $\hat{S}$ . Thus $S_{\vec{L}} ⩽_{s W} \hat{S} \equiv_{s W} \hat{WF}$ . To show that $\hat{WF} ⩽_{s W} S_{\vec{L}}$ , we adapt the reversal from Theorem 3.4 of [5]. Let ${⟨ T_{i} ⟩}_{i \in N}$ be an input for $\hat{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 ${⟨ T_{i} ⟩}_{i \in 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 : N \to 2$ is a solution to $S_{\vec{L}}$ for this graph G, then $w (n) = 1 - s (n)$ is a solution of $\hat{WF}$ for ${⟨ T_{i} ⟩}_{i \in N}$ , completing the proof that $\hat{WF} ⩽_{s W} 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 $S_{L} \equiv_{s W} WF$ , finite graphs yield a weaker Weihrauch problem.
Theorem 27.
Suppose that F is a finite graph with at least two vertices. Then $S_{F} \equiv_{W} LPO$ .
Proof.
We will prove the result for the version of $LPO$ from section §1.1. For other versions of $LPO$ , the result can be strengthened to strong Weihrauch reduction. Fix a finite graph F. To show that $S_{F} ⩽_{W} LPO$ , let G be an input graph and construct an input for $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 $S_{F} (G) = 1$ if and only if $LPO (p) > 0$ .

To prove that $LPO ⩽_{W} 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 $LPO$ . Let G be the graph with vertices ${v_{i} ∣ i \in 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 $S_{F} (G) = 0$ , output 0 for $LPO (p)$ . If $S_{F} (G) = 1$ , then the search for the least m such that $p (m) = 0$ will succeed and the appropriate value of $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 $S_{F} \equiv_{W} LPO$ and $S_{L} \equiv_{W} WF$ motivates the following question: Is there a graph H such that $LPO <_{W} S_{H} <_{W} 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, ${SE}_{H} \equiv_{W} {LPO}^{'}$ [12]. 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 $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 $S^{K}$ and $S^{D}$ are both Weihrauch equivalent to $LPO$ . Theorem 3.2 of [5] 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 $Σ_{1}^{1}$ complete. This prompts us to ask: Is there a graph G such that $S^{G} \equiv_{s W} WF$ ? Indeed, is there even a graph G such that $LPO <_{W} S^{G}$ ?

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

$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.

$RC \equiv_{s W} D \equiv_{s W} WF$ .

Proof.

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

To show that $WF ⩽_{s W} 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, $WF (T) = 1 - S_{D} (G)$ , so $WF ⩽_{s W} S_{D}$ , as desired. □

Appending a triangle to each tree node in the previous construction yields a proof that $WF$ is Weihrauch equivalent to $S_{G}$ for the graph G consisting of infinitely many disconnected triangles. (This was proven independently by Arno Pauly [12].) 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 [5].

Corollary 29.

$\hat{RC} \equiv_{s W} \hat{D} \equiv_{s W} \hat{WF}$ .

Proof.

Immediate from Theorem 28 by Proposition 3.6 part 3 of [1]. □

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.

References

Brattka,

Gherardi and

Pauly, Weihrauch complexity in computable analysis, 2018, 1–61, https://arxiv.org/abs/1707.03202.

F.G.

Dorais, Classical consequences of continuous choice principles from intuitionistic analysis, Notre Dame J. Form. Log. 55(1) (2014), 25–39. doi:10.1215/00294527-2377860.

F.G.

Dorais,

D.D.

Dzhafarov,

J.L.

Hirst,

J.R.

Mileti and

Shafer, On uniform relationships between combinatorial problems, Trans. Amer. Math. Soc. 368(2) (2016), 1321–1359. doi:10.1090/tran/6465.

J.L.

Hirst, Leaf management, Computability 9(3–4) (2020), 309–314. doi:10.3233/COM-180243.

J.L.

Hirst and

Lempp, Infinite versions of some problems from finite complexity theory, Notre Dame J. Form. Log. 37(4) (1996), 545–553. doi:10.1305/ndjfl/1040046141.

J.L.

Hirst and

Mummert, Reverse mathematics and uniformity in proofs without excluded middle, Notre Dame J. Form. Log. 52(2) (2011), 149–162. doi:10.1215/00294527-1306163.

J.L.

Hirst and

Mummert, Using Ramsey’s theorem once, Arch. Math. Logic (2019), 1–10. doi:10.1007/s00153-019-00664-z.

C.G.

JockuschJr. and

R.I.

Soare,

Π_{1}^{0}

classes and degrees of theories, Trans. Amer. Math. Soc. 173 (1972), 33–56. doi:10.2307/1996261.

Kihara,

Marcone and

Pauly, Searching for an analogue of

{ATR}_{0}

in the Weihrauch lattice, J. Symb. Log. 85(3) (2020), 1006–1043. doi:10.1017/jsl.2020.12.

10.

Kohlenbach, Higher order reverse mathematics, in: Reverse Mathematics 2001,

Simpson, ed., Lect. Notes Log., Vol. 21, Assoc. Symbol. Logic, La Jolla, CA, 2005, pp. 281–295. doi:10.1017/9781316755846.018.

11.

Kohlenbach, Applied Proof Theory: Proof Interpretations and Their Use in Mathematics, Springer Monographs in Mathematics, Springer-Verlag, Berlin, 2008, p. xx+532. ISBN 978-3-540-77532-4.

12.

Pauly, Personal communication, 2021.

13.

S.G.

Simpson, Subsystems of Second Order Arithmetic, Perspectives in Logic, 2nd edn, Cambridge University Press, Cambridge; Association for Symbolic Logic, Poughkeepsie, NY, 2009, p. xvi+444. ISBN 978-0-521-88439-6. doi:10.1017/CBO9780511581007.

14.

A.S.

Troelstra, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Lect. Notes in Math., Vol. 344, Springer, Berlin, 1973, p. xvii+485. ISBN 0-387-06491-5. doi:10.1007/BFb0066739.

Reverse mathematics and Weihrauch analysis motivated by finite complexity theory

Abstract

Keywords

1. Formalized Weihrauch analysis

LG k (Local k-coloring for graphs).

LPO (Limited principle of omniscience).

Lemma 3 ( i RCA 0 ω ).

Proof. This is a formalization of the well-known property for Weihrauch reductions. The system i RCA 0 ω can prove that compositions of given functionals exist, so the usual proof holds. □ Theorem 5 ( i RCA 0 ω ).

GC k (k-coloring of graphs).

WKL (Weak König’s Lemma).

WKL n (Weak König’s Lemma for trees in n < N ).

Lemma 10 ( i RCA 0 ).

Lemma 11 ( i RCA 0 ).

Proof. Imitate the proof of Corollary 6. □ Corollary 17 ( i RCA 0 ).

Proof. Immediate from Corollary 16. □ Parallelization of 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 RCA 0 ω ).

TGC k (Total k-coloring of graphs).

Theorem 20 ( i RCA 0 ω ).

Proof. Apply parallelization and idempotence to the reductions in Theorem 15 and Theorem 20. □ Because the associated predicates are ∃-free, the Weihrauch results of Corollary 21 can be converted to a reverse mathematics result after the fashion of Corollary 19. Corollary 22 ( i RCA 0 ).

WF (Well founded trees).

S (Isomorphic subgraph).

S L (L as a subgraph).

D (Disconnected subgraph).

References

$LG k$ (Local k-coloring for graphs).

$LPO$ (Limited principle of omniscience).

Lemma 3 ( $i {RCA}_{0}^{ω}$ ).

Proof.
This is a formalization of the well-known property for Weihrauch reductions. The system $i {RCA}_{0}^{ω}$ can prove that compositions of given functionals exist, so the usual proof holds. □
Theorem 5 ( $i {RCA}_{0}^{ω}$ ).

$GC k$ (k-coloring of graphs).

$WKL$ (Weak König’s Lemma).

$WKL n$ (Weak König’s Lemma for trees in $n^{< N}$ ).

Lemma 10 ( $i {RCA}_{0}$ ).

Lemma 11 ( $i {RCA}_{0}$ ).

Proof.
Imitate the proof of Corollary 6. □
Corollary 17 ( $i {RCA}_{0}$ ).

Proof.
Immediate from Corollary 16. □

Parallelization of $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 {RCA}_{0}^{ω}$ ).

$TGC k$ (Total k-coloring of graphs).

Theorem 20 ( $i {RCA}_{0}^{ω}$ ).

Proof.
Apply parallelization and idempotence to the reductions in Theorem 15 and Theorem 20. □

Because the associated predicates are ∃-free, the Weihrauch results of Corollary 21 can be converted to a reverse mathematics result after the fashion of Corollary 19.
Corollary 22 ( $i {RCA}_{0}$ ).

$WF$ (Well founded trees).

$S$ (Isomorphic subgraph).

$S_{L}$ (L as a subgraph).

$D$ (Disconnected subgraph).