Generalized Higman's Theorem and iterated ideals

TL;DR

This paper presents a new, explicit proof of Generalized Higman's Theorem using a transfinite hierarchy of orders, formalizable in $ ext{ATR}_0$, resolving a key open problem in reverse mathematics.

Contribution

It introduces a novel proof technique based on an explicit characterization of orders, enabling formalization in $ ext{ATR}_0$ and advancing understanding of better quasi-orders.

Findings

Characterization of bqo via transfinite hierarchy of ideals

Formalization of the proof in $ ext{ATR}_0$

New insights into the structure of iterated ideals

Abstract

Generalized Higman's Theorem is the direct counterpart of Higman's Theorem that asserts the closure of the class of \emph{better} quasi-orders, instead of the class of \emph{well} quasi-orders, under the construction $P\mapsto P^{<\omega}$ of the embeddability order on finite sequences. Traditionally, this result is obtained as a consequence of very powerful and general techniques of Nash-Williams. In this paper, we propose a new proof of this result that is based on an explicit characterization of the underlying orders. In particular, this new technique allows us to formalize the proof of the result in the formal theory $\mathsf{atr}_0$, thus resolving a long-standing open problem in the field of reverse mathematics. The main ingredient of our proof is the introduction of a transfinite hierarchy of orders $\dot I^*_\alpha(P)$ starting with $\dot I^*_0(P)=P$ and $\dot I^*_{\alpha+1}(P)$ being the inclusion order on ideals of $\dot I^*_{\alpha}(P)$. On one hand, we show that a quasi-order $P$ is a bqo if and only if all $\dot I^*_\alpha(P)$ are wqos. On the other hand, under the assumption that $P$ is a bqo, we show that the $\dot I^*_\alpha(P^{<\omega})$ are wqos, and furthermore give a characterization of their structure in terms of a transfinite iteration of a Higman-like construction. The sufficiently explicit character of this proof allows us to formalize it in a rather straightforward manner.