Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant
Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt
Dokumenter
- Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant
Forlagets udgivne version, 674 KB, PDF-dokument
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.
Originalsprog | Engelsk |
---|---|
Tidsskrift | Journal of Automated Reasoning |
Vol/bind | 65 |
Sider (fra-til) | 1027–1070 |
ISSN | 0168-7433 |
DOI | |
Status | Udgivet - 2021 |
Antal downloads er baseret på statistik fra Google Scholar og www.ku.dk
Ingen data tilgængelig
ID: 278041128