Show simple item record

dc.contributor.authorPaulson, Lawrenceen
dc.date.accessioned2015-03-16T11:29:41Z
dc.date.available2015-03-16T11:29:41Z
dc.date.issued2015-05-02en
dc.identifier.citationJournal of Automated Reasoning June 2015, Volume 55, Issue 1, pp 1-37. DOI: 10.1007/s10817-015-9322-8en
dc.identifier.issn0168-7433
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/247014
dc.description.abstractAn Isabelle/HOL formalisation of Gödel’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.
dc.description.sponsorshipJesse Alama drew my attention to Swierczkowski, the source material for this ´ project. Christian Urban assisted with nominal aspects of some of the proofs, even writing code. Brian Huffman provided the core formalisation of type hf. Dana Scott offered advice and drew my attention to Kirby. Matt Kaufmann and the referees made many insightful comments.
dc.languageEnglishen
dc.language.isoenen
dc.publisherSpringer
dc.titleA Mechanised Proof of Gödel’s Incompleteness Theorems using Nominal Isabelleen
dc.typeArticle
dc.description.versionThis is the author accepted manuscript. The final version is available from Springer at http://link.springer.com/article/10.1007%2Fs10817-015-9322-8en
prism.endingPage37
prism.publicationDate2015en
prism.publicationNameJournal of Automated Reasoningen
prism.startingPage1
prism.volume55en
rioxxterms.versionofrecord10.1007/s10817-015-9322-8en
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserveden
rioxxterms.licenseref.startdate2015-05-02en
dc.contributor.orcidPaulson, Lawrence [0000-0003-0288-4279]
dc.identifier.eissn1573-0670
rioxxterms.typeJournal Article/Reviewen
rioxxterms.freetoread.startdate2016-05-02


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record