Have a thing? Reasoning around recursion with dynamic typing in grounded arithmetic
Elliot Bobrow, Bryan Ford, and Stefan Milenković
arXiv preprint 2510.25369
October 29, 2025 (first version)
Abstract:
Neither the classical nor intuitionistic logic traditions are perfectly-aligned
with the purpose of reasoning about computation, in that neither tradition can
permit unconstrained recursive definitions without inconsistency: recursive
logical definitions must normally be proven terminating before admission and
use. We introduce grounded arithmetic or GA, a formal-reasoning foundation
allowing direct expression of arbitrary recursive definitions. GA adjusts
traditional inference rules so that terms that express nonterminating
computations harmlessly denote no semantic value (i.e., ⊥) instead of
yielding inconsistency. Recursive functions may be proven terminating in GA
essentially by “dynamically typing” terms, or equivalently, symbolically
reverse-executing the computations they denote via GA's inference rules. Once
recursive functions have been proven terminating, logical reasoning about their
results reduce to the familiar classical rules. A mechanically-checked formal
development of basic grounded arithmetic or BGA – a minimal kernel for GA –
shows that BGA simultaneously exhibits the useful metalogical properties of
being (a) semantically and syntactically consistent, (b) semantically complete,
and (c) sufficiently powerful to express and prove the termination of arbitrary
closed Turing-complete computations. This combination is impossible in
classical logic due to Göel's incompleteness theorems, but our results do not
contradict Gödel's theorems because BGA is paracomplete, not classical.
Leveraging BGA's power of computation and reflection, we find that grounded
logical operators including quantifiers are definable as non-primitive
computations in BGA, despite not being included as primitives
See also: