{"id":"arxiv/2608.16140","url":"https://arxiv.org/abs/2608.16140","tags":["math.LO","cs.LO","cs.PL"],"score":0,"title":"Internalized Truth in Reflective Grounded Arithmetic","domain":"math.LO","source":"arxiv","authors":["Bryan Ford"],"reviews":0,"subject":"math.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-08-17","reactions":{}}