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 logical
tradition can normally permit the direct expression of arbitrary
general-recursive functions without inconsistency. We introduce grounded
arithmetic or GA, a minimalistic but nonetheless powerful foundation for formal
reasoning that allows the direct expression of arbitrary recursive definitions.
GA adjusts the traditional inference rules such that terms that express
nonterminating computations harmlessly denote no semantic value (i.e.,
⊥) instead of leading into logical paradox or 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 consistency proof in Isabelle/HOL
exists for the basic quantifier-free fragment of GA. Quantifiers may be added
atop this foundation as ordinary computations, whose inference rules are thus
admissible and do not introduce new inconsistency risks. While GA is only a
first step towards richly-typed grounded deduction practical for everyday use
in manual or automated computational reasoning, it shows the promise that the
expressive freedom of arbitrary recursive definition can in principle be
incorporated into formal systems.
See also: