Maximal order types for sequences with gap condition

Abstract

Higman's lemma states that for any well partial order $X$, the partial order $X^*$ of finite sequences with members from $X$ is also well. By combining results due to Girard as well as Sch\"{u}tte and Simpson, one can show that Higman's lemma is equivalent to arithmetical comprehension over $\textsf{RCA}_0$, the usual base system of reverse mathematics. By incorporating Friedman's gap condition, Sch\"{u}tte and Simpson defined a slightly different order on finite number sequences with fewer comparisons. While it is still true that their definition yields a well partial order, it turns out that arithmetical comprehension is not enough to prove this fact. Gordeev considered a symmetric variation of this gap condition for sequences with members from arbitrary well orders. He could show, over $\textsf{RCA}_0$, that his partial order on sequences is well (for any underlying well order) if and only if arithmetical transfinite recursion is available. We present a new and simpler proof of this fact and extend Gordeev's results to weak and strong gap conditions as well as binary trees with weakly ascending labels. Moreover, we compute the maximal order types of all considered structures.