Problem #3

Is Fraïssé's Conjecture Provable in ATR₀?

Open!!

Fraïssé's Conjecture (proved by Laver in 1971) states that the class of countable linear orders is well-quasi-ordered under embeddability: there is no infinite strictly descending sequence and no infinite antichain of countable linear orders under embeddability. Working in the framework of reverse mathematics, it is known that

\mathsf{RCA_0} \vdash \text{Fraïssé's Conjecture} \rightarrow \mathsf{ATR_0},

and it is known that $\mathsf{\Pi^1_2\text{-}CA_0}$ proves Fraïssé's Conjecture. The open question is whether this gap can be closed on the lower end: does

\mathsf{ATR_0} \vdash \text{Fraïssé's Conjecture}?

A positive answer would place Fraïssé's Conjecture exactly at the level of $\mathsf{ATR_0}$ , matching the usual pattern in reverse mathematics where a theorem is shown equivalent to one of the standard "Big Five" subsystems.

Suggest an edit

Reference for the problem statement

Antonio Montalbán, Fraïssé's conjecture in Π¹₂-comprehension, 2017

Definitions

Well-quasi-order (WQO): a quasi-order with no infinite strictly descending sequence and no infinite antichain (set of pairwise incomparable elements).
$\mathsf{ATR_0}$ : the subsystem of second-order arithmetic axiomatizing arithmetical transfinite recursion — roughly, the ability to iterate arithmetical comprehension along any well-order. One of the "Big Five" reference subsystems in reverse mathematics.
$\mathsf{\Pi^1_2\text{-}CA_0}$ : the subsystem with comprehension for $\Pi^1_2$ formulas, substantially stronger than $\mathsf{ATR_0}$ .

Known Partial Results

$\mathsf{RCA_0}$ proves that Fraïssé's Conjecture implies $\mathsf{ATR_0}$ , so $\mathsf{ATR_0}$ is a necessary lower bound.
Montalbán showed that $\mathsf{\Pi^1_2\text{-}CA_0}$ suffices to prove Fraïssé's Conjecture, improving on earlier, weaker upper bounds.
Whether $\mathsf{ATR_0}$ itself already suffices — which would pin down the exact strength of the theorem — remains open.

Notes

This is a natural test case for the general phenomenon, well documented in reverse mathematics, that theorems about well-quasi-orderings tend to be very strong — often stronger than $\mathsf{ATR_0}$ — while this particular case (linear orders) sits right at the boundary where the exact strength is not yet pinned down.

Additional References

Laver, R. "On Fraïssé's order type conjecture." Annals of Mathematics, 1971 (the original proof of the conjecture).
Montalbán, A. "Fraïssé's conjecture in $\Pi^1_2$ -comprehension." (2017) — establishes the current best known upper bound and discusses the remaining gap.
Simpson, S. "Subsystems of Second Order Arithmetic." Cambridge University Press, 2009 (general background on the Big Five and reverse mathematics).

Comments

Loading comments…