Proving Gödel’s Incompleteness Theorems
Author: Lawrence Paulson
Paper Information
| Title: | Proving Gödel’s Incompleteness Theorems |
| Authors: | Lawrence Paulson |
| Proceedings: | Isabelle 2014 Papers (Unrefereed) |
| Editors: | Tobias Nipkow, Lawrence Paulson and Makarius Wenzel |
| Keywords: | Isabelle, Gödel's incompleteness theorem, nominal |
| Abstract: | ABSTRACT. Gödel’s two incompleteness theorems have been proved in Isabelle. The nominal package was used to handle variable binding in conjunction with de Bruijn indexes. This is the first mechanical proof of the second incompleteness theorem. |
| Pages: | 10 |
| Talk: | Jul 13 14:30 |
| Paper: |  |