Maximal order types for sequences with gap condition

TL;DR

This paper investigates the well partial order properties and maximal order types of sequences with various gap conditions, extending previous results and providing new proofs within reverse mathematics.

Contribution

It introduces simplified proofs and extends Gordeev's results to weak and strong gap conditions and binary trees, while computing their maximal order types.

Findings

Sequences with gap conditions form well partial orders under certain logical systems.

Arithmetical comprehension is insufficient for some gap conditions; stronger systems are needed.

The maximal order types of these structures are explicitly computed.

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.