Laver's theorem
Laver's theorem, in order theory, states that order embedding of countable total orders is a well-quasi-ordering. That is, for every infinite sequence of totally-ordered countable sets, there exists an order embedding from an earlier member of the sequence to a later member. This result was previously known as Fraïssé's conjecture, after Roland Fraïssé, who conjectured it in 1948; Richard Laver proved the conjecture in 1971. More generally, Laver proved the same result for order embeddings of countable unions of scattered orders.
In reverse mathematics, the version of the theorem for countable orders is denoted FRA and the version for countable unions of scattered orders is denoted LAV. In terms of the "big five" systems of second-order arithmetic, FRA is known to fall in strength somewhere between the strongest two systems, -CA0 and ATR0, and to be weaker than -CA0. However, it remains open whether it is equivalent to ATR0 or strictly between these two systems in strength.
