Equivalence between Fraïssé's conjecture and Jullien's theorem (Q2368905)

Fraïssé's conjecture, proved by \textit{R. Laver} [``On Fraïssé's order type conjecture'', Ann. Math. (2) 93, 89--111 (1971; Zbl 0208.28905)], asserts that the class of countable linear orderings is well quasiordered by embeddability. In [``On the strength of Fraïssé's conjecture'', Prog. Comput. Sci. Appl. Log. 12, 782--813 (1993; Zbl 0820.03037)], \textit{R. A. Shore} proved that Fraïssé's conjecture implies ATR\(_0\) over RCA\(_0\). It is unknown if ATR\(_0\) suffices to prove Fraïssé's conjecture. The author contributes to the analysis of Fraïssé's conjecture by showing that it is equivalent over RCA\(_0\) to each of two combinatorial principles: (1) that a class of well-founded labeled trees is well quasiordered, and (2) that every linear ordering which does not contain a copy of the rationals is equimorphic to a finite sum of indecomposable linear orderings. The paper also includes analysis of formulations of Jullien's theorem on scattered linear orderings (often working over RCA\(_0 + \Sigma^1_1-\)IND) and several results on extendibility of specific countable orderings.