Idealizing Useful Fictions in Omega Grounded Arithmetic
Bryan Ford
arXiv preprint 2607.25533
August 18, 2026
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 ω-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 ω-truth deliberately is not. Within that asymmetry,
incompleteness takes a new form. The Gödel 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.
See also: