Reverse Mathematics of Fraïssé's Conjecture

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 linear orders $L,K$, write $L\preccurlyeq K$ if some injective map $e:L\to K$ preserves the order. Let $\mathsf{FRA}$ say that every sequence $(L_i)_{i\in\mathbb N}$ of countable linear orders has $i<j$ with $L_i\preccurlyeq L_j$. Let $\Pi^1_1$-$\mathsf{CA}_0$ denote comprehension for $\Pi^1_1$ formulas, including set parameters.

Statement recorded in the supplied source.

The historical question has two parts: is $\mathsf{FRA}$ equivalent to $\mathsf{ATR}_0$ over $\mathsf{RCA}_0$, and is $\mathsf{FRA}$ provable in $\Pi^1_1$-$\mathsf{CA}_0$? The second part has an affirmative answer in the later Theorem 1.1 cited below. [S3] [S2]

Short English statement

Determine whether Fraïssé's embeddability principle has exactly the strength of arithmetical transfinite recursion; its historical question about a stronger comprehension upper bound was answered affirmatively.

Sources

• S1 ULAM.AI and the UnsolvedMath Contributors, UnsolvedMath: A Curated Collection of Open Mathematics Problems, record 7500121 (AMR-074-0121). 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 21, Section 4.2, p. 9. https://math.berkeley.edu/~antonio/papers/questionsRM.pdf.
• S3 Antonio Montalbán, Fraïssé's conjecture in $\Pi^1_1$-comprehension, author preprint (compiled 2017), Theorem 1.1. https://math.berkeley.edu/~antonio/papers/FraisseDeltaBQO.pdf.