We now turn from Ramsey theory to another important branch of combinatorics: WQO theory. Like Ramsey theory, WQO theory is of special interest from the viewpoint of reverse mathematics, because many of the proofs seem to need unusually strong set existence axioms.
A quasiordering is a set Q together with a reflexive, transitive relation on Q. A well quasiordering (abbreviated WQO) is a quasiordering such that for every function there exist such that m<n and . Let be the space of infinite subsets of . A better quasiordering (abbreviated BQO) is a quasiordering such that for every Borel function there exists such that . It can be shown that every BQO is a WQO but not conversely.
Generally speaking, WQO theory is an appropriate tool when considering quasiorderings of finite structures, but BQO theory is better adapted to infinite structures. For example, a famous theorem of WQO theory is Kruskal's theorem:
Finite trees are WQO under embeddability.(Here a tree is a connected acyclic graph, and embeddings are required to take vertices to vertices, and edges to paths.) Kruskal's theorem has been generalized to infinite trees, but the proof is much more difficult and involves BQO theory. Detailed references are in [32, §X.3].
There are some important results about the strength of various theorems of WQO theory. For instance, Friedman (see Simpson ) showed that Kruskal's theorem is not provable in , and he characterized exactly the strength of Kruskal's theorem, in proof-theoretic terms. This had remarkable consequences for Friedman's foundational program of finding mathematically natural, finite combinatorial statements which are proof-theoretically strong.
Consider now the following generalization of Kruskal's theorem, due to Kriz . Let T1 and T2 be finite trees where each edge is labeled with a positive integer. Write to mean that there exists an embedding of T1 into T2 such that the label of each edge of T1 is less than or equal to the minimum of the labels of the corresponding edges of T2. Kriz's theorem says that this quasiordering is a WQO.
What is the strength of Kriz's theorem? By results of Friedman (see Simpson ), Kriz's theorem is at least as strong as - . It may be much stronger, but little is known. This is an open problem which may have a big payoff.
We now consider a famous theorem of BQO theory. If Q is a countable quasiordering, let be the set of countable transfinite sequences of elements of Q. Quasiorder by putting if and only if there exists a one-to-one order-preserving map such that for all i<lh(s). The Nash-Williams transfinite sequence theorem [28,35] says that if Q is BQO then is BQO.
Marcone  has shown that the Nash-Williams theorem is provable in - but not equivalent to - . Shore  has shown that the Nash-Williams theorem implies over . There remains the problem of closing the gap. We conjecture that the Nash-Williams theorem is provable in , hence equivalent to over .
Another famous theorem of BQO theory is Laver's theorem [28,35]:
The set of all countable linear orderings is WQO (in fact BQO) under embeddability.The strength of Laver's theorem is an open problem. Shore  has shown that Laver's theorem implies over , and we conjecture that Laver's theorem is provable in .