A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS

DOI10.1017/S1755020314000112zbMATH Open1337.03021DBLPjournals/rsl/Paulson14arXiv2104.14260WikidataQ57382547 ScholiaQ57382547MaRDI QIDQ2940885FDOQ2940885

Lawrence C. Paulson

Publication date: 21 January 2015

Published in: The Review of Symbolic Logic (Search for Journal in Brave)

Abstract: A formalisation of G"odel's incompleteness theorems using the Isabelle proof assistant is described. This is apparently the first mechanical verification of the second incompleteness theorem. The work closely follows {'S}wierczkowski (2003), who gave a detailed proof using hereditarily finite set theory. The adoption of this theory is generally beneficial, but it poses certain technical issues that do not arise for Peano arithmetic. The formalisation itself should be useful to logicians, particularly concerning the second incompleteness theorem, where existing proofs are lacking in detail.

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

zbMATH Keywords

mechanical verificationsecond incompleteness theorem

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Gödel numberings and issues of incompleteness (03F40)

Cites Work

• Addition and multiplication of sets
• Finite sets and Gödel's incompleteness theorems
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (11)

• Formalization of the resolution calculus for first-order logic
• NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF
• 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
• Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’
• Distilling the requirements of Gödel's incompleteness theorems with a proof assistant
• The scope of Gödel's first incompleteness theorem
• A formally verified abstract account of Gödel's incompleteness theorems
• A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
• Computational logic: its origins and applications
• Formalizing Bachmair and Ganzinger's ordered resolution prover

Uses Software

• Isabelle/HOL

This page was built for publication: A MACHINE-ASSISTED PROOF OF GÖDEL’S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2940885)