arXiv:2608.16140 · v3

Internal Reasoning and Consistency in Reflective Grounded Arithmetic

首次提交 2026-08-17 13:48

版本更新 2026-11-11 16:15

雷达观测 2026-11-13 11:11

摘要

Reflective Grounded Arithmetic (RGA) is a paracomplete arithmetic allowing direct expression of any general-recursive computation. Every RGA term is a program and truth is grounded evaluation, with a proof certificate at each universal quantifier. This paper shows, in a machine-checked Isabelle/HOL development, that such a system is powerful enough to carry out its own metamathematics. A fuel-indexed decider of RGA's grounded semantics and checkers for RGA's proofs are compiled primitive-recursive RGA terms. RGA proves internally that its decider never affirms 0 = 1, and that every well-formed term it affirms has an RGA proof accepted by a transparent test. RGA proves that, for each valid RGA proof, its conclusion is true. RGA proves that each grounded-true well-formed term is provable. RGA proves that no proof in either of two decided classes of RGA proofs derives 0 = 1. RGA's truth predicate also serves as a medium for proof by reflection, of the kind that adds nothing to the system. RGA derives disquotation for quantifier-free formulas as rules in every context, at a free variable, and proves, as one sentence, that whenever its normalizer for polynomials in one variable gives two terms the same normal form, the equation between them is true at every value of the variable. Each such polynomial identity then follows from that sentence by closed evaluation and disquotation, with no reflection rule. A companion paper proves Gödel's incompleteness theorems for RGA and its extensions.

作者备注：substantially revised; Goedel incompleteness theorems split into separate preprint 2611.13697; now 163 pages