Idealizing Useful Fictions in Omega Grounded Arithmetic

Abstract

Grounded arithmetic is a family of formal systems for reasoning about computation in which a statement may be asserted only when a terminating computation backs it; the logics are paracomplete - for a sentence whose backing computation never settles, neither the sentence nor its negation is derivable, so paradoxes like the Liar are harmless rather than explosive. The reflective member of the family, RGA, can quantify over its own computations, but cannot certify that its own unbounded searches have definite yes-or-no answers. This paper studies what happens when that openness is closed by exactly one rule - ATI, the $\omega$-grounded universal: if every numeric instance of a universal sentence is certified decided, the universal is certified decided. The resulting system, OGA, shares RGA's syntax and rules symbol-for-symbol otherwise, and every consequence is developed as a machine-checked theorem. Decidedness certificates become abundant - every totality question about a computable function is certified to have an answer, whether or not anyone can produce it - and this is exactly the provable separation between the two systems. OGA is complete for its own semantics; certified-but-unresolved sentences receive values built from the system's own open questions. Provability remains recursively enumerable, with a primitive-recursive certificate checker, while $\omega$-truth deliberately is not. Within that asymmetry, incompleteness takes a new form. The G\"odel sentence is classified, unconditionally, as a genuine fiction: neither provable nor refutable, yet valued, and carrying a computable pedigree recording exactly what adopting it as an axiom commits one to. The adoption is itself a theorem suite: extending OGA by any finite stock of true fictions is consistent, and independently certified adoptions can never collide.