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

Title:	From Abstract to Concrete Gödel's Incompleteness Theorems—Part II
Authors:	Andrei Popescu (a /dot/ popescu /at/ mdx /dot/ ac /dot/ uk) and Dmitriy Traytel
Submission date:	2020-09-16
Abstract:	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.
BibTeX:	@article{Goedel_HFSet_Semanticless-AFP, author = {Andrei Popescu and Dmitriy Traytel}, title = {From Abstract to Concrete Gödel's Incompleteness Theorems—Part II}, journal = {Archive of Formal Proofs}, month = sep, year = 2020, note = {\url{http://isa-afp.org/entries/Goedel_HFSet_Semanticless.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Goedel_Incompleteness, HereditarilyFinite, Nominal2
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Proof outline
Proof document

Browse theories

Download this entry