Repository logo
 

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

Accepted version
Peer-reviewed

Repository DOI


Loading...
Thumbnail Image

Change log

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.

Description

Journal Title

Review of Symbolic Logic

Conference Name

Journal ISSN

1755-0203
1755-0211

Volume Title

7

Publisher

Cambridge University Press (CUP)

Rights and licensing

Except where otherwised noted, this item's license is described as http://www.rioxx.net/licenses/all-rights-reserved
Sponsorship
Engineering and Physical Sciences Research Council (EP/I011005/1)