Laver's theorem, in
order theory
Order theory is a branch of mathematics that investigates the intuitive notion of order using binary relations. It provides a formal framework for describing statements such as "this is less than that" or "this precedes that". This article intr ...
, states that
order embeddability of countable
total order
In mathematics, a total or linear order is a partial order in which any two elements are comparable. That is, a total order is a binary relation \leq on some set X, which satisfies the following for all a, b and c in X:
# a \leq a ( reflexive) ...
s is a
well-quasi-ordering
In mathematics, specifically order theory, a well-quasi-ordering or wqo is a quasi-ordering such that any infinite sequence of elements x_0, x_1, x_2, \ldots from X contains an increasing pair x_i \leq x_j with i x_2> \cdots) nor infinite sequenc ...
. That is, for every infinite
sequence
In mathematics, a sequence is an enumerated collection of objects in which repetitions are allowed and order matters. Like a set, it contains members (also called ''elements'', or ''terms''). The number of elements (possibly infinite) is calle ...
of totally-ordered
countable set
In mathematics, a set is countable if either it is finite or it can be made in one to one correspondence with the set of natural numbers. Equivalently, a set is ''countable'' if there exists an injective function from it into the natural numbers; ...
s, 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é
Roland Fraïssé (; 12 March 1920 – 30 March 2008) was a French mathematical logician.
Fraïssé received his doctoral degree from the University of Paris in 1953. In his thesis, Fraïssé used the back-and-forth method to determine whether t ...
, who conjectured it in 1948;
Richard Laver
Richard Joseph Laver (October 20, 1942 – September 19, 2012) was an American mathematician, working in set theory.
Biography
Laver received his PhD at the University of California, Berkeley in 1969, under the supervision of Ralph McKenzie, wit ...
proved the conjecture in 1971. More generally, Laver proved the same result for order embeddings of countable unions of
scattered order
In mathematical order theory, a scattered order is a linear order that contains no densely ordered subset with more than one element.
A characterization due to Hausdorff states that the class of all scattered orders is the smallest class of li ...
s.
In
reverse mathematics
Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in cont ...
, 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
In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics.
A precurs ...
, FRA is known to fall in strength somewhere between the strongest two systems,
-CA
0 and ATR
0, and to be weaker than
-CA
0. However, it remains open whether it is equivalent to ATR
0 or strictly between these two systems in strength.
See also
*
Dushnik–Miller theorem
In mathematics, the Dushnik–Miller theorem is a result in order theory stating that every infinite linear order has a non-identity order embedding into itself. It is named for Ben Dushnik and E. W. Miller, who published this theorem for countabl ...
References
{{Order theory, state=collapsed
Order theory