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

We consider five equivalent definitions for the notion of well quasi-order and examine how difficult it is to prove the equivalences of these definitions. We show exactly which equivalences hold in the systems RCA_0, RCA_0+RT^1_{<\infty}, RCA_0+CAC, WKL_0, and WKL_0+CAC, as well as in the \omega-model REC, with the exception of one potential implication in the system RCA_0+CAC. (The potentially missing implication depends on the open question of determining whether RCA_0+CAC implies WKL_0+\CAC.) Many of our results show that some implication between these equivalent definitions is not provable in RCA_0 by producing an appropriate "computable counterexample" to the classical equivalence. In some cases, these counterexamples can be extended to show that the implication is not even provable in WKL_0. We also study the difficulty of proving that the notion of well quasi-order is closed under products and intersections.