Inhabiting Kripke’s truth via a working paracomplete formal arithmetic

The Saul Kripke Center is pleased to announce that Bryan Alexander Ford (DEDIS, EPFL) will deliver a talk on Monday, March 23rd, 2026, from 10:00 am to 12:00 pm at the CUNY Graduate Center (Room 9205). The talk is free and open to all.

Title: Inhabiting Kripke’s truth via a working paracomplete formal arithmetic

Abstract: 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.