[FOM] incompleteness theorems formally verified
Jeremy Avigad
avigad at cmu.edu
Wed Jun 12 12:37:10 EDT 2013
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>
More information about the FOM
mailing list