A Mechanised Proof of Gödel's Incompleteness Theorems using Nominal Isabelle
arXiv:2104.13792 · doi:10.1007/s10817-015-9322-8
Abstract
An Isabelle/HOL formalisation of Gödel's two incompleteness theorems is presented. The work follows Świerczkowski's detailed proof of the theorems using hereditarily finite (HF) set theory. Avoiding the usual arithmetical encodings of syntax eliminates the necessity to formalise elementary number theory within an embedded logical calculus. The Isabelle formalisation uses two separate treatments of variable binding: the nominal package is shown to scale to a development of this complexity, while de Bruijn indices turn out to be ideal for coding syntax. Critical details of the Isabelle proof are described, in particular gaps and errors found in the literature.
References in corpus (4)
- General Bindings and Alpha-Equivalence in Nominal Isabelle
- The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle/ZF
- A Machine-Assisted Proof of Gödel's Incompleteness Theorems for the Theory of Hereditarily Finite Sets
- Petri Net Reachability Graphs: Decidability Status of First Order Properties
Cited by in corpus (7)
- A Machine-Assisted Proof of Gödel's Incompleteness Theorems for the Theory of Hereditarily Finite Sets
- Undecidable problems in quantum field theory
- On First-Order Model-Based Reasoning
- A Formalisation of Finite Automata using Hereditarily Finite Sets
- Towards Evolutionary Theorem Proving for Isabelle/HOL
- PaMpeR: Proof Method Recommendation System for Isabelle/HOL
- Towards Concise, Machine-discovered Proofs of Gödel's Two Incompleteness Theorems