Goodstein at the Second Threshold: An Independence Result for $ID_2$
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866911559810285568 |
|---|---|
| author | Gjetaj, Oriola Weiermann, Andreas |
| author_facet | Gjetaj, Oriola Weiermann, Andreas |
| contents | The classical Goodstein process, defined via hereditary base-$k$ exponential normal form, is a well-known example of a principle unprovable in Peano Arithmetic. In this paper, we generalize this framework by constructing a new Goodstein process based on the Hardy hierarchy. We develop an ordinal notation system utilizing a two-step collapsing procedure, which yields a proof-theoretic ordinal of $ψ_0ψ_1(\varepsilon_{Ω_2+1})$. By defining $k$-normal forms for natural numbers within this system, we introduce a Goodstein-type process and demonstrate that the theory of non-iterated positive inductive definitions for two operators ($ID_2$) cannot prove its termination. This result establishes a new independence result at the second proof-theoretic threshold, further extending the reach of Goodstein-type principles beyond the Bachmann-Howard level. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_00771 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Goodstein at the Second Threshold: An Independence Result for $ID_2$ Gjetaj, Oriola Weiermann, Andreas Logic The classical Goodstein process, defined via hereditary base-$k$ exponential normal form, is a well-known example of a principle unprovable in Peano Arithmetic. In this paper, we generalize this framework by constructing a new Goodstein process based on the Hardy hierarchy. We develop an ordinal notation system utilizing a two-step collapsing procedure, which yields a proof-theoretic ordinal of $ψ_0ψ_1(\varepsilon_{Ω_2+1})$. By defining $k$-normal forms for natural numbers within this system, we introduce a Goodstein-type process and demonstrate that the theory of non-iterated positive inductive definitions for two operators ($ID_2$) cannot prove its termination. This result establishes a new independence result at the second proof-theoretic threshold, further extending the reach of Goodstein-type principles beyond the Bachmann-Howard level. |
| title | Goodstein at the Second Threshold: An Independence Result for $ID_2$ |
| topic | Logic |
| url | https://arxiv.org/abs/2604.00771 |