Laver's theorem
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;{{r|fraisse}} Richard Laver proved the conjecture in 1971. More generally, Laver proved the same result for order embeddings of countable unions of scattered orders.{{r|harzheim|laver}}
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).{{r|hirschfeldt}} 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.{{r|montalban}}
See also
References
{{reflist|refs=
| last = Fraïssé | first = Roland | authorlink = Roland Fraïssé
| journal = Comptes Rendus Hebdomadaires des Séances de l'Académie des Sciences
| language = French
| mr = 28912
| pages = 1330–1331
| title = Sur la comparaison des types d'ordres
| url = http://gallica.bnf.fr/ark:/12148/bpt6k31787/f1330
| volume = 226
| year = 1948}}; see Hypothesis I, p. 1331
| last = Harzheim | first = Egbert
| at = Theorem 6.17, p. 201
| doi = 10.1007/b104891
| isbn = 0-387-24219-8
| publisher = Springer
| title = Ordered Sets
| series = Advances in Mathematics
| year = 2005| volume = 7
}}
| last = Hirschfeldt | first = Denis R.
| publisher = World Scientific
| series = Lecture Notes Series of the Institute for Mathematical Sciences, National University of Singapore
| title = Slicing the Truth
| title-link = Slicing the Truth
| volume = 28
| year = 2014}}; see Chapter 10
| last = Laver | first = Richard | authorlink = Richard Laver
| doi = 10.2307/1970754
| issue = 1
| journal = Annals of Mathematics
| jstor = 1970754
| pages = 89–111
| title = On Fraïssé's order type conjecture
| volume = 93
| year = 1971}}
| last = Montalbán | first = Antonio
| doi = 10.1142/S0219061317500064
| issue = 2
| journal = Journal of Mathematical Logic
| mr = 3730562
| page = 1750006, 12
| title = Fraïssé's conjecture in -comprehension
| volume = 17
| year = 2017}}
}}
{{Order theory|state=collapsed}}