The ZFC Axioms and the Basic Set Constructions

The language of set theory is first-order logic with equality whose only non-logical symbol is a binary relation symbol $\in$. Its terms are the variables $x, y, z, \dots$; its atomic formulas are $x \in y$ and $x = y$; and its formulas are built from atomic formulas by the connectives $\neg$, $\wedge$, $\vee$, $\to$, $\leftrightarrow$ and the quantifiers $\forall x$ and $\exists x$. Each axiom stated on this page is a sentence of this language, and no other vocabulary occurs in any of them.

Two conventions of ordinary first-order logic are in force throughout.

• The domain of discourse is nonempty: $\exists x\,(x = x)$ is logically valid, so some object exists before any axiom is assumed.
• Every object of the domain is a set. There are no urelements, so "$z$" and "the set $z$" say the same thing.

We write $x \neq y$ for $\neg(x = y)$ and $x \notin y$ for $\neg(x \in y)$; we abbreviate $\forall z\,(z \in x \to \varphi)$ by $\forall z \in x\,\varphi$ and $\exists z\,(z \in x \wedge \varphi)$ by $\exists z \in x\,\varphi$; and we abbreviate $\exists w\,\bigl(\psi(w) \wedge \forall v\,(\psi(v) \to v = w)\bigr)$ by $\exists! w\,\psi(w)$, read "there is exactly one $w$ with $\psi(w)$".

A formula is written $\varphi(z, \bar p)$ when its free variables are among $z$ and the variables of the list $\bar p = p_1, \dots, p_n$; the $p_i$ are its parameters. Parameters matter because an axiom schema ranges over formulas, and a formula may mention sets already in hand.

A class abbreviation $\{\, z : \varphi(z, \bar p) \,\}$ is not a term of the language. It is notation for the formula $\varphi$ itself, and a sentence written with it abbreviates a sentence that does not use it:

• $w \in \{\, z : \varphi(z, \bar p) \,\}$ abbreviates $\varphi(w, \bar p)$;
• "$\{\, z : \varphi(z, \bar p) \,\}$ is a set" abbreviates $\exists y\,\forall z\,\bigl(z \in y \leftrightarrow \varphi(z, \bar p)\bigr)$.

Every formula has a class abbreviation, and whether that abbreviation is a set is a separate question; answering it affirmatively always requires an axiom.

• ZFC. ZFC is the theory whose axioms are the ZF axioms stated on this page together with the Axiom of Choice, which this library states at The Axiom of Choice ↗. Choice is stated there and not restated here, and no construction and no result on this page uses it. The axiom ledger for this page: which of the ZFC axioms each construction and each result actually consumes records, axiom by axiom, what the material on this page does use.

• Why the class notation needs its own convention. Reading $\{\, z : \varphi(z) \,\}$ as a term would make "$\{\, z : \varphi(z) \,\}$ exists" a triviality, and that is exactly the reading There is no $R$ with $x \in R \leftrightarrow x \notin x$ for every $x$ refutes. Keeping it an abbreviation is what forces every set-forming step below to name the axiom that licenses it.

The Axiom of Extensionality is the sentence

$\forall x\,\forall y\,\bigl(\forall z\,(z \in x \leftrightarrow z \in y) \to x = y\bigr)$

of the language of set theory (The first-order language of set theory: $\in$, $=$, formulas with parameters, and class abbreviations): if every $z$ satisfies $z \in x$ if and only if $z \in y$, then $x = y$.

A set is therefore determined by its members and by nothing else. Order, repetition and any description used to present a set are invisible to identity.

• The converse is logic, not an axiom. If $x = y$ then $z \in x$ and $z \in y$ are the same statement for every $z$, by the substitution rule for equality. So Extensionality upgrades to the biconditional $x = y \leftrightarrow \forall z\,(z \in x \leftrightarrow z \in y)$, and only the right-to-left direction of that biconditional — the implication from sameness of members to equality — is assumed.

• What it is used for below. Every construction on this page produces a set by an axiom that specifies its members, and every such axiom is stated with $\leftrightarrow$. Extensionality is what turns "a set with these members" into "the set with these members", so it is the licence for each definite article and each piece of notation introduced here.

Let $\varphi(z, \bar p)$ be a formula of the language of set theory (The first-order language of set theory: $\in$, $=$, formulas with parameters, and class abbreviations) in which the variable $y$ does not occur free. The Separation instance for $\varphi$ is the sentence

$\forall \bar p\,\forall x\,\exists y\,\forall z\,\bigl(z \in y \leftrightarrow (z \in x \wedge \varphi(z,\bar p))\bigr).$

The Axiom Schema of Separation is the collection of all these sentences, one for each such $\varphi$. In words: for any parameters $\bar p$ and any set $x$, there is a set $y$ whose elements are exactly the elements $z$ of $x$ for which $\varphi(z,\bar p)$ holds.

It is a schema and not a single axiom because $\varphi$ ranges over the formulas of the language, of which there are infinitely many, and the language provides no way to quantify over them.

• The side condition is not decoration. If $y$ were allowed to occur free in $\varphi$, the instance $\varphi(z,\bar p) := z \notin y$ would assert that some $y$ satisfies $z \in y \leftrightarrow (z \in x \wedge z \notin y)$ for every $z$, which is contradictory as soon as $x$ has a member. Requiring $y$ to be fresh is what keeps the schema consistent.

• One parameter or a list. Some presentations state the schema with a single parameter $p$ rather than a list $\bar p$; the two forms prove the same theorems, since a finite list can be coded once ordered pairs are available. The list form is used here because the instances below quantify over several sets at once.

• A separated set is unique. The instance is stated with $\leftrightarrow$, so any two sets it produces have the same elements and are equal by The Axiom of Extensionality: $\forall x\,\forall y\,(\forall z\,(z \in x \leftrightarrow z \in y) \to x = y)$. That is what licenses the notation $\{\, z \in x : \varphi(z,\bar p) \,\}$ introduced at Subset $x \subseteq y$, proper subset $x \subsetneq y$, and the separation notation $\{\, z \in x : \varphi(z) \,\}$.

The Axiom of Pairing is the sentence

$\forall x\,\forall y\,\exists z\,\forall t\,\bigl(t \in z \leftrightarrow (t = x \vee t = y)\bigr)$

of the language of set theory (The first-order language of set theory: $\in$, $=$, formulas with parameters, and class abbreviations): for any $x$ and $y$ there is a set $z$ whose elements are exactly $x$ and $y$.

• The weak form is equivalent, given Separation. Several presentations assume only $\forall x\,\forall y\,\exists z\,(x \in z \wedge y \in z)$, a set containing $x$ and $y$ and possibly more, and then cut it down with The Axiom Schema of Separation: for each formula $\varphi$, $\forall \bar p\,\forall x\,\exists y\,\forall z\,(z \in y \leftrightarrow (z \in x \wedge \varphi(z,\bar p)))$ applied to the formula $t = x \vee t = y$. The result is the set asserted here, so the two forms yield the same theorems. The same choice arises for The Axiom of Power Set: $\forall x\,\exists y\,\forall z\,(\forall t\,(t \in z \to t \in x) \to z \in y)$, where the weak form is the one assumed, so that the trimming step is visible in the ledger.

• Order and repetition are invisible. Taking $y := x$ gives a set whose only element is $x$. Because $t = x \vee t = y$ and $t = y \vee t = x$ are the same condition, the axiom does not distinguish the pair formed from $x$ then $y$ from the pair formed from $y$ then $x$; recovering an order from a set is the problem The Kuratowski ordered pair $(a,b) := \{\{a\},\{a,b\}\}$ solves.

The Axiom of Union is the sentence

$\forall x\,\exists y\,\forall z\,\bigl(z \in y \leftrightarrow \exists s\,(s \in x \wedge z \in s)\bigr)$

of the language of set theory (The first-order language of set theory: $\in$, $=$, formulas with parameters, and class abbreviations): for any set $x$ there is a set $y$ whose elements are exactly the sets $z$ belonging to some member $s$ of $x$.

The axiom removes one layer of membership: it collects the members of the members of $x$, not the members of $x$.

• The weak form is equivalent, given Separation. Some presentations assume only $\forall x\,\exists y\,\forall s\,\forall z\,((s \in x \wedge z \in s) \to z \in y)$ and then cut $y$ down with The Axiom Schema of Separation: for each formula $\varphi$, $\forall \bar p\,\forall x\,\exists y\,\forall z\,(z \in y \leftrightarrow (z \in x \wedge \varphi(z,\bar p)))$. The set obtained is the one asserted here.

• Nothing is assumed about the members of $x$. They need not be nonempty, need not be distinct, and need not be related to one another. When $x$ itself has no members the right-hand side fails for every $z$, and the axiom yields a set with no members; this is computed at $\bigcup \varnothing = \varnothing$, $\bigcup \{a\} = a$, $\bigcup \{a,b\} = a \cup b$, $\bigcap \{a\} = a$, and $\bigcap \{a,b\} = a \cap b$.

The Axiom of Power Set is the sentence

$\forall x\,\exists y\,\forall z\,\bigl(\forall t\,(t \in z \to t \in x) \to z \in y\bigr)$

of the language of set theory (The first-order language of set theory: $\in$, $=$, formulas with parameters, and class abbreviations): for every set $x$ there is a set $y$ that contains every $z$ all of whose elements belong to $x$.

The axiom is assumed here in this implication form. It says that some set collects all such $z$; it does not say that $y$ contains nothing else, and trimming $y$ down to exactly those $z$ is a separate step, carried out at For every set $x$ there is exactly one set whose elements are precisely the subsets of $x$ using The Axiom Schema of Separation: for each formula $\varphi$, $\forall \bar p\,\forall x\,\exists y\,\forall z\,(z \in y \leftrightarrow (z \in x \wedge \varphi(z,\bar p)))$.

• Why the weak form. Some presentations assume the biconditional $\forall t\,(t \in z \to t \in x) \leftrightarrow z \in y$ outright. The implication form assumed here is the weaker assumption, and it keeps the Separation step visible: the ledger at The axiom ledger for this page: which of the ZFC axioms each construction and each result actually consumes then records honestly that the power set costs Power Set and Separation.

• The axiom says nothing about size. It asserts that a set collecting the subsets of $x$ exists, and nothing about how many members that set has. How large the power set of an infinite set is, is exactly the question the continuum hypothesis asks, and that question is settled by neither ZF nor ZFC (The continuum hypothesis and its generalisation are independent of ZFC ‡).

Let $\varphi(z, w, \bar p)$ be a formula of the language of set theory (The first-order language of set theory: $\in$, $=$, formulas with parameters, and class abbreviations) in which $A$ and $B$ do not occur free. The Replacement instance for $\varphi$ is the sentence

$\forall \bar p\,\forall A\,\Bigl(\forall z\,\bigl(z \in A \to \exists! w\,\varphi(z,w,\bar p)\bigr) \to \exists B\,\forall w\,\bigl(w \in B \leftrightarrow \exists z\,(z \in A \wedge \varphi(z,w,\bar p))\bigr)\Bigr).$

The Axiom Schema of Replacement is the collection of all these sentences, one for each such $\varphi$. In words: if for every $z \in A$ there is exactly one $w$ with $\varphi(z,w,\bar p)$, then there is a set $B$ whose elements are exactly those $w$.

• The class-function reading. A formula $\varphi(z,w,\bar p)$ satisfying $\forall z \in A\ \exists! w\,\varphi(z,w,\bar p)$ assigns to each $z \in A$ a single $w$, so it behaves like a function on $A$ without being a set of ordered pairs; it is called a class function on $A$. The instance says that the image of a set under a class function is a set. The hypothesis is required only on $A$: what $\varphi$ does outside $A$ is irrelevant.

• Replacement yields Separation, given a set with no elements. Fix a set $x$ and a formula $\psi(z,\bar p)$. If some $c \in x$ satisfies $\psi(c,\bar p)$, then $\varphi(z,w,\bar p,c) := (\psi(z,\bar p) \wedge w = z) \vee (\neg\psi(z,\bar p) \wedge w = c)$ assigns exactly one $w$ to each $z \in x$, so an instance of this schema applied to $x$ returns the set of those $w$; that set is exactly the one The Axiom Schema of Separation: for each formula $\varphi$, $\forall \bar p\,\forall x\,\exists y\,\forall z\,(z \in y \leftrightarrow (z \in x \wedge \varphi(z,\bar p)))$ asserts, since the value $c$ contributed by the second disjunct itself satisfies $\psi$. If instead no $c \in x$ satisfies $\psi(c,\bar p)$, the set to be produced has no elements, and a set with no elements is asserted outright by The Axiom of Infinity: there is a set containing a set with no elements and closed under $y \mapsto y \cup \{y\}$. The case split is not avoidable: the hypothesis of the schema demands a value at every $z \in x$, so the collection being separated cannot itself be taken as the domain. Separation is nevertheless stated separately, because every construction on this page uses Separation and no construction on this page needs the full strength of Replacement.

• Where Replacement is genuinely needed. Nothing on this page consumes it; The axiom ledger for this page: which of the ZFC axioms each construction and each result actually consumes records that. It becomes indispensable for transfinite recursion and for the ordinal and cardinal hierarchies, where the sets constructed are not subsets of any set already in hand.

The Axiom of Infinity is the sentence

$\exists I\,\Bigl(\exists e\,\bigl(e \in I \wedge \neg\exists t\,(t \in e)\bigr) \wedge \forall y\,\bigl(y \in I \to \exists s\,(s \in I \wedge \forall t\,(t \in s \leftrightarrow (t \in y \vee t = y)))\bigr)\Bigr)$

of the language of set theory (The first-order language of set theory: $\in$, $=$, formulas with parameters, and class abbreviations).

It is written here in $\in$ and $=$ alone, with no abbreviations, because the notation it is usually stated in is introduced later on this page. Once that notation is available, the sentence reads: there is a set $I$ with $\varnothing \in I$ such that $y \in I$ implies $y \cup \{y\} \in I$. The first conjunct is $\varnothing \in I$ written out, and the inner clause $\forall t\,(t \in s \leftrightarrow (t \in y \vee t = y))$ says exactly that $s$ is $y \cup \{y\}$.

• The only unconditional existence assertion on this page. Extensionality and Foundation produce no sets at all, and every other axiom produces new sets from sets already given; this one asserts outright that a set $I$ with the two stated properties exists. Two results below say what its closure clause does: $y \cup \{y\}$ is never $y$, since $y$ is one of its elements while $y \notin y$ (Under Foundation, $x \notin x$ for every set $x$, there are no sets with $x \in y \in x$, and there are no sets with $x \in y \in z \in x$), and $y \mapsto y \cup \{y\}$ is injective (If $x \cup \{x\} = y \cup \{y\}$ then $x = y$).

• Inductive sets and $\mathbb{N}$. A set satisfying the two conjuncts above is what Inductive set ↗ calls inductive, and the natural numbers are built at The natural numbers $\mathbb{N}$ (von Neumann) ↗ as the smallest inductive set. Those items state the axiom in the abbreviated form; the sentence displayed above is the same assertion with the abbreviations expanded.

The Axiom of Foundation, also called the Axiom of Regularity, is the sentence

$\forall S\,\Bigl(\exists t\,(t \in S) \to \exists s\,\bigl(s \in S \wedge \neg\exists u\,(u \in s \wedge u \in S)\bigr)\Bigr)$

of the language of set theory (The first-order language of set theory: $\in$, $=$, formulas with parameters, and class abbreviations): every set with at least one member has a member $s$ that shares no member with it.

It is written here without abbreviations, for the same reason as The Axiom of Infinity: there is a set containing a set with no elements and closed under $y \mapsto y \cup \{y\}$: the usual statement uses notation introduced later on this page. In that notation it reads: every nonempty set $S$ has a member $s$ with $s \cap S = \varnothing$. Such an $s$ is called an $\in$-minimal member of $S$.

• What it rules out. A set $S$ that had no $\in$-minimal member would let one descend forever through membership. The axiom forbids that, and Under Foundation, $x \notin x$ for every set $x$, there are no sets with $x \in y \in x$, and there are no sets with $x \in y \in z \in x$ draws the consequences that this page needs: no set is a member of itself, and there is no membership cycle of length two or three.

• It is used nowhere else on this page. Every other construction below is carried out without it; the ledger at The axiom ledger for this page: which of the ZFC axioms each construction and each result actually consumes records exactly which results depend on it.

There is exactly one set with no elements: there is a set $e$ such that $\neg\exists z\,(z \in e)$, and any two such sets are equal. That set is written $\varnothing$.

• Existence is derived, not assumed. Several presentations take "there is a set with no elements" as an axiom of its own. Here it is a theorem, because the nonemptiness of the domain of discourse is already a validity of first-order logic and Separation converts any set whatever into this one.

For sets $x$ and $y$ we write $x \subseteq y$, and say that $x$ is a subset of $y$ or that $x$ is included in $y$, for the formula $\forall t\,(t \in x \to t \in y)$ of the language of set theory (The first-order language of set theory: $\in$, $=$, formulas with parameters, and class abbreviations); thus $x \subseteq y$ means that every element of $x$ is an element of $y$. We also write $y \supseteq x$ for $x \subseteq y$.

$x$ is a proper subset of $y$, written $x \subsetneq y$, when $x \subseteq y$ and $x \neq y$.

Separation notation. Let $x$ be a set, $\varphi(z,\bar p)$ a formula and $\bar p$ parameters. The Axiom Schema of Separation: for each formula $\varphi$, $\forall \bar p\,\forall x\,\exists y\,\forall z\,(z \in y \leftrightarrow (z \in x \wedge \varphi(z,\bar p)))$ supplies a set whose elements are exactly the elements $z$ of $x$ for which $\varphi(z,\bar p)$ holds, and The Axiom of Extensionality: $\forall x\,\forall y\,(\forall z\,(z \in x \leftrightarrow z \in y) \to x = y)$ shows there is only one such set. It is written

$\{\, z \in x : \varphi(z,\bar p) \,\}$

and every set introduced on this page by separating a condition inside a set already in hand is written this way. Directly from the definition, $\{\, z \in x : \varphi(z,\bar p) \,\} \subseteq x$.

• $\subset$ is not used in this library. Sources disagree about it: some write $\subset$ for inclusion and some for proper inclusion, so a formula containing it cannot be read without knowing which convention its author used. $\subseteq$ and $\subsetneq$ are unambiguous and are the only two symbols used here.

• Membership and inclusion are different relations. $t \in x$ says $t$ is one of the elements of $x$; $t \subseteq x$ says every element of $t$ is an element of $x$. Neither implies the other in general, and $\mathcal{P}(\varnothing) = \{\varnothing\}$; $\varnothing \in \mathcal{P}(a)$ and $a \in \mathcal{P}(a)$; $a \subseteq b$ if and only if $\mathcal{P}(a) \subseteq \mathcal{P}(b)$; $\bigcup \mathcal{P}(a) = a$; $\bigcap \mathcal{P}(a) = \varnothing$; and $\mathcal{P}(a \cap b) = \mathcal{P}(a) \cap \mathcal{P}(b)$ while only $\mathcal{P}(a) \cup \mathcal{P}(b) \subseteq \mathcal{P}(a \cup b)$ holds is where the two are systematically related.

For all sets $x$, $y$ and $z$:

• (i) $\varnothing \subseteq x$;
• (ii) $x \subseteq x$;
• (iii) if $x \subseteq y$ and $y \subseteq z$ then $x \subseteq z$;
• (iv) $x = y$ if and only if $x \subseteq y$ and $y \subseteq x$.

Let $x$ and $y$ be sets. The Axiom of Pairing: $\forall x\,\forall y\,\exists z\,\forall t\,(t \in z \leftrightarrow (t = x \vee t = y))$ gives a set whose elements are exactly $x$ and $y$, and The Axiom of Extensionality: $\forall x\,\forall y\,(\forall z\,(z \in x \leftrightarrow z \in y) \to x = y)$ shows there is only one such set; it is written $\{x,y\}$. Thus $\{x,y\}$ is the set whose elements are exactly $x$ and $y$, and $\{x\} := \{x,x\}$, the singleton of $x$, is the set whose only element is $x$:

$t \in \{x,y\} \leftrightarrow (t = x \vee t = y), \qquad t \in \{x\} \leftrightarrow t = x .$

• The pair is unordered. $t = x \vee t = y$ and $t = y \vee t = x$ are the same condition, so $\{x,y\} = \{y,x\}$, and the notation records no order. $\{a,b\} = \{c,d\}$ if and only if ($a = c$ and $b = d$) or ($a = d$ and $b = c$); in particular $\{a\} = \{c,d\}$ if and only if $a = c = d$ says exactly how much information a pair does carry, and The Kuratowski ordered pair $(a,b) := \{\{a\},\{a,b\}\}$ is the construction that recovers an order from unordered pairs alone.

• A singleton is not its element. $\{x\}$ has exactly one element, namely $x$, and $x$ and $\{x\}$ are different sets whenever they have different elements; $\{\varnothing\}$ has one element while $\varnothing$ has none, so the two are already distinct at the bottom of the hierarchy.

For all sets $a$, $b$, $c$, $d$:

$\{a,b\} = \{c,d\} \ \leftrightarrow\ \bigl((a = c \wedge b = d) \vee (a = d \wedge b = c)\bigr).$

In particular, taking $b := a$, $\{a\} = \{c,d\}$ if and only if $a = c$ and $a = d$.

Let $x$ be a set. The Axiom of Union: $\forall x\,\exists y\,\forall z\,(z \in y \leftrightarrow \exists s\,(s \in x \wedge z \in s))$ gives a set whose elements are exactly the sets $z$ belonging to some member of $x$, and The Axiom of Extensionality: $\forall x\,\forall y\,(\forall z\,(z \in x \leftrightarrow z \in y) \to x = y)$ shows there is only one such set; it is written $\bigcup x$. Thus $\bigcup x$ is the set whose elements are exactly the elements of the elements of $x$, and $a \cup b := \bigcup\{a,b\}$ is the binary union of $a$ and $b$, formed from the unordered pair of The unordered pair $\{x,y\}$ and the singleton $\{x\} = \{x,x\}$:

$z \in \bigcup x \leftrightarrow \exists s\,(s \in x \wedge z \in s).$

The membership criterion for the binary union, that $z \in a \cup b$ holds exactly when $z \in a$ or $z \in b$, is proved at $\bigcup \varnothing = \varnothing$, $\bigcup \{a\} = a$, $\bigcup \{a,b\} = a \cup b$, $\bigcap \{a\} = a$, and $\bigcap \{a,b\} = a \cap b$ rather than assumed here.

• One layer only. $\bigcup x$ collects the elements of the elements of $x$, not the elements of $x$. For a set of sets of sets the operation therefore has to be applied twice, and that iteration is what makes $\bigcup\bigcup R$ the right ambient set for the domain and range of a relation.

• Notation. $\bigcup$ with a single set argument is the primitive operation supplied by the axiom; $\cup$ between two sets is the derived binary one. The indexed form $\bigcup_{i \in I} A_i$ is a further abbreviation, defined once indexed families are available.

Let $x$ be a set with $x \neq \varnothing$. Then there is a set whose elements are exactly the sets belonging to every member of $x$; that is, the class $\{\, z : \forall s\,(s \in x \to z \in s) \,\}$ is a set. Moreover, for every $B \in x$ the separated set $\{\, z \in B : \forall s\,(s \in x \to z \in s) \,\}$ is that same set, so the construction does not depend on which member of $x$ is used.

Let $x$ be a set with $x \neq \varnothing$. For a set $x \neq \varnothing$ the collection $\{\, z : \forall s\,(s \in x \to z \in s) \,\}$ is a set, and it does not depend on the member of $x$ used to separate it shows that the sets belonging to every member of $x$ form a set, and that it does not depend on the member of $x$ used to build it; it is written $\bigcap x$. Thus for $x \neq \varnothing$, $\bigcap x$ is the set whose elements are exactly the sets belonging to every element of $x$, and $a \cap b := \bigcap\{a,b\}$ is the binary intersection of $a$ and $b$:

$z \in \bigcap x \leftrightarrow \forall s\,(s \in x \to z \in s) \quad (x \neq \varnothing).$

The binary case is legitimate because $a \in \{a,b\}$, so the unordered pair of The unordered pair $\{x,y\}$ and the singleton $\{x\} = \{x,x\}$ is never empty. Two sets $a$ and $b$ are disjoint when $a \cap b = \varnothing$ (There is exactly one set with no elements, written $\varnothing$).