Internalized Truth in Reflective Grounded Arithmetic
2026-08-17 • Logic in Computer Science
Logic in Computer ScienceProgramming Languages
AI summaryⓘ
The authors discuss a special arithmetic system called Reflective Grounded Arithmetic (RGA) that can define its own notion of truth, something classical systems with arithmetic cannot do due to Tarski's theorem. They use a formal proof assistant, Isabelle/HOL, to build and verify a truth predicate within RGA, showing it works correctly for all formulas including those with quantifiers. Their work also proves key properties connecting truth and provability inside RGA, and they confirm RGA's consistency. This shows that RGA is a solid, self-referential system capable of meaningful mathematical reasoning.
Tarski's undefinability theoremReflective Grounded Arithmetictruth predicateIsabelle/HOLprimitive-recursive functionsinternal proof-checkerconsistencyquantifiersformal systemmetatheorems
Authors
Bryan Ford
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.