Fedor Pakhomov - Higman's lemma for bqo's is provable in ATR₀

This lecture was part of the Workshop on "Reverse Mathematics: New Paradigms" held at the ESI August 4 - 8, 2025.

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à.

Видео Fedor Pakhomov - Higman's lemma for bqo's is provable in ATR₀ канала Erwin Schrödinger International Institute for Mathematics and Physics (ESI)