Have a thing? Reasoning around recursion with dynamic typing in grounded arithmetic
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.