WQO Theory

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

There are some important results about the strength of various theorems of WQO theory. For instance, Friedman (see Simpson [29]) 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 [17]. Let *T*_{1} and *T*_{2} be finite trees where each
edge is labeled with a positive integer. Write
to mean
that there exists an embedding of *T*_{1} into *T*_{2} such that the label
of each edge of *T*_{1} is less than or equal to the minimum of the
labels of the corresponding edges of *T*_{2}. *Kriz's theorem*
says that this quasiordering is a WQO.

What is the strength of Kriz's theorem? By results of Friedman (see Simpson [29]), 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 [23] has shown that the Nash-Williams theorem is provable in - but not equivalent to - . Shore [26] 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 [26] has shown that Laver's theorem implies over , and we conjecture that Laver's theorem is provable in .