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$. Gödel's incompleteness theorems hold for RGA, but their proofs must be adapted. In RGA an implication $A \rightarrow B$ is strictly stronger than an entailment $A \vdash B$: RGA discharges a hypothesis only when it can prove the hypothesis decided, a restriction needed to defuse Curry's paradox. RGA's implication is material and RGA has the disjunction property, so RGA proves no implication between ungrounded sentences. The implications that the textbook proof of Gödel's second theorem uses are of this kind and fail, but the entailments and rules it uses hold: Gödel's proof survives as entailments. RGA does not prove its consistency sentence $\mathit{Con}$: RGA carries out Gödel's argument internally, with a decided proof predicate and explicit proof transformers, and only the last step, that RGA does not prove $0 = 1$, is left to HOL. RGA also proves its own second incompleteness theorem as an entailment from $\mathit{Con}$, and as a single sentence quantified over proofs.

翻译：暂无翻译