Well-Ordered Linearizations

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 partial order $(P,\le_P)$ is well-founded if it has no infinite strictly descending sequence. A linearization is a linear order on the same underlying set extending $\le_P$. Let $\mathsf{EXT}(\omega^*)$ assert that every well-founded partial order has a well-founded linearization.

Statement recorded in the supplied source.

Is $\mathsf{EXT}(\omega^*)$ equivalent to $\mathsf{ACA}_0$ over $\mathsf{RCA}_0$? [S2]

Short English statement

Does guaranteeing a well-ordered extension of every well-founded countable partial order require exactly arithmetical comprehension?

Sources

• S1 ULAM.AI and the UnsolvedMath Contributors, UnsolvedMath: A Curated Collection of Open Mathematics Problems, record 7500120 (AMR-074-0120). 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 20, Section 4.1, p. 8. https://math.berkeley.edu/~antonio/papers/questionsRM.pdf.