Computable Quantification in Reflective Grounded Arithmetic
Bryan Ford
arXiv preprint 2607.25533
July 28, 2026
Abstract:
Informal statements of Gödel's incompleteness theorems often run: “no
consistent formal system with arithmetic can be complete” - omitting the fact
that the theorems as proved assume classical logic. This paper presents
reflective grounded arithmetic (RGA), a paracomplete arithmetic in which truth
is grounded in computation rather than assumed by classical fiat, and in which
universal quantification is grounded reflectively: a universal statement is
true when the system's own proof search certifies its schematic instance, and
false when it refutes a particular numeral instance. RGA permits unconstrained
recursive definitions, proves the totality of addition and multiplication as
internally quantified theorems, and represents exactly the recursively
enumerable sets - the ingredient list of the folklore Gödel statement - while
remaining consistent. This work proves, with all results machine-checked in
Isabelle/HOL: soundness and consistency; open completeness - provability
coincides with grounded truth on well-formed statements; N-soundness - every
provable totality claim is backed by an actual value; a Church-Turing
characterization of RGA's expressive power; and ω-incompleteness - grounded
truth is recursively enumerable, and therefore some family of statements has
every numeric instance provable while its universal closure is not merely
unprovable but semantically ungrounded. The resulting logic occupies a
Markov-flavored, substructural corner distinct from both classical and
intuitionistic arithmetic: double-negation elimination holds, quantified
excluded middle fails, refuted universals yield explicit counterexample
witnesses, and the deduction theorem's abstraction direction fails precisely at
ungrounded hypotheses.
See also: