Internalized Truth in Reflective Grounded Arithmetic
Bryan Ford
arXiv preprint 2608.16140
August 17, 2026
Abstract:
By Tarski's undefinability theorem, no consistent classical formal system that
includes arithmetic can define its own truth predicate. Reflective Grounded
Arithmetic (RGA) is a powerful arithmetic whose universal quantifier is
grounded in its own reflected proof search, and whose paracompleteness
circumvents Tarski's theorem. This paper presents a machine-checked
Isabelle/HOL development that defines a truth predicate for RGA's full
language, quantifiers included, as an internal term of RGA itself. This term is
compiled from a primitive-recursive decider for its operational semantics, and
proven adequate in both directions. Around this predicate the development
closes a square of metatheorems: for every formula RGA proves, RGA derives the
formula's internal truth; every grounded-true formula is internally provable;
internal truth implies internal provability; and the consistency of RGA
follows. The two directions run on disjoint internal machines – a certified
decider and a certified proof-checker, both RGA terms. Reaching these results
involved substantial ordinary reasoning carried out within RGA: coded syntax
and substitution, compiled primitive-recursive functions with symbolic
unfolding laws, internal strong induction, and a verified proof-checker for the
system written in the system's own formal language. The development thus
demonstrates along the way that RGA is a workable formal system supporting
nontrivial mathematical reasoning.
See also: