On Nash-Williams' Theorem regarding sequences with finite range
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866911884750356480 |
|---|---|
| author | Pakhomov, Fedor Soldà, Giovanni |
| author_facet | Pakhomov, Fedor Soldà, Giovanni |
| contents | 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án 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 $α$-wqo's in a way that is formalizable within primitive-recursive set theory with urelements, in a smooth and code-free fashion. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_13842 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | On Nash-Williams' Theorem regarding sequences with finite range Pakhomov, Fedor Soldà, Giovanni Logic 06A07 03B30 03F35 03E30 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án 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 $α$-wqo's in a way that is formalizable within primitive-recursive set theory with urelements, in a smooth and code-free fashion. |
| title | On Nash-Williams' Theorem regarding sequences with finite range |
| topic | Logic 06A07 03B30 03F35 03E30 |
| url | https://arxiv.org/abs/2405.13842 |