反思基础算术中的内在真
Internalized Truth in Reflective Grounded Arithmetic
浏览论文内容
中文总结 AI 辅助
本文在Isabelle/HOL中开发了经机器验证的RGA系统，定义了其内在真谓词，完成相关元定理闭合，证明RGA是支持非平凡数学推理的可行形式系统。
中文摘要 AI 辅助
根据塔斯基不可定义性定理，任何包含算术的一致经典形式系统都无法定义自身的真谓词。反思基础算术（Reflective Grounded Arithmetic，RGA）是一种强大的算术，其全称量词以自身的反思证明搜索为基础，且其超完备性规避了塔斯基定理。本文提出了一个经机器验证的Isabelle/HOL开发，该开发为RGA的完整语言（包括量词）定义了一个RGA自身的内在项形式的真谓词。该谓词从其操作语义的原始递归判定器编译而来，并被证明在两个方向上都是充分的。围绕该谓词，该开发完成了一组元定理的闭合：对于RGA证明的每个公式，RGA都能推导出该公式的内在真；每个基础为真的公式都是内在可证的；内在真蕴含内在可证性；且RGA的一致性可由此得出。这两个方向运行在不相交的内在机器上——一个是经认证的判定器，另一个是经认证的证明检查器，二者均为RGA项。获得这些结果需要在RGA内进行大量常规推理：编码的语法与替换、带有符号展开律的编译后原始递归函数、内在强归纳，以及用系统自身形式语言编写的经验证的系统证明检查器。该开发由此沿途证明，RGA是一种支持非平凡数学推理的可行形式系统。
英文摘要
By Tarski's undefinability theorem, no consistent classical formal system that includes arithmetic can define its own truth predicate. Reflective Grounded Arithmetic (RGA) is a powerful arithmetic whose universal quantifier is grounded in its own reflected proof search, and whose paracompleteness circumvents Tarski's theorem. This paper presents a machine-checked Isabelle/HOL development that defines a truth predicate for RGA's full language, quantifiers included, as an internal term of RGA itself. This term is compiled from a primitive-recursive decider for its operational semantics, and proven adequate in both directions. Around this predicate the development closes a square of metatheorems: for every formula RGA proves, RGA derives the formula's internal truth; every grounded-true formula is internally provable; internal truth implies internal provability; and the consistency of RGA follows. The two directions run on disjoint internal machines---a certified decider and a certified proof-checker, both RGA terms. Reaching these results involved substantial ordinary reasoning carried out within RGA: coded syntax and substitution, compiled primitive-recursive functions with symbolic unfolding laws, internal strong induction, and a verified proof-checker for the system written in the system's own formal language. The development thus demonstrates along the way that RGA is a workable formal system supporting nontrivial mathematical reasoning.
