Embeddings between well-orderings: computability-theoretic reductions (Q1987213)

For any two well-orders, one always embeds into the other. In fact, for any two well-orders, one is always isomorphic to an initial segment of the other. When considering countable well-orders in subsystems of second-order arithmetic, both of these facts are equivalent to the system of arithmetical transfinite recursion over the base system of recursive comprehension [\textit{S. G. Simpson}; Subsystems of second order arithmetic. Cambridge: Cambridge University Press; Urbana, IL: Association for Symbolic Logic (ASL) (2009; Zbl 1181.03001); \textit{H. M. Friedman} and \textit{J. L. Hirst}; Ann. Pure Appl. Logic 47, No. 1, 11--29 (1990; Zbl 0706.03044)]. The present work analyzes the complexity of producing embeddings between countable well-orders from the perspective of the Weihrauch degrees. Think of a mathematical problem as consisting of a collection of instances and, for each instance, an associated collection of solutions to that instance. In order to apply the methods of computability theory, restrict to problems where all instances and solutions are countable mathematical objects, such as countable well-orders and embeddings between countable well-orders. One such problem \(\mathsf{P}\) Weihrauch reduces to another such problem \(\mathsf{Q}\) (written \(\mathsf{P} \leq_W \mathsf{Q}\)) if there is a uniformly computable procedure for using problem \(\mathsf{Q}\) to solve problem \(\mathsf{P}\). Specifically, \(\mathsf{P} \leq_W \mathsf{Q}\) if there are Turing machines \(\Phi\) and \(\Psi\) such that \(\Phi\) encodes \(\mathsf{P}\)-instances into \(\mathsf{Q}\)-instances and \(\Psi\) decodes \(\mathsf{Q}\)-solutions into \(\mathsf{P}\)-solutions. This means that \(\Phi(I)\) is a \(\mathsf{Q}\)-instance whenever \(I\) is a \(\mathsf{P}\)-instance, and \(\Psi(I, S)\) is a \(\mathsf{P}\)-solution to the \(\mathsf{P}\)-instance \(I\) whenever \(S\) is a \(\mathsf{Q}\)-solution to the \(\mathsf{Q}\)-instance \(\Phi(I)\). Two problems \(\mathsf{P}\) and \(\mathsf{Q}\) that Weihrauch reduce to each other are called Weihrauch equivalent (written \(\mathsf{P} \equiv_W \mathsf{Q}\)) and are thought of as having the same uniform computational content. A problem's Weihrauch equivalence class is called its Weihrauch degree. The comparability of countable well-orders can be phrased as a mathematical problem in the above sense in two different ways: \begin{itemize} \item \(\mathsf{CWO}\): Given two countable well-orders, produce an embedding of one of them onto an initial segment of the other. \item \(\mathsf{WCWO}\): Given two countable well-orders, produce an embedding of one of them into the other. \end{itemize} (\(\mathsf{CWO}\) stands for `comparability of well-orders', and \(\mathsf{WCWO}\) stands for `weak comparability of well-orders'.) In [\textit{T. Kihara} et al., J. Symb. Log. 85, No. 3, 1006--1043 (2020; Zbl 1473.03026)], it is shown that \(\mathsf{WCWO} \leq_W \mathsf{CWO} \equiv_W \mathsf{ATR}\), but whether \(\mathsf{ATR} \leq_W \mathsf{WCWO}\) is left as an open question. Here, \(\mathsf{ATR}\) denotes the problem corresponding to the principle axiom of the arithmetical transfinite recursion axiomatic system. The present work answers the question by showing that \(\mathsf{ATR} \leq_W \mathsf{WCWO}\) indeed holds (Theorem~6.3). Thus \(\mathsf{WCWO} \equiv_W \mathsf{CWO} \equiv_W \mathsf{ATR}\) in the Weihrauch degrees, just as the theorems corresponding to \(\mathsf{WCWO}\) and \(\mathsf{CWO}\) are both equivalent to arithmetical transfinite recursion in the sense of reverse mathematics. Recall now Fraïssé's conjecture/Laver's theorem, which states that the countable linear orders are well-quasi-ordered by the embeddability relation: for any sequence \((L_i)_{i \in \mathbb{N}}\) of countable linear orders, there are \(i < j\) such that \(L_i\) embeds into \(L_j\). Determining the precise axiomatic strength of Laver's theorem is a significant open problem in reverse mathematics [\textit{R. A. Shore}, Prog. Comput. Sci. Appl. Log. 12, 782--813 (1993; Zbl 0820.03037); \textit{A. Montalbán}, J. Math. Log. 17, No. 2, Article ID 1750006, 12 p. (2017; Zbl 1472.03066)]. The present work analyzes Laver's theorem and various restrictions thereof in the Weihrauch degrees. Notably, it is shown that, in the Weihrauch degrees, \(\mathsf{WQO}_\mathrm{LO}\) (i.e., the problem corresponding to Laver's theorem) is strictly below closed choice on Baire space, but it is not below \(\mathsf{ATR}\) (Corollaries~8.2 and~8.5). Whether \(\mathsf{ATR} \leq_W \mathsf{WQO}_\mathrm{LO}\) remains open.