An Abstract Formalization of Gödel's Incompleteness Theorems

Andrei Popescu 🌐 and Dmitriy Traytel 🌐

September 16, 2020

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


We present an abstract formalization of Gödel's incompleteness theorems. We analyze sufficient conditions for the theorems' applicability to a partially specified logic. 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 Swierczkowski–Paulson semantics-based approach. This AFP entry is the main entry point to the results described in our CADE-27 paper A Formally Verified Abstract Account of Gödel's Incompleteness Theorems. As part of our abstract formalization's validation, we instantiate our locales twice in the separate AFP entries Goedel_HFSet_Semantic and Goedel_HFSet_Semanticless.


BSD License


Session Goedel_Incompleteness