Higman's Lemma for Better Quasi-Orders is Provable in ATR₀

Explore a mathematical lecture demonstrating that Higman's lemma for better quasi-orders (bqo's) is provable within the formal system ATR₀. Learn about the classical Higman's lemma from well-quasi-order theory, which states that for any well-quasi-order P, the embeddability order P* on finite sequences over P forms a well-quasi-order. Discover how better quasi-orders represent a natural class of well-quasi orders with strong closure properties, and examine Nash-Williams theorem asserting that for a bqo P, the embeddability order on transfinite sequences over P forms a bqo. Understand Marcone's previous work proving that Nash-Williams theorem is provable in Π¹₁-CA₀, implies ATR₀, and over ATR₀ is equivalent to Higman's lemma for bqo's. Follow the proof that Higman's lemma for bqo's is provable in ATR₀, which also establishes that Nash-Williams theorem is provable in ATR₀. Examine the main technical innovation of iterated ideal orders I_α(P), including the proof that P is bqo if and only if all I_α(P) are well-quasi-orders, and the demonstration that orders I_α(P*) behave predictably when P is a bqo. This research represents joint work with Giovanni Soldà and was presented as part of the Workshop on "Reverse Mathematics: New Paradigms" at the Erwin Schrödinger International Institute for Mathematics and Physics.