Computable Quantification in Reflective Grounded Arithmetic

Abstract

Informal statements of G\"odel'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\"odel 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 $\omega$-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.