Auto formalisation of Goedel's Second Incompleteness Theorem in Binary Recursive Arithmetic

Technical Summary: Auto Formalisation of Gödel's Second Incompleteness Theorem in Binary Recursive Arithmetic

Problem Statement
The paper reports an experiment in the autoformalisation of Gödel's Second Incompleteness Theorem (Gödel II) for Church's Basic Recursive Arithmetic (BRA) using the proof assistant Agda and the large language model (LLM) Claude. The primary challenge addressed is the formalisation of a text (R. Guard's 1963 lecture notes) that, while precise, contains typographical errors, gaps, and implicit mathematical arguments that require substantial reconstruction. A secondary problem involves evaluating the capabilities and limitations of current LLMs in generating correct mathematical formalisations from such texts, particularly when the initial specifications are ambiguous or incorrect.

Methodology
The project employed a "zero-code" approach where the author did not write any Agda code; the entire development (approximately 50,000 lines) was generated through interaction with Claude. The formalisation was conducted from scratch without external libraries or tactics, adhering strictly to the --safe --without-K --exact-split options to ensure no postulates were used.

The methodology involved two distinct phases:

1. Initial Autonomous Attempt: An attempt was made using a paper by Rose. This failed because the underlying theorem in Rose's paper was false. The LLM successfully formalised a statement that superficially resembled Gödel's theorem but was mathematically unrelated, highlighting the model's ability to reason correctly from incorrect specifications.
2. Corrected Formalisation: The project shifted to Guard's 1963 notes. The formalisation required reconstructing implicit arguments, specifically regarding the internal numeral-encoding operation (num) and the interaction between substitution and numeral closure.
   • Logical Framework: The system uses a Hilbert-style calculus with axioms for equality, propositional logic, and primitive recursion (Church's combinators o, u, v, C, R).
   • Internalisation: A critical technical hurdle was the lack of a Deduction Theorem in the object language. The author provided Claude with Mario Carneiro's technique of "lifting" derivations (proving P ⊃ A instead of A under hypothesis P) to handle hypothetical reasoning within the Hilbert system.
   • Recursion: The verifier thmT (which enumerates derived formulae) was defined using course-of-values recursion. Since Church's recursor R does not directly support standard course-of-values recursion, a "nested-R trick" was employed to synthesize an iteration combinator, with its correctness proved via internal induction.
   • Substitution: The formalisation replaced complex multi-variable simultaneous substitution machinery with nested single-variable substitution, relying on a "numeral-inertness" lemma (proving that num(x) is closed under substitution) to handle re-scanning of substituted terms.

Key Contributions and Results

1. Machine-Checked Proof: The project produced a complete, machine-checked proof of Gödel's Second Incompleteness Theorem for BRA. The development contains approximately 50,000 lines of Agda code with zero postulates.
2. Clarification of Guard's Notes: The formalisation explicitly resolved several ambiguities in Guard's text:
   • The num vs. code distinction: Clarified the difference between the internal term num(x) (computing the encoding of a value) and the meta-level code(x) (the Gödel handle).
   • Diagonal Lemma: Distinguished between two forms of the Gödel sentence (G_sub and G_sbf) and bridged the gap using predicate-Leibniz substitutivity.
   • Validation Invariant: Defined a canonical behavior for the verifier thmT on invalid inputs (returning the code of 0=0) to ensure closure equations hold universally.
   • Carneiro Lift: Systematically applied the lifting technique to manage hypothetical derivations in a context-free Hilbert system.
3. Architectural Simplification: The project demonstrated that nested single-variable substitution, combined with the numeral-inertness lemma, is sufficient to replace dedicated multi-variable substitution machinery, reducing the codebase by roughly 10,000 lines.
4. LLM Case Study: The project serves as a case study for LLMs in mathematics. It demonstrated that while LLMs can generate complex formal proofs, they may fail to detect when a formal specification is mathematically insufficient (as seen in the Rose attempt) or when a proof relies on implicit meta-theoretic properties not captured in the object specification.

Significance and Claims
The paper claims that this experiment suggests the use of LLMs may substantially change the activity of formalisation. It highlights that type theory is well-suited for representing combinatorial facts about syntax, allowing for the verification of statement correctness. However, it also notes the limitations: the LLM can produce a "correct" proof of a "wrong" theorem if the specification is flawed, lacking a global picture of the mathematical intent.

The work provides a fully verified, constructive version of Gödel's Second Incompleteness Theorem for BRA, filling a gap in the literature where only a version for hereditary finite sets (by Paulson) was previously known. It documents the reconstruction of implicit mathematical arguments required to bridge the gap between informal lecture notes and a rigorous machine-checked proof, offering a blueprint for future autoformalisation efforts involving texts with gaps or ambiguities. The author explicitly notes that the mathematical content and final text were reviewed by the human author, while the code generation and specific sections (5–11) were generated by Claude.