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 order 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 ( re ...
s is a
well-quasi-ordering
In mathematics, specifically order theory, a well-quasi-ordering or wqo on a set X is a quasi-ordering of X for which every 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) ...
. 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 cal ...
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 numbe ...
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é, 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
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 of mathematics, foundation for much, but not all, ...
, 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
References
{{Order theory, state=collapsed
Order theory