[FOM] Gödel’s 2nd Incompleteness Theorem mechanically "proven"

Steven Ericsson-Zenith steven at iase.us
Sun Apr 5 14:41:10 EDT 2015

Larry Paulson has just announced a mechanized proof of Gödel’s second
incompleteness theorem.


---------- Forwarded message ----------
From: Larry Paulson <lp15 at cam.ac.uk>
Date: Sun, Apr 5, 2015 at 4:19 AM
Subject: [isabelle] finally published online: Gödel’s Incompleteness
To: Isabelle Users <cl-isabelle-users at lists.cam.ac.uk>

A Mechanised Proof of Gödel’s Incompleteness Theorems Using Nominal Isabelle

“… The Isabelle formalisation uses two separate treatments of variable
binding: the nominal package… and de Bruijn indices … . Critical details of
the Isabelle proof are described, in particular gaps and errors found in
the literature."

Now available online at SpringerLink:


Paywalled, but full texts available here:

Larry Paulson
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150405/56a6ada4/attachment.html>

More information about the FOM mailing list