### Abstract

The theory of hereditarily finite sets is formalised, following the development of Swierczkowski. An HF set is a finite collection of other HF sets; they enjoy an induction principle and satisfy all the axioms of ZF set theory apart from the axiom of infinity, which is negated. All constructions that are possible in ZF set theory (Cartesian products, disjoint sums, natural numbers, functions) without using infinite sets are possible here. The definition of addition for the HF sets follows Kirby. This development forms the foundation for the Isabelle proof of Gödel's incompleteness theorems, which has been formalised separately.

### License

BSD License

### History

February 23, 2015
  Added the theory "Finitary" defining the class of types that can be embedded in hf, including int, char, option, list, etc.

### Topics

- Logic/Set theory

### Session HereditarilyFinite

- HF
- Ordinal
- Rank
- Finite_Automata
- Finitary
- OrdArith

### Used by

- MLSS Decision Procedure
- From Abstract to Concrete Gödel’s Incompleteness Theorems—Part II
- Category Theory with Adjunctions and Limits
- Finite Automata in Hereditarily Finite Set Theory
- Gödel’s Incompleteness Theorems

## Cite

×

HereditarilyFinite-AFP

    @article{HereditarilyFinite-AFP,
      author  = {Lawrence C. Paulson},
      title   = {The Hereditarily Finite Sets},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2013},
      note    = {\url{https://isa-afp.org/entries/HereditarilyFinite.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
- Nov 17, 2013 : Isabelle2013-1