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., bottom) 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.

翻译：古典逻辑与直觉主义逻辑传统均未能完美契合计算推理之目的，二者皆无法在保持一致性的前提下允许无约束的递归定义：递归逻辑定义通常须先证明其终止性方可被引入使用。本文提出基础算术（GA），作为一种允许直接表达任意递归定义的形式推理基础。GA通过调整传统推理规则，使得表达非终止计算之项无害地指称无语义值（即底值），而非引发不一致性。在GA中证明递归函数终止性，本质上可通过"动态类型化"项来实现，或等价地通过GA推理规则对其指称的计算进行符号化逆向执行。一旦递归函数被证明终止，关于其结果的逻辑推理即简化为熟悉的古典规则。对基础基础算术（BGA）——GA的最小内核——进行机械验证的形式化开发表明，BGA同时具备以下实用元逻辑性质：（a）语义与句法一致性；（b）语义完备性；（c）足以表达并证明任意封闭图灵完备计算的终止性。由于哥德尔不完备性定理，该组合在古典逻辑中不可实现，但我们的结果并不与哥德尔定理矛盾，因为BGA具有超完备性而非古典性。借助BGA的计算与反射能力，我们发现包括量词在内的基础逻辑算子可在BGA中定义为非原始计算，尽管它们未被作为原始构件包含其中。