A MACHINE-ASSISTED PROOF OF GÖDEL'S INCOMPLETENESS THEOREMS FOR THE THEORY OF HEREDITARILY FINITE SETS. Issue 3 (3rd April 2014)

• Record Type: Journal Article
• Authors: PAULSON, LAWRENCE C.
• Is Part Of: Review of symbolic logic. Volume 7:Issue 3(2014)
• Page Start: 484
• Page End: 498
• Publication Date: 2014-04-03
• Subjects: Logic, Symbolic and mathematical -- Periodicals; 511.3
• DOI: 10.1017/S1755020314000112
• Languages: English
• ISSNs: 1755-0203

Abstract

<abstract abstract-type="normal"> <title>Abstract</title> <p>A formalization of Gödel'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 Świerczkowski (<xref ref-type="bibr" rid="ref14">2003</xref>), 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 formalization itself should be useful to logicians, particularly concerning the second incompleteness theorem, where existing proofs are lacking in detail.</p> </abstract>