Strengths of Laver and Nash–Williams BQO Theorems

Definitions and mathematical statement

Shared notation.

$\mathbb N=\{1,2,\ldots\}$, and $\mathbb Z,\mathbb Q,\mathbb R,\mathbb C$ denote the integers, rationals, reals and complex numbers. Any other conventions are specified locally.

Work over $\mathsf{RCA}_0$, the subsystem of second-order arithmetic with $\Delta^0_1$ comprehension and $\Sigma^0_1$ induction; all structures and orders are countable and coded by sets of integers. $\mathsf{ACA}_0$ adds comprehension for every arithmetical formula (set parameters allowed), and $\mathsf{ATR}_0$ adds arithmetical transfinite recursion along every coded well-order. Reverse-mathematical equivalence means provability of both implications over this base. For an infinite $M\subseteq\mathbb N$, a barrier $B$ on $M$ is a family of finite increasing sequences from $M$ such that no member is a proper subset of another and every infinite subset of $M$ has an initial segment in $B$. Write $s\triangleleft t$ when some increasing sequence has $s$ as an initial segment and has $t$ as an initial segment after its first element is removed. A quasi-order $(Q,\le_Q)$ is a better-quasi-order (bqo) if every map $f:B\to Q$ on every barrier admits $s\triangleleft t$ with $f(s)\le_Q f(t)$. Here quasi-order means reflexive and transitive. Let $L(Q)$ be the class of countable linear orders whose points have labels in $Q$. Its quasi-order uses order-preserving injections $e$ with each source label $\le_Q$ its image label. For a countable ordinal $\alpha$, let $S_\alpha(Q)$ be all functions $s:\alpha\to Q$, ordered by $s\le t$ if there is a strictly increasing $e:\alpha\to\alpha$ with $s(i)\le_Q t(e(i))$ for every $i<\alpha$. Let $\mathsf{LAV}$ assert that $L(Q)$ is bqo whenever $Q$ is bqo; let $\mathsf{NWT}$ assert that $S_\alpha(Q)$ is bqo whenever $\alpha$ is well-ordered and $Q$ is bqo.

Statement recorded in the supplied source.

Determine separately the exact reverse-mathematical strengths of $\mathsf{LAV}$ and $\mathsf{NWT}$ over $\mathsf{RCA}_0$. [S2]

Short English statement

Which set-existence axioms are exactly necessary for the labelled-linear-order and unrestricted transfinite-sequence bqo closure theorems?

Sources

• S1 ULAM.AI and the UnsolvedMath Contributors, UnsolvedMath: A Curated Collection of Open Mathematics Problems, record 7500124 (AMR-074-0124). CC BY 4.0. https://huggingface.co/datasets/ulamai/UnsolvedMath.
• S2 Antonio Montalbán, Open Questions in Reverse Mathematics, author preprint (17 August 2010), Question 24, Section 4.4, pp. 9--10. https://math.berkeley.edu/~antonio/papers/questionsRM.pdf.