Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant
Research output: Contribution to journal › Journal article › Research › peer-review
Documents
- Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant
Final published version, 674 KB, PDF document
We present an abstract development of Gödel’s incompleteness theorems, performed with the help of the Isabelle/HOL proof assistant. We analyze sufficient conditions for the applicability of our theorems to a partially specified logic. In addition to the usual benefits of generality, our abstract perspective enables a comparison between alternative approaches from the literature. These include Rosser’s variation of the first theorem, Jeroslow’s variation of the second theorem, and the Świerczkowski–Paulson semantics-based approach. As part of the validation of our framework, we upgrade Paulson’s Isabelle proof to produce a mechanization of the second theorem that does not assume soundness in the standard model, and in fact does not rely on any notion of model or semantic interpretation.
Original language | English |
---|---|
Journal | Journal of Automated Reasoning |
Volume | 65 |
Pages (from-to) | 1027–1070 |
ISSN | 0168-7433 |
DOIs | |
Publication status | Published - 2021 |
Number of downloads are based on statistics from Google Scholar and www.ku.dk
No data available
ID: 278041128