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

[Steven Ericsson-Zenith]

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

Steven


---------- 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
Theorems
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:

http://link.springer.com/article/10.1007/s10817-015-9322-8

Paywalled, but full texts available here:
http://www.cl.cam.ac.uk/~lp15/papers/Formath/

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