Hereditarily finite set

A recursive definition of well-founded hereditarily finite sets is as follows: Only sets that can be built by a finite number of applications of these two rules are hereditarily finite.

For example, the first cannot be hereditarily finite since it contains at least one infinite set as an element, when

The class of all hereditarily finite sets is denoted by

, meaning that the cardinality of each member is smaller than

(Analogously, the class of hereditarily countable sets is denoted by

th stage of the von Neumann universe.

In 1937, Wilhelm Ackermann introduced an encoding of hereditarily finite sets as natural numbers.

that maps each hereditarily finite set to a natural number, given by the following recursive definition: For example, the empty set

contains no members, and is therefore mapped to an empty sum, that is, the number zero.

On the other hand, a set with distinct members

The Ackermann coding can be used to construct a model of finitary set theory in the natural numbers.

, swapping its two arguments) models Zermelo–Fraenkel set theory ZF without the axiom of infinity.

Here, each natural number models a set, and the

can be seen to be in exact correspondence with a class of rooted trees, namely those without non-trivial symmetries (i.e. the only automorphism is the identity): The root vertex corresponds to the top level bracket

and each edge leads to an element (another such set) that can act as a root vertex in its own right.

No automorphism of this graph exist, corresponding to the fact that equal branches are identified (e.g.

, trivializing the permutation of the two subgraphs of shape

This graph model enables an implementation of ZF without infinity as data types and thus an interpretation of set theory in expressive type theories.

Such models have more intricate edge structure.

also represents the first von Neumann ordinal number, denoted

All finite von Neumann ordinals are indeed hereditarily finite and, thus, so is the class of sets representing the natural numbers.

includes each element in the standard model of natural numbers and so a set theory expressing

Now note that Robinson arithmetic can already be interpreted in ST, the very small sub-theory of Zermelo set theory Z− with its axioms given by Extensionality, Empty Set and Adjunction.

has a constructive axiomatization involving these axioms and e.g. Set induction and Replacement.

Axiomatically characterizing the theory of hereditarily finite sets, the negation of the axiom of infinity may be added.

, this establishes that the axiom of infinity is not a consequence of these other

The hereditarily finite sets are a subclass of the Von Neumann universe.

Here, the class of all well-founded hereditarily finite sets is denoted

This formulation shows, again, that there are only countably many hereditarily finite sets:

in Knuth's up-arrow notation (a tower of