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.

翻译：无论是经典逻辑还是直觉主义逻辑传统，都无法完美契合计算推理的目的，因为这两种逻辑传统通常无法直接表达任意的一般递归函数而不导致不一致性。我们引入了基础算术（Grounded Arithmetic，简称GA），这是一个简约而强大的形式推理基础，允许直接表达任意的递归定义。GA调整了传统的推理规则，使得表达非终止计算的项无害地表示无语义值（即“底”），而非导致逻辑悖论或不一致性。在GA中，递归函数的终止性本质上可通过“动态类型化”项来证明，或等价地，通过GA的推理规则符号化地反向执行它们所表示的计算。一旦递归函数被证明终止，关于其结果的逻辑推理便简化为熟悉的经典规则。GA的基本无量词片段已在Isabelle/HOL中通过机械验证的一致性证明。量词可作为普通计算添加于此基础之上，其推理规则因此是可接纳的，且不会引入新的不一致性风险。尽管GA仅是迈向丰富类型化基础演绎的第一步，尚不足以满足手动或自动化计算推理的日常实用需求，但它展示了将任意递归定义的表达自由原则上融入形式系统的潜力。