Formalizing Paradoxes in Grounded Arithmetic using Isabelle/HOL
Ananthajit Srikanth and Bryan Ford
Isabelle Workshop 2026
June 24–25, 2026
Lisbon, Portugal
Abstract:
Standard logical foundations in theorem proving constrain the set of recursive
functions that are directly expressible to avoid inconsistencies. However,
this prevents us from expressing all Turing-complete computations via direct
recursive definitions. We consider Grounded Arithmetic, a reasoning framework
that avoids inconsistency from unconstrained recursive definitions by
“dynamically type-checking” terms. Using the formalization of GA in
Isabelle/HOL, we prove three self-referential statements to be nonterminating
computation: the Liar Paradox, the Truthteller sentence, and Curry’s paradox.
To do so, we model each statement in GA as a function taking a certain number
of steps of computation, and metalogically derive a contradiction if these
terms were to terminate. In turn, this allows us to show that these statements
have no concrete value in our framework. Using our non-standard inference
rules, terms with no concrete value cannot be used in a proof by contradiction,
and thus are inert when reasoning about other computations. We then discuss the
accessibility of our approach, and how it permits us to avoid common
inconsistencies that would otherwise occur when removing constraints from
direct recursive definitions in other formal systems.
Paper:
PDF
See also: