On Nash-Williams' Theorem regarding sequences with finite range

TL;DR

This paper proves Nash-Williams' theorem on transfinite sequences with finite range within a specific logical system, establishing its reverse-mathematical equivalence to ATR_0 and introducing new order-theoretic characterizations.

Contribution

It demonstrates that Nash-Williams' theorem is provable in ATR_0, resolving an open problem, and develops a new formal framework for the theory of alpha-wqo's.

Findings

Nash-Williams' theorem is equivalent to ATR_0.

Established new order-theoretic characterizations of transfinite Higman's order.

Developed a formalizable theory of alpha-wqo's within primitive-recursive set theory.

Abstract

The famous theorem of Higman states that for any well-quasi-order (wqo) $Q$ the embeddability order on finite sequences over $Q$ is also wqo. In his celebrated 1965 paper, Nash-Williams established that the same conclusion holds even for all the transfinite sequences with finite range, thus proving a far reaching generalization of Higman's theorem. In the present paper we show that Nash-Williams' Theorem is provable in the system $\mathsf{ATR}_0$ of second-order arithmetic, thus solving an open problem by Antonio Montalb\'an and proving the reverse-mathematical equivalence of Nash-Williams' Theorem and $\mathsf{ATR}_0$. In order to accomplish this, we establish equivalent characterization of transfinite Higman's order and an order on the cumulative hierarchy with urelements from the starting wqo $Q$, and find some new connection that can be of purely order-theoretic interest. Moreover, in this paper we present a new setup that allows us to develop the theory of $\alpha$-wqo's in a way that is formalizable within primitive-recursive set theory with urelements, in a smooth and code-free fashion.