Search papers, labs, and topics across Lattice.
This paper introduces reflective grounded arithmetic (RGA), a novel paracomplete arithmetic framework that grounds truth in computation rather than classical logic, allowing for a more nuanced understanding of universal quantification. RGA proves the totality of addition and multiplication as internally quantified theorems and captures the recursively enumerable sets while maintaining consistency. Key results include soundness, consistency, and a characterization of RGA's expressive power, alongside demonstrating that some universal statements can be semantically ungrounded despite having provable instances.
Grounded truth in arithmetic can be computationally certified, revealing a new landscape where provability and semantic grounding diverge.
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.
