Zermelo–Fraenkel set theory

Zermelo–Fraenkel set theory is the usual first-order axiomatization of sets by extensionality, empty set, pairing, union, power set, infinity, separation, replacement and foundation.

The usual set theory with extensionality, empty set, pairing, union, power set, infinity and full separation, before adjoining replacement. Modern presentations often include foundation; the convention should be specified when comparing theories. Class-theoretic variants add classes and class comprehension, rather than treating proper classes as sets.

Every proper class is in bijection with the universe. Over class-theoretic Zermelo set theory, with class-parameter separation, this is equivalent to replacement plus global choice. For replacement, a proper functional image of a set would give a surjection from that set onto the universe, contradicted by diagonal separation. The proper class of ordinals supplies the global well-order. Conversely rank followed by uniformly chosen rank-segment well-orders is set-like, and every proper class in that order has order type equal to the entire ordinal class.

Full intuitionistic Zermelo–Fraenkel set theory uses intuitionistic first-order logic, extensionality, pairing, union, infinity, full separation, power set, collection and epsilon induction. Collection is stronger than replacement intuitionistically. This is distinct from predicative constructive ZF, which restricts separation and replaces full power set. The full theory supports a Boolean-valued inner universe over intuitionistic set theory, giving the relative consistency of classical ZF.

Using the double-negation Boolean algebra, form well-founded names whose immediate subnames have truth-value weights. Define valued membership and equality by recursion on the underlying well-founded trees. Logical conjunction and universal quantification use meets; disjunction and existence use Boolean joins. Explicit names for pairs, unions and subsets verify the elementary set axioms, and collection for Boolean-valued names handles unbounded witnesses. The resulting internal valued universe validates classical ZF. This is a negative inner interpretation, not an assertion that the external intuitionistic universe satisfies excluded middle.

A well-founded recursively built set code with a set of immediate subnames and a Boolean coefficient for each. The coefficient records the extent to which the corresponding subname belongs. More generally one may permit repeated coded subnames, joining their coefficients. Recursive valued equality identifies different codes representing the same valued set; external equality of codes is not the interpreted equality.

For a name $a$ and formula $\phi$, form the set of pairs $(u,p)$ with $u$ in the immediate domain of $a$, $p$ a Boolean truth value, and some name $v$ satisfying $p\le a(u)\wedge [[\phi (u,v)]]$. Full separation makes this a set, and intuitionistic collection gives a set of witness names covering all its pairs. A name with these witnesses in its domain collects the entire Boolean value of every existential assertion over $a$, without selecting one witness whose value is top. No choice or maximum principle is used.

A definable class bijection $\pi$ of a model's universe changes membership as displayed. Images and inverse images of sets under $\pi$ remain sets by the Axiom schema of replacement. The new extension of $y$ is the old set $\pi (y)$. Thus the representative of any desired extension $b$ is ${\pi }^{-1}(b)$. Extensionality follows from bijectivity; separation and replacement translate to old definable formulas; pairs, unions and power sets have explicit representatives. Infinity follows by iterating the new empty set and successor. Foundation need not survive: interchanging $\varnothing$ and $\{\varnothing \}$ makes the old empty set a Quine atom. A full such permutation of a model of choice still satisfies choice; failure of choice requires an additional symmetry restriction.

A Quine atom is a set whose sole member is itself. It violates the Axiom of foundation while respecting the axiom of extensionality. Swapping pairwise distinct old objects $a_n$ with their singletons in a Rieger-Bernays permutation model supplies many Quine atoms, provided those transpositions have disjoint supports. For example, the old ordinals $a_n=\omega +n$ and their singletons are disjoint families.

Start with distinct formal atoms $q\in A$ with membership extensions $\{q\}$. Recursively adjoin a unique representative $S(X)$ of every subset $X$ of a previous stage, except that $S(\{q\})=q$ uses the atom already present. Define membership by these extensions. Each set-sized collection of objects has bounded construction rank, so it has a representative at a later stage. This gives full extensionality, unlike adjoining an ordinary singleton distinct from a Quine atom. Definable subsets and ranges, unions and power sets are set-sized collections in the ambient model and hence have representatives. The pure finite hierarchy supplies infinity. Every permutation of the atoms extends recursively; hereditary finite support restriction gives the hereditarily finite-supported Quine-atom model, whose two-element atom subsets have no choice function.

Build the cumulative universe over an infinite set $A$ of Quine atoms, and extend every permutation of $A$ recursively to its other sets. An object has finite support if every permutation fixing that finite subset of $A$ fixes the object. Retain objects whose members, recursively away from the atomic self-loops, also have finite support. Parameters and domains give finite supports for definable subsets and functional ranges; the collection of all retained subsets of a retained set is again supported. These observations verify separation, replacement and power set, and the pure natural-number hierarchy gives infinity. There is no choice function on the two-element subsets of $A$: swap two atoms outside its supposed finite support, fixing their unordered pair but interchanging either possible selected member.

The axiom asserts the existence of a set containing the empty set and closed under the successor operation $x\mapsto x\cup \{x\}$:In Zermelo–Fraenkel set theory, this supplies a set from which the set of natural numbers is constructed.

A set $I$ is inductive if it contains the empty set and contains $x\cup \{x\}$ whenever it contains $x$. The axiom of infinity asserts that an inductive set exists. The natural numbers form the least inductive set: intersect one inductive set with the class of objects belonging to every inductive set. This use of separation gives a set, and the defining class is closed under successor.

ZFC is Zermelo–Fraenkel set theory together with the axiom of choice.