Have a thing? Reasoning around recursion with dynamic typing in grounded arithmetic
Elliot Bobrow, Bryan Ford, Stefan Milenković
TL;DR
This work introduces grounded arithmetic (GA), a paracomplete formal foundation that permits direct expression of arbitrary recursive definitions by using dynamic typing (habeas quid) to prevent inconsistency from nonterminating computations. It develops a quantifier-free core, Basic Grounded Arithmetic (BGA), with detailed operational semantics and a consistency proof, and then extends to full GA with computable quantification that is realized as reflective computation. The paper also reports a mechanically verified Isabelle/HOL formalization of BGA and parts of GA, and discusses pathways toward richer type systems, automation, and implications for Gödel-type results in grounded settings. Overall, GA offers a viable avenue for expressive, termination-aware reasoning about computation while maintaining logical soundness in a paracomplete regime, with potential practical impact for formal verification and automated reasoning about complex computations.
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., "bottom") 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.