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)- 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
- Formalization of the resolution calculus for first-order logic
- Generic Authenticated Data Structures, Formally.
- 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
- Formalized proof systems for propositional logic
- 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
- Formalisation vs. understanding. A case study in Isabelle
- A machine-assisted proof of Gödel's incompleteness theorems for the theory of hereditarily finite sets
- Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version
- Hereditarily finite sets in constructive type theory
- 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
- A formalisation of finite automata using hereditarily finite sets
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)
