Reverse mathematics and the equivalence of definitions for well and better quasi-orders

Source abstract

In reverse mathematics, one formalizes theorems of ordinary mathematics in second order arithmetic and attempts to discover which set theoretic axioms are required to prove these theorems. Often, this project involves making choices between classically equivalent definitions for the relevant mathematical concepts. In this paper, we consider a number of equivalent definitions for the notions of well quasi-order and better quasi-order and examine how difficult it is to prove the equivalences of these definitions. As usual in reverse mathematics, we work in the context of subsystems of second order arithmetic and take RCA 0 as our base system. RCA 0 is the subsystem formed by restricting the comprehension scheme in second order arithmetic to formulas and adding a formula induction scheme for formulas. For the purposes of this paper, we will be concerned with fairly weak extensions of RCA 0 (indeed strictly weaker than the subsystem ACA 0 which is formed by extending the comprehension scheme in RCA 0 to cover all arithmetic formulas) obtained by adjoining certain combinatorial principles to RCA 0 . Among these, the most widely used in reverse mathematics is Weak König's Lemma; the resulting theory WKL 0 is extensively documented in [11] and elsewhere. We give three other combinatorial principles which we use in this paper. In these principles, we use k to denote not only a natural number but also the finite set {0, …, k − 1}.