AI 中文总结
研究提出自反基础算术RGA，其真值基于计算，全称量化自反。允许递归定义并证明加法乘法全性，能表示递归可枚举集且一致。经机器验证有可靠性、一致性等多种性质，所得逻辑处于独特子结构角落。
AI 中文摘要
哥德尔不完全性定理的非正式表述常说：“没有一个包含算术的一致形式系统是完全的”，却忽略了所证定理假定经典逻辑这一事实。本文提出自反基础算术（RGA），一种超完全算术，其中真值基于计算而非经典的假定，全称量化基于自反：当系统自身的证明搜索验证其模式实例时全称陈述为真，反驳特定数字实例时为假。RGA允许无约束递归定义，将加法和乘法的全性证明为内部量化定理，精确表示递归可枚举集，且保持一致性。通过Isabelle/HOL机器检查证明了其可靠性、一致性、开放完全性、N - 可靠性、丘奇 - 图灵表达能力特征以及ω - 不完全性。所得逻辑处于与经典和直觉主义算术不同的马尔可夫风格子结构角落。
英文摘要
Informal statements of Gödel's incompleteness theorems often run: "no consistent formal system with arithmetic can be complete" - omitting the fact that the theorems as proved assume classical logic. This paper presents reflective grounded arithmetic (RGA), a paracomplete arithmetic in which truth is grounded in computation rather than assumed by classical fiat, and in which universal quantification is grounded reflectively: a universal statement is true when the system's own proof search certifies its schematic instance, and false when it refutes a particular numeral instance. RGA permits unconstrained recursive definitions, proves the totality of addition and multiplication as internally quantified theorems, and represents exactly the recursively enumerable sets - the ingredient list of the folklore Gödel statement - while remaining consistent. This work proves, with all results machine-checked in Isabelle/HOL: soundness and consistency; open completeness - provability coincides with grounded truth on well-formed statements; N-soundness - every provable totality claim is backed by an actual value; a Church-Turing characterization of RGA's expressive power; and $ω$-incompleteness - grounded truth is recursively enumerable, and therefore some family of statements has every numeric instance provable while its universal closure is not merely unprovable but semantically ungrounded. The resulting logic occupies a Markov-flavored, substructural corner distinct from both classical and intuitionistic arithmetic: double-negation elimination holds, quantified excluded middle fails, refuted universals yield explicit counterexample witnesses, and the deduction theorem's abstraction direction fails precisely at ungrounded hypotheses.
