The logical strength of minimal bad arrays

This paper studies logical aspects of the notion of better-quasi-order, which was introduced by C. Nash-Williams [Proc. Cambridge Philos. Soc. 61 (1965), pp. 697–720; Proc. Cambridge Philos. Soc. 64 (1968), pp. 273–290]. A central tool in the theory of better-quasi-orders is the minimal bad array lemma. We show that this lemma is exceptionally strong from the viewpoint of reverse mathematics, a framework from mathematical logic. Specifically, it is equivalent to the set existence principle of <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="normal upper Pi 2 Superscript 1"> <mml:semantics> <mml:msubsup> <mml:mi mathvariant="normal"> Π </mml:mi> <mml:mn>2</mml:mn> <mml:mn>1</mml:mn> </mml:msubsup> <mml:annotation encoding="application/x-tex">\Pi ^1_2</mml:annotation> </mml:semantics> </mml:math> </inline-formula> -comprehension, over the base theory <inline-formula content-type="math/mathml"> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" alttext="sans-serif upper A sans-serif upper T sans-serif upper R sans-serif 0"> <mml:semantics> <mml:mrow class="MJX-TeXAtom-ORD"> <mml:mi mathvariant="sans-serif">A</mml:mi> <mml:mi mathvariant="sans-serif">T</mml:mi> <mml:msub> <mml:mi mathvariant="sans-serif">R</mml:mi> <mml:mn mathvariant="sans-serif">0</mml:mn> </mml:msub> </mml:mrow> <mml:annotation encoding="application/x-tex">\mathsf {ATR_0}</mml:annotation> </mml:semantics> </mml:math> </inline-formula> .