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

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 First and Second Incompleteness Theorems from a separate AFP entry by instantiating them to the case of finite sound extensions of the Hereditarily Finite (HF) Set theory, i.e., FOL theories extending the HF Set theory with a finite set of axioms that are sound in the standard model. The concrete results had been previously formalised in an AFP entry by Larry Paulson; our instantiation reuses the infrastructure developed in that entry.


BSD License


Session Goedel_HFSet_Semantic