Foundations of BQO Theory and Subsystems of SecondOrder Arithmetic

Abstract. We consider the reverse mathematics of wqo and bqo theory. We survey the literature on the subject, which deals mainly with the more advanced results about wqos and bqos, and prove some new results about the elementary properties of these combinatorial structures. We state several open problems about the axiomatic strength of both elementary and advanced results. A quasi-ordering (i.e. a reflexive and transitive binary relation) is awqo (well quasi-ordering) if it contains no infinite descending chains and no infinite sets of pairwise incomparable elements. This concept is very natural, and has been introduced several times, as documented in [19]. The usual working definition of wqo is obtained from the one given above with an application of Ramsey’s theorem: a quasi-ordering on the setQ is wqo if for every sequence {xn | n ∈ N}of elements ofQ there existm < n such thatxm xn. The notion of bqo (better quasi-ordering) is a strengthening of wqo which was introduced byNash-Williams in the 1960’s in a sequence of papers culminating in [30] and [31]. This notion has proved to be very useful in showing that specific quasi-orderings are indeed wqo. Moreover the property of being bqo is preserve