Provable Better-Quasi-Orders

It has recently been shown that fairly strong axiom systems such as ACA0 cannot prove that the antichain with three elements is a better-quasi-order (bqo). In the present paper, we give a complete characterization of the finite partial orders that are provably bqo in such axiom systems. The result will also be extended to infinite orders. As an application, we derive that a version of the minimal bad array lemma is weak over ACA0. In sharp contrast, a recent result shows that the same version is equivalent to (Formula presented)-comprehension over the stronger base theory ATR0