Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Goodstein at the Second Threshold: An Independence Result for $ID_2$

Oriola Gjetaj, Andreas Weiermann

Abstract

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.

Goodstein at the Second Threshold: An Independence Result for $ID_2$

Abstract

The classical Goodstein process, defined via hereditary base- 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 . By defining -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 () 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.

Paper Structure

This paper contains 16 sections, 45 theorems, 17 equations.

Table of Contents

  1. Introduction
  2. Notation and Conventions
  3. Construction of ordinal notation system for ID2
  4. Function psi
  5. Notation system OT
  6. Fundamental sequences for ID2
  7. Proof-theoretic properties
  8. Properties of the ordinal notation system for ID2
  9. Ordinal Context
  10. Properties of an ordinal context
  11. Goodstein sequences for ID2
  12. Hardy hierarchy and Goodstein process
  13. Base change operation
  14. Ordinal Assignment
  15. Independence of the Goodstein process
  16. ...and 1 more sections

Key Result

Lemma 1

Properties of function $\psi_1$: $\blacktriangleleft$$\blacktriangleleft$

Theorems & Definitions (121)

  • Definition
  • Lemma 1
  • Definition
  • Lemma 2
  • Definition
  • Definition : The term system $(\mathsf{T},<)$
  • Definition
  • Lemma 3
  • Definition : Operations on $\mathsf{T}$
  • Definition
  • ...and 111 more