Laver's theorem, inorder theory, states thatorder embeddability of countabletotal orders is awell-quasi-ordering. That is, for every infinitesequence of totally-orderedcountable sets, there exists an order embedding from an earlier member of the sequence to a later member. This result was previously known asFraïssé's conjecture, afterRoland Fraïssé, who conjectured it in 1948;^[1]Richard Laver proved the conjecture in 1971. More generally, Laver proved the same result for order embeddings of countable unions ofscattered orders.^[2][3]

Inreverse mathematics, the version of the theorem for countable orders is denoted FRA (for Fraïssé) and the version for countable unions of scattered orders is denoted LAV (for Laver).^[4] In terms of the "big five" systems ofsecond-order arithmetic, FRA is known to fall in strength somewhere between the strongest two systems,${\displaystyle {\mathrm{\Pi }}_1^1}$-CA₀ and ATR₀, and to be weaker than${\displaystyle {\mathrm{\Pi }}_1^1}$-CA₀. However, it remains open whether it is equivalent to ATR₀ or strictly between these two systems in strength.^[5]

• Dushnik–Miller theorem

• Order theory

• CS1 French-language sources (fr)