A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle

DOI10.1007/s10817-015-9322-8zbMath1357.68200arXiv2104.13792OpenAlexW2015224901WikidataQ56853390 ScholiaQ56853390MaRDI QIDQ286772

Lawrence Charles Paulson

Publication date: 26 May 2016

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2104.13792

zbMATH Keywords

formalisation of mathematicsGödel's incompleteness theoremsIsabelle/HOLnominal syntax

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) First-order arithmetic and fragments (03F30) Gödel numberings and issues of incompleteness (03F40)

Related Items

A Formalisation of Finite Automata Using Hereditarily Finite Sets ⋮ Formalization of the resolution calculus for first-order logic ⋮ Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started ⋮ Undecidable problems in quantum field theory ⋮ A Formal Proof of the Computation of Hermite Normal Form in a General Setting ⋮ A step towards absolute versions of metamathematical results ⋮ Synthetic undecidability and incompleteness of first-order axiom systems in Coq. Extended version ⋮ Unnamed Item ⋮ Programming and verifying a declarative first-order prover in Isabelle/HOL ⋮ Generic Authenticated Data Structures, Formally. ⋮ 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 ⋮ Hereditarily Finite Sets in Constructive Type Theory

Uses Software

• Coq
• Isabelle/HOL
• Isabelle/ZF
• Nominal Isabelle
• FinFuns
• Incompleteness Theorems
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A new approach to abstract syntax with variable binding
• Nominal techniques in Isabelle/HOL
• Set theory. An introduction to independence proofs
• Advanced logic for applications
• Set theory for verification. I: From foundations to functions
• More Church-Rosser proofs (in Isabelle/HOL)
• Isabelle/HOL. A proof assistant for higher-order logic
• Theorem proving in higher order logics. 18th international conference, TPHOLs 2005, Oxford, UK, August 22--25, 2005. Proceedings.
• Nominal Sets
• A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS
• Formalising FinFuns – Generating Code for Functions as Data from Isabelle/HOL
• 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
• General Bindings and Alpha-Equivalence in Nominal Isabelle