Definition (Zermelo‒Fraenkel set theory):
Zermelo‒Fraenkel set theory (ZF set theory) is the theory given by the following axioms (where most are written in the language of set theory ):
- Axiom of extensionality:
- Empty set:
- Restricted comprehension schema: Given a set and a formula in the language of set theory . Then we have a set of all such that is true. We write this as the set .
- Replacement schema: Given a set and a formula in the language of set theory , such that for all there exists a unique such that is true. Then there exists a set whose elements are all those . We write this as the set .
- Power set:
- Infinity: There exists an inductive set. An inductive set is one that contains an empty set, and if it contains , then it contains .
Note that in the Infinity axiom, we said that the inductive set contains `an' empty set. We will soon see that there is in fact a unique empty set, so we can change our definition of an inductive set to one that contains `the' empty set.