Summary
This paper studies a form of arithmetic where statements are true only if there is a terminating, step-by-step process proving them. The authors build a system called Inductive Grounded Arithmetic (IGA) that can handle complex infinite structures and famous mathematical results, like Goodstein's theorem and the hydra game, by grounding every part of the proof in explicit finite steps. Their system is checked by a computer for consistency and aligns perfectly with classical understandings while revealing the exact logical differences from classical truth. Essentially, they show how certain advanced mathematical truths arise within this grounded and inductive framework, pinpointing where classical logic and this approach diverge.
What this means in practice
- •For formal methods engineers: Ensure correctness of proofs about complex recursive structures using grounded induction principles proven consistent by this system.
- •For program verification teams: Use grounded induction rules to certify termination and correctness of programs with complex recursion or infinite-like behavior.
A theory result. No direct application yet.
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 $\varepsilon_0$ notation system in HOL follows, and it certifies the Veblen notation as an ordinal below every $\varphi(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 $\mathcal O$ are interderivable over IGA.