Logblog: Richard Zach's Logic Blog
Going through old emails, I found the following announcement by Larry Paulson, posted to the FOM list by Jeremy Avigad. Good stuff, including the link to Stanis?aw ?wierczkowski's monograph in Dissertationes Mathematicae where he carries out the proof of the incompleteness theorems in HF, the theory of hereditarily finite sets. This should be of independent interest even if you don't care about proof formalization -- I hear of it, I think, but haven't read it. You can buy it here.
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. ?wierczkowski, who presents proofs of both incompleteness theorems using the hereditarily finite sets rather than Peano Arithmetic:
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 => Prov["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.