Fact and Fiction in Grounded Set Theory
Bryan Ford
Submitted to arXiv on August 19, 2026
Abstract:
Classical set theory buys its power on credit: its axioms assert totalities no
computation could survey. This paper asks what set theory looks like when truth
must be earned – when, following the discipline of grounded arithmetic (GA), a
statement may be asserted only when a terminating computation backs it, so that
paradoxes harmlessly denote nothing rather than exploding. Developing set
theory mechanically, in Isabelle/HOL, across the four GA proof systems, we find
that the classical axioms sort into a precise anatomy. Sets whose membership
computation settles form a full Boolean algebra — complement included – and
support a calculus reducing the halting problem itself to their operations plus
exactly one set former, the sole entrypoint of undecidability. Hereditary
decided sets get foundation for free and choice as a computation, while the
classical prohibitions (no universal set, no complement) become theorems and
the collecting axioms fail for recursion-theoretic reasons. In the world of
omega grounded arithmetic (OGA), membership becomes three-valued by
proof-theoretic status – affirmed, denied, or fictional: certified decided
yet neither provable nor refutable, valued in an algebra of the system’s own
open questions. There the collecting axioms return in total form with their
failures converted to priced fictions; equality grades into three exact
strengths, with extensionality provably strung between them – pointwise
provable, uniformly a Gödel sentence – yet adoptable as an axiom under a
consistency guarantee that composes. Tarski’s universe axiom, classically an
addition even to ZFC, becomes a theorem, each universe carrying a fiction-free
grounded core. The result is a graded ZF table: every classical axiom’s
verdict, in each world, with machine-checked evidence – ZF fails computably,
but holds fictionally, and the fiction is measurable.
Preprint:
PDF
See also: