A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
From MaRDI portal
Publication:286772
DOI10.1007/S10817-015-9322-8zbMATH Open1357.68200DBLPjournals/jar/Paulson15arXiv2104.13792OpenAlexW2015224901WikidataQ56853390 ScholiaQ56853390MaRDI QIDQ286772FDOQ286772
Authors: Lawrence C. Paulson 
Publication date: 26 May 2016
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Abstract: An Isabelle/HOL formalisation of G"odel's two incompleteness theorems is presented. The work follows 'Swierczkowski'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.
Full work available at URL: https://arxiv.org/abs/2104.13792
Recommendations
Mechanization of proofs and logical operations (03B35) First-order arithmetic and fragments (03F30) Gödel numberings and issues of incompleteness (03F40)
Cites Work
- Nominal techniques in Isabelle/HOL
- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
- Set theory. An introduction to independence proofs
- Isabelle/HOL. A proof assistant for higher-order logic
- Nominal sets. Names and symmetry in computer science
- A new approach to abstract syntax with variable binding
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Advanced logic for applications
- Set theory for verification. I: From foundations to functions
- More Church-Rosser proofs (in Isabelle/HOL)
- Theorem proving in higher order logics. 18th international conference, TPHOLs 2005, Oxford, UK, August 22--25, 2005. Proceedings.
- A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS
- Title not available (Why is that?)
- Addition and multiplication of sets
- Proof Pearl: De Bruijn Terms Really Do Work
- Towards Self-verification of HOL Light
- Metamathematics, Machines and Gödel's Proof
- The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
- Finite sets and Gödel's incompleteness theorems
- Theorem Proving in Higher Order Logics
- Theorem Proving in Higher Order Logics
- Title not available (Why is that?)
- General bindings and alpha-equivalence in Nominal Isabelle
Cited In (19)
- Hereditarily Finite Sets in Constructive Type Theory
- Theory of symbolic expressions. II
- A step towards absolute versions of metamathematical results
- Automated proofs of Löb's theorem and Gödel's two incompleteness theorems
- Generic Authenticated Data Structures, Formally.
- Formalization of the resolution calculus for first-order logic
- A Formalisation of Finite Automata Using Hereditarily Finite Sets
- Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started
- Theorem Proving in Higher Order Logics
- Undecidable problems in quantum field theory
- Automated search for Gödel's proofs
- The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
- A formally verified abstract account of Gödel's incompleteness theorems
- Formalization of the Resolution Calculus for First-Order Logic
- Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version
- Programming and verifying a declarative first-order prover in Isabelle/HOL
- A Formal Proof of the Computation of Hermite Normal Form in a General Setting
- Title not available (Why is that?)
Uses Software
This page was built for publication: A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q286772)
