Inductive Grounded Arithmetic: Goodstein, the Hydra, and Γ0
Bryan Ford
arXiv preprint 2610.34548
October 25, 2026
Abstract:
What does a recursive definition mean when the logic is grounded, so
that 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
notation system in HOL
follows, and it certifies the Veblen notation as an ordinal below
every .
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
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. Conditional proof at arbitrary hypotheses,
on the other hand, is inconsistent, by Curry’s paradox.
In the semantic sense of
the characterization theorem the one rule makes every positive
definition an inductive definition, and it shows precisely where
implication at a hypothesis that is not provably decided is what has
to be paid for.
See also: