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 by embeddability. Shore proved that Fraïssé's Conjecture implies $\mathsf{ATR}_0$ over $\mathsf{RCA}_0$ . This question asks whether this implication can be reversed. That is, does $\mathsf{ATR}_0$ suffice to prove Fraïssé's Conjecture? More generally, what is the precise strength (in the sense of reverse mathematics) of Fraïssé's Conjecture?

Suggest an edit

Definitions

A well-quasi-order (WQO) is a quasi-order with no infinite strictly descending sequence and no infinite antichain (set of pairwise incomparable elements).
$\mathsf{ATR_0}$ is the subsystem of second-order arithmetic axiomatizing arithmetical transfinite recursion—roughly, the ability to iterate arithmetical comprehension along any well-order.

Known Partial Results

Laver's original proof of Fraïssé's Conjecture requires $\Pi^1_2$ -comprehension.
Montalbán proved that Fraïssé's Conjecture is provable from $\Pi^1_1$ -comprehension.
It is known that Fraïssé's Conjecture does not imply $\Pi^1_1$ -comprehension (because Fraïssé's Conjecture is a $\Pi^1_2$ -statement and $\Pi^1_1$ -comprehension cannot be equivalent to any $\Pi^1_2$ -statement).
Shore proved that Fraïssé's Conjecture implies $\mathsf{ATR}_0$ over $\mathsf{RCA}_0$ so $\mathsf{ATR}_0$ is a lower bound on the reverse mathematical strength of Fraïssé's Conjecture.

Reference for the problem statement

[Mon17]Antonio Montalbán, Fraïssé's conjecture in Π¹₁-comprehension, Journal of Mathematical Logic, 2017 [doi]

Comments

Loading comments…