Definition
Zermelo–Fraenkel Set Theory
Zermelo–Fraenkel set theory (ZF) is a first-order axiomatic theory whose objects are sets and whose only non-logical symbol is membership,
. The statement means that the set is an element of the set . Its axioms are extensionality, empty set, pairing, union, power set, infinity and foundation, together with the axiom schemas of separation and replacement. An axiom schema supplies an axiom for each formula of the appropriate form. These axioms specify when sets are equal, which sets exist and how further sets may be constructed.
ZF does not include the axiom of choice (AC). The theory obtained by adding it is