Equivalence between Fraïssé’s conjecture and Jullien’s theorem

We say that a linear ordering L is extendible if every partial ordering that does not embed L can be extended to a linear ordering which does not embed L either. Jullien’s theorem is a complete classification of the countable extendible linear orderings. Fraïssé’s conjecture, which is actually a theorem, is the statement that says that the class of countable linear ordering, quasiordered by the relation of embeddability, contains no infinite descending chain and no infinite antichain. In this paper we study the strength of these two theorems from the viewpoint of Reverse Mathematics and Effective Mathematics. As a result of our analysis we get that they are equivalent over the basic system of RCA 0 + Σ 1 1 - IND . o prove that Fraïssé’s conjecture is equivalent, over RCA 0 , to two other interesting statements. One that says that the class of well founded labeled trees, with labels from { + , − } , and with a very natural order relation, is well quasiordered. The other statement says that every linear ordering which does not contain a copy of the rationals is equimorphic to a finite sum of indecomposable linear orderings. studying the proof theoretic strength of Jullien’s theorem, we prove the extendibility of many linear orderings, including ω 2 and η , using just ATR 0 + Σ 1 1 - IND . Moreover, for all these linear orderings, L , we prove that any partial ordering, P , which does not embed L has a linearization, hyperarithmetic (or equivalently Δ 1 1 ) in P ⊕ L , which does not embed L .