Strength of Kříž's Labeled-Tree Theorem

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. A finite tree is a finite connected acyclic graph, here with each edge labelled by a positive integer. A topological embedding sends vertices injectively to vertices and each edge to a path between its endpoint images, with path interiors mutually disjoint and disjoint from all image vertices. Put $T\le T^{\prime}$ if such an embedding exists and every source edge label is at most each label on its corresponding target path. Kříž's theorem says that every infinite sequence of these labelled trees has $i<j$ with $T_i\le T_j$.

Statement recorded in the supplied source.

Determine the exact reverse-mathematical strength of this labelled-tree well-quasi-order theorem over $\mathsf{RCA}_0$. [S2]

Short English statement

Which axioms exactly prove well-quasi-ordering of finite trees under topological embeddings that never decrease an edge label?

Sources

• S1 ULAM.AI and the UnsolvedMath Contributors, UnsolvedMath: A Curated Collection of Open Mathematics Problems, record 7500212 (AMR-074-0212). CC BY 4.0. https://huggingface.co/datasets/ulamai/UnsolvedMath.
• S2 Stephen G. Simpson, Open Problems in Reverse Mathematics (15 December 1999), WQO Theory, paragraph beginning Consider now the following generalization. https://sgslogic.net/t20/talks/cta/problems/node8.html.