### 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.

### License

BSD License

### Topics

- Logic/Proof theory

### Session Goedel_HFSet_Semanticless

- SyntaxN
- Coding
- Predicates
- Sigma
- Coding_Predicates
- Pf_Predicates
- II_Prelims
- Pseudo_Coding
- Quote
- Functions
- Goedel_I
- Instance

### Depends on

- An Abstract Formalization of Gödel’s Incompleteness Theorems
- The Hereditarily Finite Sets
- Nominal 2

### Auto-related entries

- From Abstract to Concrete Gödel’s Incompleteness Theorems—Part I
- CoSMeDis: A confidentiality-verified distributed social media platform
- A General Theory of Syntax with Bindings
- Cardinality of Equivalence Relations

## Cite

×

Goedel_HFSet_Semanticless-AFP

    @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   = {September},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Goedel_HFSet_Semanticless.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Sep 18, 2020 : Isabelle2020