A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
From MaRDI portal
(Redirected from Publication:286772)
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.
Recommendations
Cites work
- scientific article; zbMATH DE number 3130531 (Why is no real title available?)
- scientific article; zbMATH DE number 5539366 (Why is no real title available?)
- scientific article; zbMATH DE number 1170091 (Why is no real title available?)
- scientific article; zbMATH DE number 2198106 (Why is no real title available?)
- scientific article; zbMATH DE number 3400430 (Why is no real title available?)
- A machine-assisted proof of Gödel's incompleteness theorems for the theory of hereditarily finite sets
- A new approach to abstract syntax with variable binding
- Addition and multiplication of sets
- Advanced logic for applications
- Finite sets and Gödel's incompleteness theorems
- Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
- General bindings and alpha-equivalence in Nominal Isabelle
- Isabelle/HOL. A proof assistant for higher-order logic
- Metamathematics, Machines and Gödel's Proof
- More Church-Rosser proofs (in Isabelle/HOL)
- Nominal sets. Names and symmetry in computer science
- Nominal techniques in Isabelle/HOL
- Proof Pearl: De Bruijn Terms Really Do Work
- Set theory for verification. I: From foundations to functions
- Set theory. An introduction to independence proofs
- The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
- Theorem Proving in Higher Order Logics
- Theorem Proving in Higher Order Logics
- Theorem proving in higher order logics. 18th international conference, TPHOLs 2005, Oxford, UK, August 22--25, 2005. Proceedings.
- Towards Self-verification of HOL Light
Cited in
(21)- A step towards absolute versions of metamathematical results
- Undecidable problems in quantum field theory
- A formalisation of finite automata using hereditarily finite sets
- Formalisation vs. understanding. A case study in Isabelle
- Theory of symbolic expressions. II
- Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version
- Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started
- Programming and verifying a declarative first-order prover in Isabelle/HOL
- Generic Authenticated Data Structures, Formally.
- Theorem Proving in Higher Order Logics
- A machine-assisted proof of Gödel's incompleteness theorems for the theory of hereditarily finite sets
- Formalization of the Resolution Calculus for First-Order Logic
- Automated proofs of Löb's theorem and Gödel's two incompleteness theorems
- Hereditarily finite sets in constructive type theory
- Formalization of the resolution calculus for first-order logic
- Formalized proof systems for propositional logic
- Automated search for Gödel's proofs
- A Formal Proof of the Computation of Hermite Normal Form in a General Setting
- 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
Describes a project that uses
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)
