English

Provable better quasi orders

Logic 2023-05-03 v1

Abstract

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

Keywords

Cite

@article{arxiv.2305.01066,
  title  = {Provable better quasi orders},
  author = {Anton Freund and Alberto Marcone and Fedor Pakhomov and Giovanni Soldà},
  journal= {arXiv preprint arXiv:2305.01066},
  year   = {2023}
}
R2 v1 2026-06-28T10:22:51.216Z