Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.34548

Inductive Grounded Arithmetic: Goodstein, the Hydra, and $Γ_0$

Bryan Ford
View original source ↗Read source document ↗Export metadata ↓

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 $φ(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.

Explore related subjects

math.LOcs.LOcs.PL

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Bryan Ford. 2026-10-25. Inductive Grounded Arithmetic: Goodstein, the Hydra, and $Γ_0$. https://arxiv.org/abs/2610.34548

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Integration in Hensel minimal fields

We develop a framework of motivic integration in the style of Hrushovski--Kazhdan in arbitrary Hensel minimal fields of equicharacteristic zero. Hence our work generalizes that of Hrushovski--Kazhdan and Yin, but applies more broadly to discretely valued fields, almost real closed fields with analytic structure, pseudo-local fields, and coarsenings. In more detail, we obtain isomorphisms of Grothendieck rings of definable sets, with or without volume forms, in the valued field sort and in the leading term sort. Along the way we develop a theory of effective 1-h-minimal structures, where finite definable sets can be lifted from the leading term sort to the valued fields sort. We show that many natural examples of 1-h-minimal structures are effective, and develop dimension theory and a theory of differentiation in $\mathrm{RV}$ for effective structures.

math.LO↗
arXiv2026

Bistationary Traces, Wide Levels, and Branch-Cover Rigidity for an Unrestricted Typed Variant of the Hayut-Magidor Forcing

For every uncountable regular cardinal $α$, $\mathbb S^{\ast}(α)$ is an explicitly typed four-coordinate forcing motivated by the ladder-system construction of Hayut and Magidor. The forcing is $σ$-closed and, after adjoining a formal maximum, $α$-strategically closed. For $α\geqω_2$, every nonempty countable family of designated generic branches has a stationary and costationary common trace on the generic ladder-coordinate set $L_α$, while no countable family of cofinal branches generates $L_α$. These conclusions persist under a Kurepa-style level-size bound. In the unrestricted forcing, for every infinite cardinal $μ<α$ in the ground model, some level of the generic tree contains a copy of $({}^μ2)^V$. Consequently, the endpoint-corrected restriction family indexed by $\mathcal P_{ω_2}α$ is too wide, whereas the scaled restriction system indexed by $\mathcal P_αα$ has all levels of size less than $α$ exactly when $α$ is strongly inaccessible in the ground model. When these equivalent conditions hold, the branch-covering number of $L_α$ relative to the scaled system is at least $ω_1$. The low-cofinality empty-value convention also ensures that the set of domains of $L_α$ contains no club in $\mathcal P_αα$. The unrestricted tree clause of the motivating presentation is retained, without asserting forcing equivalence.

math.LO↗
arXiv2026

On the structure of certain valued fields II

We study the structure of finitely ramified henselian valued fields of mixed characteristic with arbitrary residue fields via their residue rings of higher length, where a residue ring of length $n$ is the quotient ring of the valuation ring by the $n$-th power of its maximal ideal. We prove an approximate lifting theorem for homomorphisms between residue rings of higher length and explicitly determine the optimal bound of error of lifting. As applications, we obtain several Ax-Kochen-Ershov principles for relative completeness, relative existential completeness, and existential closedness using the pure ring structures on the residue rings. And we show that any formula on a residue ring of length $k$ is equivalent to a normal form of sentences in pure ordered group structure and special formulas at level $n$, uniformly for all finitely ramified henselian valued fields of mixed characteristic $(0,p)$ and the same initial ramification index $e$. Here, for $n\ge k$, a special formula at level $n$ represents a definable set on a residue ring of length $k$ given by a projection image of a definable set in pure ring structure on a residue ring of length $n$. Also, such $n$ is optimally computed from the precise estimation of error of lifting and depends only on $k$, residue characteristic $p$, and initial ramification index $e$.

math.LO↗