Gödel's Incompleteness Theorems

Title:	Gödel's Incompleteness Theorems
Author:	Lawrence C. Paulson
Submission date:	2013-11-17
Abstract:	Gödel's two incompleteness theorems are formalised, following a careful presentation by Swierczkowski, in the theory of hereditarily finite sets. This represents the first ever machine-assisted proof of the second incompleteness theorem. Compared with traditional formalisations using Peano arithmetic (see e.g. Boolos), coding is simpler, with no need to formalise the notion of multiplication (let alone that of a prime number) in the formalised calculus upon which the theorem is based. However, other technical problems had to be solved in order to complete the argument.
BibTeX:	@article{Incompleteness-AFP, author = {Lawrence C. Paulson}, title = {Gödel's Incompleteness Theorems}, journal = {Archive of Formal Proofs}, month = nov, year = 2013, note = {\url{http://isa-afp.org/entries/Incompleteness.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	HereditarilyFinite, Nominal2
Used by:	Goedel_HFSet_Semantic, Surprise_Paradox
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.