Higman's lemma is a classical statement of wqo theory saying that for any wqo P, the embeddability order P* on finite sequences over P is a wqo. Better quasi-orders (bqo) are a natural class of well-quasi orders that is known to enjoy strong closure properties. Nash-Williams theorem asserts that for a bqo P, the embeddability order on transfinite sequences over P forms a bqo. Marcone had proved that Nash-Williams theorem is provable in Π¹₁-CA₀, implies ATR₀, and furthermore over ATR₀ is equivalent to Higman's lemma for bqo's, i.e. the principle that for any bqo P, P* is also bqo.
We prove Higman's lemma for bqo's in ATR₀ and thus also show that Nash-Williams theorem is provable in ATR₀. Our main technical innovation are the iterated ideal orders I_α(P). On one hand we prove that P is bqo iff all I_α(P) are wqo's. On the other hand we show that the orders I_α(P*) behave in a tame way, when P is a bqo.
This is a joint work with Giovanni Soldà.