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 $\le$ on Q. A well quasiordering (abbreviated WQO) is a quasiordering such that for every function $f:\mathbb{N}\to Q$ there exist $m,n\in\mathbb{N}$ such that m<n and $f(m)\le f(n)$. Let $[\mathbb{N} ]^{\infty}$ be the space of infinite subsets of $\mathbb{N}$. A better quasiordering (abbreviated BQO) is a quasiordering such that for every Borel function $f:[\mathbb{N} ]^{\infty}\to Q$ there exists $X\in[\mathbb{N} ]^{\infty}$ such that $f(X)\le f(X\setminus\{\min(X)\})$. 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 [29]) showed that Kruskal's theorem is not provable in $\mathsf{ATR}_0$, 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₁ and T₂ be finite trees where each edge is labeled with a positive integer. Write $T_1\le T_2$ to mean that there exists an embedding of T₁ into T₂ such that the label of each edge of T₁ is less than or equal to the minimum of the labels of the corresponding edges of T₂. 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 $\Pi^1_1$- $\mathsf{CA}_0$. 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 $\widetilde{Q}$ be the set of countable transfinite sequences of elements of Q. Quasiorder $\widetilde{Q}$ by putting $s\le t$ if and only if there exists a one-to-one order-preserving map $f:\mathrm{lh}(s)\to\mathrm{lh}(t)$ such that $s(i)\le t(f(i))$ for all i<lh(s). The Nash-Williams transfinite sequence theorem [28,35] says that if Q is BQO then $\widetilde{Q}$is BQO.

Marcone [23] has shown that the Nash-Williams theorem is provable in $\Pi^1_1$- $\mathsf{CA}_0$ but not equivalent to $\Pi^1_1$- $\mathsf{CA}_0$. Shore [26] has shown that the Nash-Williams theorem implies $\mathsf{ATR}_0$ over $\mathsf{RCA}_0$. There remains the problem of closing the gap. We conjecture that the Nash-Williams theorem is provable in $\mathsf{ATR}_0$, hence equivalent to $\mathsf{ATR}_0$ over $\mathsf{RCA}_0$.

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 $\mathsf{ATR}_0$over $\mathsf{RCA}_0$, and we conjecture that Laver's theorem is provable in $\mathsf{ATR}_0$.