AI 中文总结
本文在根基算术家族的RGA系统基础上，引入ATI规则构建OGA系统，证明其完备性、可证明性为递归可枚举等性质，并将哥德尔语句归类为有用虚构，确立了有限真虚构扩展OGA的一致性。
AI 中文摘要
根基算术是用于推理计算的形式系统家族，其中仅当终止计算支持时才可断言一个陈述；这类逻辑是亚相容的——对于其支持计算永远无法确定的语句，既不能推导该语句也不能推导其否定，因此像说谎者悖论这类悖论是无害的而非爆炸性的。该家族中的反思成员RGA可对自身计算进行量化，但无法证明自身无界搜索具有确定的是或否答案。本文研究通过一条规则ATI（即ω根基全称规则）闭合这种开放性时会发生什么：若全称语句的每个数值实例都被证明已判定，则该全称语句被证明已判定。所得系统OGA在其他方面与RGA具有完全相同的语法和规则，且所有结论都作为机器可验证定理被开发。已判定性证明变得丰富——关于可计算函数的每个全体性问题都被证明有一个答案，无论是否有人能给出它——这正是两个系统之间可证明的分离。OGA对于自身语义是完备的；已证明但未解决的语句会被赋予由系统自身未决问题构建的值。可证明性仍为递归可枚举，带有原始递归的证明检查器，而ω-真理则被刻意不如此。在这种不对称性中，不完备性呈现出新形式。哥德尔语句被无条件归类为真正的虚构：既不可证明也不可反驳，但具有价值，且带有可计算谱系，记录了将其作为公理采纳所承诺的内容。这种采纳本身就是一组定理：通过任何有限数量的真虚构扩展OGA是一致的，且独立验证的采纳永远不会冲突。
英文摘要
Grounded arithmetic is a family of formal systems for reasoning about computation in which a statement may be asserted only when a terminating computation backs it; the logics are paracomplete - for a sentence whose backing computation never settles, neither the sentence nor its negation is derivable, so paradoxes like the Liar are harmless rather than explosive. The reflective member of the family, RGA, can quantify over its own computations, but cannot certify that its own unbounded searches have definite yes-or-no answers. This paper studies what happens when that openness is closed by exactly one rule - ATI, the $ω$-grounded universal: if every numeric instance of a universal sentence is certified decided, the universal is certified decided. The resulting system, OGA, shares RGA's syntax and rules symbol-for-symbol otherwise, and every consequence is developed as a machine-checked theorem. Decidedness certificates become abundant - every totality question about a computable function is certified to have an answer, whether or not anyone can produce it - and this is exactly the provable separation between the two systems. OGA is complete for its own semantics; certified-but-unresolved sentences receive values built from the system's own open questions. Provability remains recursively enumerable, with a primitive-recursive certificate checker, while $ω$-truth deliberately is not. Within that asymmetry, incompleteness takes a new form. The Gödel sentence is classified, unconditionally, as a genuine fiction: neither provable nor refutable, yet valued, and carrying a computable pedigree recording exactly what adopting it as an axiom commits one to. The adoption is itself a theorem suite: extending OGA by any finite stock of true fictions is consistent, and independently certified adoptions can never collide.
