Laver's theorem
From Wikipedia, the free encyclopedia
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;[1] Richard Laver proved the conjecture in 1971. More generally, Laver proved the same result for order embeddings of countable unions of scattered orders.[2][3]
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).[4] 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.[5]
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
