Laver's theorem, in order theory, states that order embeddability 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 (for Fraïssé) and the version for countable unions of scattered orders is denoted LAV (for Laver). 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.
See also
References
- Fraïssé, Roland (1948), "Sur la comparaison des types d'ordres", Comptes Rendus Hebdomadaires des Séances de l'Académie des Sciences (in French), 226: 1330–1331, MR 0028912; see Hypothesis I, p. 1331
- Harzheim, Egbert (2005), Ordered Sets, Advances in Mathematics, vol. 7, Springer, Theorem 6.17, p. 201, doi:10.1007/b104891, ISBN 0-387-24219-8
- Laver, Richard (1971), "On Fraïssé's order type conjecture", Annals of Mathematics, 93 (1): 89–111, doi:10.2307/1970754, JSTOR 1970754
- Hirschfeldt, Denis R. (2014), Slicing the Truth, Lecture Notes Series of the Institute for Mathematical Sciences, National University of Singapore, vol. 28, World Scientific; see Chapter 10
- Montalbán, Antonio (2017), "Fraïssé's conjecture in -comprehension", Journal of Mathematical Logic, 17 (2): 1750006, 12, doi:10.1142/S0219061317500064, MR 3730562
Order theory | |
---|---|
Key concepts | |
Results | |
Properties & Types (list) |
|
Constructions | |
Topology & Orders | |
Related |