Three-Element Better-Quasi-Order

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. The three-element antichain is $Q=\{0,1,2\}$ with $i\le_Q j$ precisely when $i=j$.

Statement recorded in the supplied source.

Is there a subsystem of second-order arithmetic strictly weaker than $\mathsf{ATR}_0$ over $\mathsf{RCA}_0$ which proves that this antichain is bqo? [S2]

Short English statement

Can the better-quasi-order property of only three incomparable elements be proved with strictly less than arithmetical transfinite recursion?

Sources

• S1 ULAM.AI and the UnsolvedMath Contributors, UnsolvedMath: A Curated Collection of Open Mathematics Problems, record 7500125 (AMR-074-0125). 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 25, Section 4.4, p. 10. https://math.berkeley.edu/~antonio/papers/questionsRM.pdf.
• S3 Anton Freund, On the Logical Strength of the Better Quasi Order with Three Elements, arXiv:2206.11132v2 (10 August 2022), Introduction, pp. 1--2. https://arxiv.org/pdf/2206.11132.