A Mechanised Proof of Gödel’s Incompleteness Theorems Using Nominal Isabelle
Type
Article
Change log
Authors
Paulson, LC
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.
Description
Keywords
Godel's incompleteness theorems, Isabelle/HOL, Nominal syntax, Formalisation of mathematics
Journal Title
Journal of Automated Reasoning
Conference Name
Journal ISSN
0168-7433
1573-0670
1573-0670
Volume Title
55
Publisher
Springer Science and Business Media LLC
Publisher DOI
Sponsorship
Jesse 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.