### Abstract

Gödel's two incompleteness theorems are formalised, following a careful presentation by Swierczkowski, in the theory of hereditarily finite sets. This represents the first ever machine-assisted proof of the second incompleteness theorem. Compared with traditional formalisations using Peano arithmetic (see e.g. Boolos), coding is simpler, with no need to formalise the notion of multiplication (let alone that of a prime number) in the formalised calculus upon which the theorem is based. However, other technical problems had to be solved in order to complete the argument.

### License

BSD License

### Topics

- Logic/Proof theory

### Session Incompleteness

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

### Depends on

- The Hereditarily Finite Sets
- Nominal 2

### Used by

- From Abstract to Concrete Gödel’s Incompleteness Theorems—Part I
- Surprise Paradox

### Auto-related entries

- MLSS Decision Procedure
- Recursion Theorem in ZF
- Probabilistic Primality Testing
- Bertrand’s postulate
- Category Theory with Adjunctions and Limits

## Cite

×

Incompleteness-AFP

    @article{Incompleteness-AFP,
      author  = {Lawrence C. Paulson},
      title   = {Gödel's Incompleteness Theorems},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2013},
      note    = {\url{https://isa-afp.org/entries/Incompleteness.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
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Dec 2, 2013 : Isabelle2013-1
- Nov 17, 2013 : Isabelle2013-1