Provable better quasi orders

Abstract

It has recently been shown that fairly strong axiom systems such as ${\mathsf{ACA}}_0$ cannot prove that the antichain with three elements is a better quasi order ($\mathsf{bqo}$). In the present paper, we give a complete characterization of the finite partial orders that are provably $\mathsf{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 $\mathsf{AC}{\mathsf{A}}_0$. In sharp contrast, a recent result shows that the same version is equivalent to ${\Pi }_2^1$-comprehension over the stronger base theory ${\mathsf{ATR}}_0$.