|
The
Hereditarily
Finite
Sets
Title: |
The Hereditarily Finite Sets |
Author:
|
Lawrence C. Paulson
|
Submission date: |
2013-11-17 |
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. |
Change history: |
[2015-02-23]: Added the theory "Finitary" defining the class of types that can be embedded in hf, including int, char, option, list, etc. |
BibTeX: |
@article{HereditarilyFinite-AFP,
author = {Lawrence C. Paulson},
title = {The Hereditarily Finite Sets},
journal = {Archive of Formal Proofs},
month = nov,
year = 2013,
note = {\url{http://isa-afp.org/entries/HereditarilyFinite.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Used by: |
Finite_Automata_HF, Incompleteness |
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.
|
|