While Kripke inspired numerous alternative approaches to truth and paradox,
could we accomplish something like ordinary “working mathematical reasoning” in
any of them? Yes. Grounded arithmetic (GA) combines paracomplete reasoning
and computational semantics into a concrete, usable, and powerful Peano-esque
formal theory of natural numbers and computation. GA weakens key classical
inference rules with “habeas quid” preconditions: obligations to prove we “have
a thing” before using it in subsequent reasoning. In reward for this
inconvenience, GA permits unconstrained recursive definitions of both functions
and predicates, including traditional classical and intuitionistic paradoxes
like the Liar or Curry’s, but also including useful constructs like a simple
mutually-recursive formulation of Cantor pairings. GA includes powerful
quantifiers that yield a natural resolution of Yablo’s paradox. In contrast
with classical arithmetic, all of GA’s logical connectives including
quantifiers reduce to ordinary computations in basic grounded arithmetic (BGA),
a minimalistic formal foundation for recursive computation. A
mechanically-checked metatheory development shows that BGA has properties
defying the conventional interpretation of Gödel’s incompleteness theorems by
being simultaneously (a) semantically and syntactically consistent, (b)
semantically complete, and (c) sufficiently powerful to represent any recursive
(Turing-complete) computation. Ongoing work reinterpreting classical results
from this Kripke-inspired paracomplete perspective suggests that Cantor’s
theorem may have (always) been a “paradox in hiding” and that the Axiom of
Choice may have been blameless for the Banach-Tarski paradox.