"The full development is concise, at under 17,000 lines, plus a further 3000 lines to develop HF set theory."
JM ---------- Forwarded message ---------- Date: Wed, 12 Jun 2013 12:37:10 -0400 From: Jeremy Avigad <[email protected]> Subject: incompleteness theorems formally verified 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. _______________________________________________ Logica-l mailing list [email protected] http://www.dimap.ufrn.br/cgi-bin/mailman/listinfo/logica-l
