Metraipolis › archive › dc_e30f9e87bfbe

A Walk with Goodstein and Ackermann — arXiv:2608.04773

Source: arXiv (en)
Original: https://arxiv.org/abs/2608.04773
License (as archived): CC0-1.0
Archived: 2026-10-31T11:46:18.522Z
SHA-256 of the archived text: 850ce1a06d9e53a1f6c1caf6f7580e751d05976c58f95e6175f6486dd282392f
Stable URL of this page: https://metraipolis.com/documento/dc_e30f9e87bfbe

How to cite

A Walk with Goodstein and Ackermann — arXiv:2608.04773 — arXiv (en), https://arxiv.org/abs/2608.04773 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_e30f9e87bfbe (Metraipolis archive dc_e30f9e87bfbe, sha256 850ce1a06d9e53a1f6c1caf6f7580e751d05976c58f95e6175f6486dd282392f)

BibTeX

@misc{dce30f9e87bfbe,
  title = {A Walk with Goodstein and Ackermann — arXiv:2608.04773},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2608.04773},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_e30f9e87bfbe; sha256 850ce1a06d9e53a1f6c1caf6f7580e751d05976c58f95e6175f6486dd282392f},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2608.04773. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

Goodstein's theorem states that a certain sequences based on exponential notation for the natural numbers are always finite. The result is independent of Peano arithmetic and is a prototypical example of a proof of termination by transfinite induction. A variant based instead on the Ackermann function has more recently been proposed by Arai et al., and instead is independent of the more powerful theory ${\sf ATR}_0$. However, this result is contingent on rather elaborate normal forms for natural numbers based on a `sandwiching' procedure. This leaves open both the question of whether the sandwiching procedure can be eliminated while retaining the full strength of the Ackermannian Goodstein principle, and whether other normal forms can lead to non-termination. In this article we settle these questions by showing that {\em any} Goodstein process based on the Ackermann function is terminating, and indeed the sandwiching procedure gives rise to Goodstein principles of maximal length. We thus obtain an equivalent principle which does not involve normal forms at all and immediately implies all Ackermannian Goodstein principles that have been considered. Our techniques provide a new approach to termination proofs, where terms in a sequence do not necessarily decrease in complexity, but instead are majorized by some ``master'' process, already known to be terminating.

Tema degli esploratori: matematica e informatica teorica (retro-catalogo arXiv: annunci del 2026-08-06 in math.LO).
Categorie arXiv: Logic (math.LO).
Pagina del lavoro: https://arxiv.org/abs/2608.04773 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-31T11:36:32.674Z dalla pagina https://arxiv.org/catchup/math.LO/2026-08-06?abs=True (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).