From Abstract to Concrete Gödel's Incompleteness Theorems—Part II

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 validate an abstract formulation of Gödel's Second Incompleteness Theorem from a separate AFP entry by instantiating it to the case of finite consistent extensions of the Hereditarily Finite (HF) Set theory, i.e., consistent FOL theories extending the HF Set theory with a finite set of axioms. The instantiation draws heavily on infrastructure previously developed by Larry Paulson in his direct formalisation of the concrete result. It strengthens Paulson's formalization of Gödel's Second from that entry by not assuming soundness, and in fact not relying on any notion of model or semantic interpretation. The strengthening was obtained by first replacing some of Paulson’s semantic arguments with proofs within his HF calculus, and then plugging in some of Paulson's (modified) lemmas to instantiate our soundness-free Gödel's Second locale.


BSD License


Session Goedel_HFSet_Semanticless