Leaf management

Abstract

Finding the set of leaves for an unbounded tree is a nontrivial process in both the Weihrauch and reverse mathematics settings. Despite this, many combinatorial principles for trees are equivalent to their restrictions to trees with leaf sets. For example, let $\hat{WF}$ denote the problem of choosing which trees in a sequence are well-founded, and let $PK$ denote the problem of finding the perfect kernel of a tree. Let ${\hat{WF}}_{L}$ and ${PK}_{L}$ denote the restrictions of these principles to trees with leaf sets. Then $\hat{WF}$ , ${\hat{WF}}_{L}$ , $PK$ , and ${PK}_{L}$ are all equivalent to $Π_{1}^{1} – {CA}_{0}$ over ${RCA}_{0}$ , and all strongly Weihrauch equivalent.

Keywords

Reverse mathematics computability Weihrauch

1. Introduction

The first section of this paper shows that for unbounded trees, finding leaf sets is a nontrivial process. The second section describes an algorithm for transforming trees into trees with leaf sets in such a way that properties related to infinite paths and perfect subtrees are preserved. The main equivalence results are presented in this section. The paper closes with a section containing an application to hypergraphs, where the use of a combinatorial principle restricted to sequences of trees with leaf sets is central to the proof of a Weihrauch equivalence.

All relevant background information on reverse mathematics can be found in Simpson’s text [7]. For background on Weihrauch analysis, see the work of Brattka, Gherardi, and Pauly [3].

2. Leaf sets

In second order arithmetic settings, a tree is encoded by a set of finite sequences of natural numbers that is closed under initial subsequences. For any finite sequence σ, let $| σ |$ denote the length of σ. A leaf in a tree is a sequence that has no extensions in the tree. For a tree T, let $leaf (T)$ denote the set of leaves of T. A function $b : N \to N$ is a bounding function for T if for every $σ \in T$ and for every $i < | σ |$ , $σ (i) ⩽ b (i)$ . If a tree T has a bounding function, little set comprehension is required to calculate $leaf (T)$ .

Proposition 1.
$({RCA}_{0})$ If b is a bounding function for the tree T, then $leaf (T)$ exists.
Proof.
Working in ${RCA}_{0}$ , the sequence σ is a leaf of T if and only if $σ \in T$ and for each $j ⩽ b (| σ | + 1)$ we have $σ^{⌢} j \notin T$ . Thus, the set $leaf (T)$ is computable using T and b as parameters, and exists by recursive comprehension. □

Let $bleaf$ denote the Weihrauch problem that accepts a tree T and a bounding function b as inputs and outputs the set $leaf (T)$ . For a bounded tree, the preceding proof describes a process for computing the leaf set. Consequently, $bleaf$ is at the lowest level of the Weihrauch hierarchy, as stated in the following proposition.
Proposition 2.
$bleaf \equiv_{W} 0$ and $bleaf \equiv_{sW} id$ .

Finding leaf sets for trees without bounding functions is nontrivial. The formulation of $LPO$ parallelized in the next proposition is the one preceding Theorem 6.7 of Brattka, Gherardi, and Pauly [3], and the Boolean negation of Definition 2.6 of Brattka and Gherardi [2].
Proposition 3.
$({RCA}_{0})$ The following are equivalent.
${ACA}_{0}$ .

For every tree T, the set $leaf (T)$ exists.

$\hat{LPO}$ : If ${⟨ p_{i} ⟩}_{i \in N}$ is a sequence of sequences of natural numbers, then there is a function $z : N \to {0, 1}$ such that for each i, $z (i) = 1$ if and only if $\exists n (p_{i} (n) = 0)$ .

Proof.
We will work in ${RCA}_{0}$ throughout the proof. To see that (1) implies (2), note that $σ \in leaf (T)$ if and only if $σ \in T$ and $\forall j (σ^{⌢} j \notin T)$ . Thus arithmetical comprehension proves the existence of $leaf (T)$ .

To see that (2) implies (3), assume (2) and let ${⟨ p_{i} ⟩}_{i \in N}$ be an instance of $\hat{LPO}$ . Consider the tree T constructed from ${⟨ p_{i} ⟩}_{i \in N}$ as follows. Every finite sequence of ones is in T. For each $n \in N$ the sequence $σ_{n}$ consisting of $n + 1$ ones followed by a zero is in T. The sequence $σ_{n}^{⌢} j$ is in T if and only if $p_{n} (j) = 0$ and $\forall i < j (p_{n} (i) \neq 0)$ . The set of sequences T exists by recursive comprehension and is a tree because it is closed under initial segments. Apply (2) to find $leaf (T)$ . The function $z : N \to {0, 1}$ defined by $z (n) = 1$ if and only if $σ_{n} \notin leaf (T)$ exists by recursive comprehension and is a solution of the instance of $\hat{LPO}$ .

To complete the proof, by Lemma III.1.3 of Simpson [7], it suffices to use (3) to find the range of an injection. Let $f : N \to N$ be an injection. By recursive comprehension, we can find the sequence ${⟨ p_{i} ⟩}_{i \in N}$ defined by $p_{i} (n) = 0$ if $f (n) = i$ , and $p_{i} (n) = 1$ otherwise. Apply (3) to find z such that $z (i) = 1$ if and only if $\exists n (p_{i} (n) = 0)$ . Then the set ${i ∣ z (i) = 1}$ is the range of f, is computable from z, and so exists by recursive comprehension. □

By virtue of our circuitous reverse mathematics treatment, we can easily prove the related Weihrauch reducibility result. Let $leaf$ denote the problem that accepts a tree T as input and outputs the leaf set $leaf (T)$ . Proposition 4.
$leaf \equiv_{sW} \hat{LPO}$ .
Proof.
The proof that (2) implies (3) for Proposition 3 also shows that $\hat{LPO} ⩽_{sW} leaf$ . To prove the reverse relation, fix T and let ${⟨ σ_{i} ⟩}_{i \in N}$ be an enumeration of the sequences in T. For each i, let $p_{i} (j) = 0$ if $σ_{i}^{⌢} j \in T$ and let $p_{i} (j) = 1$ otherwise. If z is a solution to this instance of $\hat{LPO}$ , then it is also a characteristic function for $leaf (T)$ . □

3. Transforming trees

As shown in the previous section, finding the leaf set for an arbitrary tree is a nontrivial process in both the reverse mathematics and Weihrauch settings. However, in many cases it is possible to uniformly transform trees into trees with leaf sets while preserving many Weihrauch equivalences and equivalence theorems of reverse mathematics. The transformation can be defined using the following operations on finite sequences. For every $σ \in N^{< N}$ , let $σ + 1$ denote the sequence with exactly the same length as σ such that for all $n < | σ |$ , $(σ + 1) (n) = σ (n) + 1$ . For example, $⟨ 1, 3, 5 ⟩ + 1 = ⟨ 2, 4, 6 ⟩$ . Similarly, define $σ \frac{\cdot}{} 1$ so that $(σ \frac{\cdot}{} 1) (n) = σ (n) \frac{\cdot}{} 1$ . Our main tree transformation is $T^{*}$ as defined in the following theorem. Naïvely, $T^{*}$ is created by adding 1 to every node of T and attaching a leaf labeled 0 to each positive node.

Lemma 5.
$({RCA}_{0})$ Suppose $T \subset N^{< N}$ is a tree. The following are also trees: $T^{-} = {σ \frac{\cdot}{} 1 ∣ σ \in T}$ , $T^{+} = {σ + 1 ∣ σ \in T}$ , and $T^{} = T^{+} \cup {σ^{⌢} 0 ∣ σ \in T^{+}}$ . Furthermore, given a sequence* ${⟨ T_{i} ⟩}_{i \in N}$ , we can find the sequence $⟨ T_{i}^{}, leaf (T_{i}^{}) ⟩$ .
Proof.
Working in ${RCA}_{0}$ , it is easy to use recursive comprehension to prove the existence of the sets $T^{-}$ , $T^{+}$ , and $T^{}$ . The initial segments of the shifts $σ \frac{\cdot}{} 1$ and $σ + 1$ are the shifts of initial segments of σ, so $T^{-}$ and $T^{+}$ are trees. A proper initial segment of a sequence in the set ${σ^{⌢} 0 ∣ σ \in T^{+}}$ is an initial segment of an element of $T^{+}$ , so $T^{}$ is also a tree.

To complete the proof, suppose ${⟨ T_{i} ⟩}_{i \in N}$ is a sequence of trees. For each i, $σ \in T_{i}^{}$ if and only if every element of σ is positive and $σ \frac{\cdot}{} 1 \in T_{i}$ , or $σ = τ^{⌢} 0$ , every digit of τ is positive, and $τ \frac{\cdot}{} 1 \in T_{i}$ . Thus recursive comprehension implies that ${⟨ T_{i}^{} ⟩}_{i \in N}$ exists. For each i, the sequence $σ \in leaf (T_{i}^{})$ if and only if $σ \in T_{i}^{}$ and the last entry of σ is 0. Thus ${RCA}_{0}$ can prove that the sequence of pairs $⟨ T_{i}^{}, leaf (T_{i}^{}) ⟩$ exists. □

The trees T and $T^{}$ share many properties. Information about paths and subtrees of one can be uniformly transformed to information about the other. As described in Definition I.6.6 of Simpson [7], a subtree S of T is perfect if every sequence in S has incompatible extensions in S. The perfect kernel of T is the union of all the perfect subtrees of T.
Theorem 6.
$({RCA}_{0})$ A tree T and the transform* $T^{}$ satisfy the following.*
T is well-founded if and only if $T^{}$ is well-founded.*

T has at most one path if and only if $T^{}$ has at most one path.*

S is a perfect subtree of T if and only if $S^{+}$ is a perfect subtree of $T^{}$ .

K is the perfect kernel of T if and only if* $K^{+}$ is the perfect kernel of $T^{}$ .

Proof.
Each part follows from the fact that the map taking σ to $σ + 1$ is a bijection between the paths of T and those of $T^{}$ and also between the perfect subtrees of T and those of $T^{}$ . □

The next two theorems list familiar equivalences for tree statements that continue to hold when restricted to trees with leaf sets. For both proofs, the central tool is the transformation from T to $T^{}$ . In the following theorem, the labels used for the combinatorial principles are consistent with those used for the associated Weihrauch problems by Kihara, Marcone, and Pauly [6].
Theorem 7.
$({RCA}_{0})$ The following are equivalent.
${ATR}_{0}$ .

The $Σ_{1}^{1}$ separation principle: For any $Σ_{1}^{1}$ formulas $φ_{0} (n)$ and $φ_{1} (n)$ containing no free occurrences of Z, if $\neg \exists n (φ_{0} (n) \land φ_{1} (n))$ , then $\begin{matrix} \exists Z \forall n ((φ_{0} (n) \to n \in Z) \land (φ_{1} (n) \to n \notin Z)) . \end{matrix}$

$Σ_{1}^{1} – SEP$ : If ${⟨ T_{0, i} ⟩}_{i \in N}$ and ${⟨ T_{1, i} ⟩}_{i \in N}$ are sequences of trees such that for each i, at most one of $T_{0, i}$ and $T_{1, i}$ has an infinite path, then there is a set Z such that for all n, $T_{0, n}$ has an infinite path implies $n \in Z$ and $T_{1, n}$ has an infinite path implies $n \notin Z$ .

${Σ_{1}^{1} – SEP}_{L}$ : Item ( 3 ) for ${⟨ T_{0, i}, leaf (T_{0, i}) ⟩}_{i \in N}$ and ${⟨ T_{1, i}, leaf (T_{1, i}) ⟩}_{i \in N}$ , sequences of trees with leaf sets.

$Σ_{1}^{1} – {CA}^{-}$ : If ${⟨ T_{i} ⟩}_{i \in N}$ is a sequence of trees each with at most one infinite path, then there is a set Z such that for all n, $n \in Z$ if and only if $T_{n}$ has an infinite path.

$Σ_{1}^{1} – {CA}_{L}^{-}$ : Item ( 5 ) for sequences of trees with leaf sets.

${PTT}_{1}$ : If T has uncountably many paths then T has a non-empty perfect subtree.

${PTT}_{1}_{L}$ : Item ( 7 ) for trees with leaf sets.

Proof.
The equivalence of (1) and (2) is Theorem V.5.1 of Simpson [7]. The existence of an infinite path in a tree can be written as a $Σ_{1}^{1}$ formula, so (2) implies (3). To prove the converse, use a bootstrapping argument, proving ${ACA}_{0}$ from (3) by creating a sequence of pairs of linear trees that compute the range of an injection. Then use ${ACA}_{0}$ and (3) to derive (2) by an application of Lemma 3.14 of Friedman and Hirst [5]. The equivalence of (5) and (1) is Theorem V.5.2 of Simpson [7], and the equivalence of (7) and (1) is Theorem V.5.5 of Simpson [7]. Item (4) is a restriction of (3), so (3) implies (4) trivially. The converse is an immediate consequence of Theorem 6. Similarly, (5) and (6) are equivalent, as are (7) and (8). □

To avoid confusion with the subsystem $Π_{1}^{1} – {CA}_{0}$ , in following theorem we use $\hat{WF}$ as a label for the combinatorial principle denoted by $Π_{1}^{1} - CA$ in the article of Kihara, Marcone, and Pauly [6]. Note that $\hat{WF}$ is the infinite parallelization of the principle $WF$ , that takes a tree as an input and outputs a 1 if the tree is well-founded and a 0 otherwise.
Theorem 8.
$({RCA}_{0})$ The following are equivalent:
$Π_{1}^{1} – {CA}_{0}$ : If $φ (n)$ is a $Π_{1}^{1}$ formula, then there is a set Z such that for all n, $n \in Z$ if and only if $φ (n)$ .

$\hat{WF}$ : If ${⟨ T_{i} ⟩}_{i \in N}$ is a sequence of trees, then there is a set Z such that for all n, $n \in Z$ if and only if T has no infinite path.

${\hat{WF}}_{L}$ : Item ( 2 ) for sequences of trees with leaf sets.

$PK$ : Every tree has a perfect kernel.

${PK}_{L}$ : Item ( 4 ) for trees with leaf sets.

Proof.
The equivalence of (1) and (2) is Theorem VI.1.1 of Simpson [7]. The equivalence of (1) and (4) is Theorem VI.1.3 of Simpson [7]. The restriction (3) follows trivially from (2), and the converse follows immediately from Theorem 6. By a similar argument, (4) and (5) are equivalent. □

We now turn to the Weihrauch analogs of the preceding results. The main tool is the computability theoretic version of Lemma 5.
Lemma 9.
There is a uniformly computable map from trees T to $T^{-}$ , and invertible uniformly computable maps from T to $T^{+}$ and $T^{}$ . Also, there is a computable functional mapping sequences of trees* ${⟨ T_{i} ⟩}_{i \in N}$ to $⟨ T_{i}^{}, leaf (T_{i}^{}) ⟩$ .
Proof.
The processes described at the beginning of the section are uniformly computable, and for $T^{+}$ and $T^{}$ , uniformly computably invertible. Leaf sets are uniformly computable for trees of the form $T^{}$ . □

The following Weihrauch analog of Theorem 7 is based on the results of Kihara, Marcone, and Pauly [6].
Theorem 10.
${PTT}_{1} \equiv_{sW} {PTT}_{1}_{L} <_{W} Σ_{1}^{1} – SEP$ . Also, the following principles are strongly Weihrauch equivalent: $Σ_{1}^{1} – SEP$ , ${Σ_{1}^{1} – SEP}_{L}$ , $Σ_{1}^{1} – {CA}^{-}$ , and $Σ_{1}^{1} – {CA}_{L}^{-}$ .
Proof.
The equivalences between the statements and the versions restricted to trees with leaf sets follow from Lemma 9 and Theorem 6. The equivalence of $Σ_{1}^{1} – SEP$ and $Σ_{1}^{1} – {CA}^{-}$ is included in Theorem 3.11 of Kihara, Marcone, and Pauly [6], while ${PTT}_{1} <_{sW} Σ_{1}^{1} – SEP$ follows from their Corollary 3.7, Theorem 3.11, and Proposition 6.4 [6]. □

We close the section with the Weihrauch analog of Theorem 8. Theorem 11.
$WF \equiv_{sW} {WF}_{L}$ . Also, the following four principles are strongly Weihrauch equivalent: $\hat{WF}$ , ${\hat{WF}}_{L}$ , $PK$ , and ${PK}_{L}$ .
Proof.
The equivalences $WF \equiv_{sW} {WF}_{L}$ , $\hat{WF} \equiv_{sW} {\hat{WF}}_{L}$ , and $PK \equiv_{sW} {PK}_{L}$ all follow immediately from Lemma 9 and Theorem 6. It suffices to show that $\hat{WF} \equiv_{sW} PK$ .

To see that $\hat{WF} ⩽_{sW} PK$ , let ${⟨ T_{i} ⟩}_{i \in N}$ be a sequence of trees, the input for $\hat{WF}$ . For sequences σ and τ with $| σ | = | τ |$ , let $σ * τ$ denote the sequence consisting of alternating entries of σ and τ. Thus for σ and τ of length $n + 1$ , $σ * τ = ⟨ σ (0), τ (0), \dots, σ (n), τ (n) ⟩$ . Define the tree T by including the following sequences:
$⟨ i ⟩ \in T$ for each $i \in N$ , and

if $σ \in T_{i}$ , $| σ | = n$ , and τ is a binary sequence of length n, then ${⟨ i ⟩}^{⌢} (σ * τ) \in T$ and the initial segment of ${⟨ i ⟩}^{⌢} (σ * τ)$ omitting the last element is also in T.
The tree T is uniformly computable from the sequence ${⟨ T_{i} ⟩}_{i \in N}$ . If $T_{i}$ has an infinite path p, then for every binary sequence τ, all initial segments of ${⟨ i ⟩}^{⌢} (p * τ)$ are in T. In this case, there is a perfect subtree of T above $⟨ i ⟩$ , so $⟨ i ⟩$ is in the perfect kernel of T. If $T_{i}$ is well-founded, then the subtree of extensions of $⟨ i ⟩$ in T is also well-founded, so no perfect subtree of T contains $⟨ i ⟩$ . Thus, if K is a perfect kernel for T, then $T_{i}$ is well-founded if and only if $⟨ i ⟩ \in K$ . Summarizing, $Z = {i ∣ ⟨ i ⟩ \in K}$ is the desired output for $\hat{WF}$ .

To see that $PK ⩽_{sW} \hat{WF}$ , let T be an input tree for $PK$ . In the following, we freely conflate finite sequences with their natural number codes. For each finite sequence σ, we define the tree $T_{σ}$ . If $σ \notin T$ , then $T_{σ}$ is empty. If $σ \in T$ , then define $T_{σ}$ as follows:
$⟨ σ ⟩ \in T_{σ}$ , and

if $⟨ σ, \dots, ⟨ τ_{0}, \dots, τ_{m} ⟩ ⟩ \in T_{σ}$ , and for each $i ⩽ m$ , $τ_{i}^{⌢} e_{i, 0}$ and $τ_{i}^{⌢} e_{i, 1}$ are incompatible extensions of $τ_{i}$ in T, then $\begin{matrix} ⟨ σ, \dots, ⟨ τ_{0}, \dots, τ_{m} ⟩, ⟨ τ_{0}^{⌢} e_{0, 0}, τ_{0}^{⌢} e_{0, 1}, \dots, τ_{m}^{⌢} e_{m, 0}, τ_{m}^{⌢} e_{m, 1} ⟩ ⟩ \in T_{σ} . \end{matrix}$
The sequence ${⟨ T_{σ} ⟩}_{σ \in N^{< N}}$ (which can be viewed as ${⟨ T_{i} ⟩}_{i \in N}$ ) is uniformly computable from T. For each finite sequence σ, $T_{σ}$ has an infinite path if and only if σ is contained in a perfect subtree of T. Let Z be a solution of $\hat{WF}$ for ${⟨ T_{σ} ⟩}_{σ \in N^{< N}}$ . Then $Z = {σ \in N^{< N} ∣ T_{σ} is well-founded}$ , and $K = {σ \in N^{< N} ∣ σ \notin Z}$ is the perfect kernel of T. □

4. An application

This section presents a Weihrauch analysis closely related to Theorem 6 of Davis, Hirst, Pardo, and Ransom [4]. A hypergraph $H = (V, E)$ consists of a set of vertices $V = {v_{0}, v_{1}, \dots}$ and a set of edges $E = {e_{1}, e_{2}, \dots}$ , where each edge in E is a set of vertices. For hypergraphs, an edge can be a set of any cardinality. If every edge of a hypergraph has cardinality exactly 2, then H is a graph. A k-coloring of a hypergraph $H = (V, E)$ is a function $f : V \to k$ . A k-coloring is called proper if every edge with at least two vertices contains vertices of different colors. Let $HPC (k)$ be the problem that accepts a hypergraph H as input, outputs 1 if H has a proper k-coloring, and outputs 0 otherwise.

The second part of the proof of the following theorem applies a leaf management result from the preceding section.

Theorem 12.

For all $k ⩾ 2$ , $HPC (k) \equiv_{sW} WF$ .

Proof.

To see that $HPC (k) ⩽_{sW} WF$ , let $H = (V, E)$ be a hypergraph input for $HPC (k)$ . In the following, we freely conflate vertices and finite collections of vertices with their integer codes. Build a tree T by including sequences $σ = ⟨ σ_{0}, σ_{1}, \dots, σ_{m} ⟩$ satisfying the following conditions for each $i ⩽ m$ .

If $i = 2 j$ , then $σ_{i}$ is a set of two vertices in edge $e_{j}$ , or $σ_{i}$ is a code for ∅ and $e_{j}$ does not contain a pair of vertices in the list ${v_{0}, \dots, v_{m}}$ .

If $i = 2 j + 1$ , then $σ_{i} < k$ . We view this as a color for $v_{j}$ .

The partial coloring of H given by the odd entries of σ uses distinct colors on the pairs of vertices listed in the even entries.

The odd entries of any infinite path in T encode a proper k-coloring of H. Also, any proper k-coloring of H can be used to define an infinite path through T. (If H has no edges of cardinality less than 2, an infinite path can be uniformly computed from any proper coloring, but this is not necessary for the current argument.) Thus,

HPC (k)

is 1 for H if and only if

WF

is 0 for T.

By Theorem 11, $WF \equiv_{sW} {WF}_{L}$ , so to complete the proof it suffices to show that ${WF}_{L} ⩽_{sW} HPC (k)$ . We will prove this for $k = 2$ and indicate how to modify the argument for larger values of k.

Let T be an input for ${WF}_{L}$ , that is, a tree with a leaf set. Emulating the construction from the proof of Theorem 6 of Davis et al. [4], define a hypergraph H as follows. The vertices of H include the five vertices ${a_{0}, a_{1}, b_{0}, b_{1}, s}$ plus two vertices labeled $σ_{0}$ and $σ_{1}$ for each sequence $σ \in T$ . The edges of H consist of

$(a_{0}, a_{1})$ , $(a_{1}, s)$ , $(b_{0}, b_{1})$ , and $(b_{1}, s)$ ,

$(σ_{0}, σ_{1})$ for every nonempty $σ \in T$ ,

$(σ_{1}, s)$ if σ is a leaf of T,

$E_{σ} = {σ_{1}} \cup {τ_{0} ∣ τ \in T \land \exists n τ = σ^{⌢} n}$ if $σ \in T$ is not a leaf, and

$E_{0} = {a_{0}, b_{0}} \cup {σ_{0} ∣ σ \in T \land | σ | = 1}$ .

H is uniformly computable from T and its leaf set. Note that the leaf set is used in the third and fourth bullets. H has a proper 2-coloring if and only if T has an infinite path. For details, see the proof of Theorem 6 of [4]. Thus

{WF}_{L} ⩽_{sW} HPC (2)

. To prove the reduction for larger values of k, modify the construction by adding a complete subgraph on

k - 2

vertices to H and connecting each of its vertices to every vertex of H with an edge consisting of two vertices. □

Parallelization yields the Weihrauch analog of part of the reverse mathematical Theorem 6 of Davis et al. [4].

Corollary 13.

For $k ⩾ 2$ , $\hat{WF} \equiv_{sW} \hat{HPC} (k)$ .

Proof.

Fix k. By Theorem 12, $WF \equiv_{sW} HPC (k)$ , so by Proposition 3.6 part (3) of Brattka, Gherardi, and Pauly [3], $\hat{WF} \equiv_{sW} \hat{HPC} (k)$ □

The arguments used in Theorem 6 of [4] can be used to extend Theorem 12 and Corollary 13 to conflict-free colorings.

Footnotes

Acknowledgements

A talk related to this paper was presented at Dagstuhl Seminar 18361, organized by Vasco Brattka, Damir Dzhafarov, Alberto Marcone, and Arno Pauly, and held September 2–7 of 2018 at Schloss Dagstuhl, the Leibniz-Zentrum für Informatik []. The author’s travel to the seminar was supported by a Board of Trustees travel grant from Appalachian State University.

References

Brattka,

Dzhafarov,

Marcone and

Pauly, Measuring the complexity of computational content: From combinatorial problems to analysis (Dagstuhl Seminar 18361), Dagstuhl Reports8 (2018), to appear.

Brattka and

Gherardi, Effective choice and boundedness principles in computable analysis, Bull. Symbolic Logic17(1) (2011), 73–117. ISSN 1079-8986. doi:10.2178/bsl/1294186663.

Brattka,

Gherardi and

Pauly, Weihrauch complexity in computable analysis, 2017, 50+xi pages, arXiv:1707.03202.

Davis,

Hirst,

Pardo and

Ransom, Reverse mathematics and colorings of hypergraphs, Arch. Math. Logic (2018). doi:10.1007/s00153-018-0654-z.

Friedman and

Hirst, Weak comparability of well orderings and reverse mathematics, Ann. Pure Appl. Logic47(1) (1990), 11–29. ISSN 0168-0072. doi:10.1016/0168-0072(90)90014-S.

Kihara,

Marcone and

Pauly, Searching for an analogue of ATR₀ in the Weihrauch lattice, 2018, 35 pages, arXiv:1812.01549.

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. 444. ISBN 978-0-521-88439-6. doi:10.1017/CBO9780511581007.