Inductive Grounded Arithmetic: Goodstein, the Hydra, and Γ0
Abstract
What does a recursive definition mean when the logic is grounded, so a sentence is true only if a terminating process makes it so? Kripke's answer for the special case of truth was the least fixed point. This paper takes that answer as a rule. Reflective Grounded Arithmetic (RGA) already writes any recursive definition as one self-referential term, paradoxes included. Inductive Grounded Arithmetic (IGA) adds the elimination rule for every positive one, so that accessibility, the winning positions of a game, and grounded truth itself each come with their own induction principle. The rule is sound for the omega model and the system is consistent, both machine-checked in Isabelle/HOL. With the rule, IGA proves Goodstein's theorem outright, in a logic without implication at an undecided hypothesis, and the Kirby-Paris hydra game for primitive recursive strategies, both with every step of the arithmetic a grounded derivation. It proves the Cantor normal forms well-founded, from which the well-foundedness of the standard ε0 notation system in HOL follows, and it certifies the Veblen notation as an ordinal below every φ(n,0). It defines Kripke truth for RGA's own language as one fixed point that agrees with the omega model exactly. Two equivalences locate what the classical world has and the grounded one does not. IGA proves the whole Veblen notation well-founded exactly when it admits bivalence of accessibility for that order, and bivalence of accessibility for an order is sound exactly when the order is well-founded; so Γ0 lies at most one instance of excluded middle away, at the accessibility predicate of the notation, and that instance, the well-foundedness sentence and one membership claim in a primitive-recursive form of Kleene's 𝒪 are interderivable over IGA.
Related
- Computable Quantification in Reflective Grounded Arithmetic
- Coinduction in Grounded Arithmetic
- Internal Reasoning and Consistency in Reflective Grounded Arithmetic
- Uniform generalization of Goodstein's theorem and Cichon's independence proof
- Slaying the Hydra: Interaction-Aware Circuit Discovery in Language Models
BibTeX
@misc{ford2026inductive,
title = {{Inductive Grounded Arithmetic: Goodstein, the Hydra, and $Γ_0$}},
author = {Bryan Ford},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2610.34548},
eprint = {2610.34548},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2610.34548},
note = {CC BY-NC-ND 4.0},
}
RIS
TY - UNPB
TI - Inductive Grounded Arithmetic: Goodstein, the Hydra, and Γ_0
AU - Bryan Ford
PY - 2026
DA - 2026/10/25
PB - arXiv
DO - 10.48550/arxiv.2610.34548
UR - https://arxiv.org/abs/2610.34548
AB - What does a recursive definition mean when the logic is grounded, so a sentence is true only if a terminating process makes it so? Kripke's answer for the special case of truth was the least fixed point. This paper takes that answer as a rule. Reflective Grounded Arithmetic (RGA) already writes any recursive definition as one self-referential term, paradoxes included. Inductive Grounded Arithmetic (IGA) adds the elimination rule for every positive one, so that accessibility, the winning positions of a game, and grounded truth itself each come with their own induction principle. The rule is sound for the omega model and the system is consistent, both machine-checked in Isabelle/HOL. With the rule, IGA proves Goodstein's theorem outright, in a logic without implication at an undecided hypothesis, and the Kirby-Paris hydra game for primitive recursive strategies, both with every step of the arithmetic a grounded derivation. It proves the Cantor normal forms well-founded, from which the well-foundedness of the standard ε_0 notation system in HOL follows, and it certifies the Veblen notation as an ordinal below every φ(n,0). It defines Kripke truth for RGA's own language as one fixed point that agrees with the omega model exactly. Two equivalences locate what the classical world has and the grounded one does not. IGA proves the whole Veblen notation well-founded exactly when it admits bivalence of accessibility for that order, and bivalence of accessibility for an order is sound exactly when the order is well-founded; so Γ_0 lies at most one instance of excluded middle away, at the accessibility predicate of the notation, and that instance, the well-foundedness sentence and one membership claim in a primitive-recursive form of Kleene's 𝒪 are interderivable over IGA.
ER -