The notion of well quasi-order (WQO) is a natural generalization of well-orders to partial orders. Simply put, a partial order is a WQO if it is well-founded and all its antichains are finite. Several equivalent characterizations of WQO show that the notion is actually quite robust.

In the 1960’s Nash-Williams introduced a strengthening of WQO he called better quasi-order (BQO). This was instrumental in Laver’s 1971 proof of Fraïssé’s conjecture: the collection of countable linear orders is a WQO under embeddability. In fact all proofs of Fraïssé’s conjecture actually establish Laver’s stronger statement: countable linear orders are a BQO under embeddability.

This survey assumes no previous knowledge of WQOs and BQOs: we will start from the definitions and the basic characterizations, then move on to some sample results. We will pay attention to the logic side of the theory, looking at WQO and BQO theory from the viewpoint of ordinal analysis, reverse mathematics and Weihrauch reducibility. For example, it turns out that many proofs and proof techniques in this area require quite strong axioms.

The notion of well quasi-order (WQO) is a natural generalization of that of well-order to partial orders. Simply put, a partial order is a WQO if it is well-founded and all its antichains are finite. Several equivalent characterizations of WQO show that the notion is actually quite robust.

In the 1960’s Nash-Williams introduced a strengthening of WQO he called better quasi-order (BQO). This was instrumental in Laver’s 1971 proof of Fraïssé’s conjecture: the collection of countable linear orders is a WQO under embeddability. In fact all proofs of Fraïssé’s conjecture actually establish Laver’s stronger statement: countable linear orders are a BQO under embeddability.

This survey assumes no previous knowledge of WQOs and BQOs: we will start from the definitions and the basic characterizations, then move on to some sample results. We will pay attention to the logic side of the theory, looking at WQO and BQO theory from the viewpoint of reverse mathematics. In fact many proofs and proof techniques in this area require quite strong axioms.

The notion of well quasi-order (WQO) is a natural generalization of that of well-order to partial orders. Simply put, a partial order is a WQO if it is well-founded and all its antichains are finite. Several equivalent characterizations of WQO show that the notion is actually quite robust.

In the 1960’s Nash-Williams introduced a strengthening of WQO he called better quasi-order (BQO). This was instrumental in Laver’s 1971 proof of Fraïssé’s conjecture: the collection of countable linear orders is a WQO under embeddability. In fact all proofs of Fraïssé’s conjecture actually establish Laver’s stronger statement: countable linear orders are a BQO under embeddability.

This survey assumes no previous knowledge of WQOs and BQOs: we will start from the definitions and the basic characterizations, then move on to some sample results. We will pay attention to the logic side of the theory, looking at WQO and BQO theory from the viewpoint of reverse mathematics. In fact many proofs and proof techniques in this area require quite strong axioms.