[FOM] incompleteness theorems formally verified

[Jeremy Avigad]

Dear friends and colleagues,

Larry Paulson, Professor of Computational Logic at Cambridge University, 
has recently completed a formal verification of Gödel's incompleteness 
theorems, using the popular Isabelle interactive proof system.

Because this should be of interest to the FOM community, I asked him to 
send me an announcement that I could post to this list. That 
announcement appears below.

Paulson was the initial designer of Isabelle, which he continues to 
develop with Tobias Nipkow and Makarius Wenzel. About 10 years ago, he 
also formalized Gödel's constructible hierarchy in Isabelle, to prove 
the relative consistency of the axiom of choice. Related publications 
can be found on his web page,

http://www.cl.cam.ac.uk/~lp15/ <http://www.cl.cam.ac.uk/%7Elp15/>

Best wishes,

Jeremy Avigad

******

Larry's announcement:

I've completed a formalisation of Gödel's two incompleteness theorems, 
including what may be the first-ever formalisation of the second 
incompleteness theorem. The proof was done in Isabelle/HOL and uses 
Christian Urban's Nominal2 package for dealing with bound variables. The 
formalisation follows an unpublished paper by S S'wierczkowski, who 
presents proofs of both incompleteness theorems using the hereditarily 
finite sets rather than Peano Arithmetic:

http://journals.impan.gov.pl/dm/PDF/dm422-0-00.pdf

Proving the second incompleteness theorem requires some quite intricate 
operations on alphabets, as well as lengthy derivations in an internal 
calculus. Apart from those derivations, the proof script is structured 
and quite legible. The full development is concise, at under 17,000 
lines, plus a further 3000 lines to develop HF set theory. (A recent Coq 
proof of the first incompleteness theorem alone is over 52,000 lines.)

The development is instructive. While first-order logic is formalised 
here using "nominal" binding primitives, the coding uses de Bruijn 
indexes. A precise correspondence is proved between the two 
representations of formulas. A series of correspondence proofs provides 
confidence in the correctness of the complicated syntactic definitions. 
The second incompleteness theorem follows from the Hilbert-Bernays 
derivability conditions. Proving the crucial theorem |- A IMP 
Provable["A"] requires transforming a coded formula. During this 
process, the coded variables (which are constant terms) need to be 
replaced by terms consisting of a special function applied to the same 
variable (not coded). But this calculus has no functions, and this step 
needs to be expressed by introducing new variables that satisfy a 
certain relation with the original variables. The proof is by induction 
on the formula A, but relies on properties proved by a mutual induction 
within the encoded first-order calculus itself.





-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20130612/980bb91e/attachment.html>