A formally verified abstract account of Gödel's incompleteness theorems

We present an abstract development of Gödel’s incompleteness theorems, performed with the help of the Isabelle/HOL theorem prover. We analyze sufficient conditions for the theorems’ applicability 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 S ́wierczkowski–Paulson semantics-based approach. As part of our framework’s validation, we upgrade Paulson’s Isabelle proof to produce a mech- anization 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.

This is the Author’s accepted version of a paper published in Automated Deduction – CADE 27. CADE 2019. Lecture Notes in Computer Science, vol 11716 . The final authenticated version is available online at https://doi.org/10.1007/978-3-030-29436-6_26

Popescu A., Traytel D. (2019) A Formally Verified Abstract Account of Gödel’s Incompleteness Theorems. In: Fontaine P. (eds) Automated Deduction – CADE 27. CADE 2019. Lecture Notes in Computer Science, vol 11716. Springer, Cham