디멘의 블로그 Dimen's Blog
이데아를 여행하는 히치하이커
Alice in Logicland

EN

List of ZFC Axioms

Mathematics
Set Theory
Name Meaning
Extensionality Set is an unordered collection of elements.
Existence* There exists the empty set.
Pairing* From $X, Y$ follows $Z = \lbrace X, Y \rbrace$.
Union From $X = \lbrace Y_i \rbrace$ follows $Z = \bigcup Y_i$.
Power Set From $X$ follows $\mathcal{P}(X)$.
Separation Schema** From $X$ follows $Y = \lbrace y \in X : \phi(y) \rbrace$, where $\phi$ is a first-order formula.
Infinity There exists a set containing all the natural numbers.
Regularity $\in$ is a well-ordering.
Replacement From $X$ follows $f[X]$, where $f$ is a class function definable in first-order logic.
Choice Every collection of nonempty sets $\lbrace X_i \rbrace$ has a choice function.
Name Formula (Free variables are to be quantified by $\forall$)
Extensionality $X = Y \leftrightarrow (z \in X \leftrightarrow z \in Y)$
Existence* $\exists Z : z \not\in Z$
Pairing* $\exists Z : z \in Z \leftrightarrow (z = X \lor z = Y)$
Union $\exists Z : z \in Z \leftrightarrow \exists x \in X (z \in x)$
Power Set $\exists Z : z \in Z \leftrightarrow (w \in z \rightarrow w \in X)$
Separation Schema** $\exists Z : z \in Z \leftrightarrow (z \in X \land \phi(z))$
Infinity $\exists Z : \varnothing \in Z \land (z \in Z \rightarrow z \cup \lbrace z \rbrace \in Z)$
Regularity $\exists x \in X : \forall y \in X [ y \not\in x]$
Replacement $\displaylines{[\forall x \in X \; \exists! y :\phi(x, y)] \rightarrow [\exists Y \; \forall x \in X \; \exists y \in Y : \phi(x, y)]}$
Choice $\displaylines{\varnothing \notin X \rightarrow \exists f : X \rightarrow \bigcup X [ f(x) \in x ]}$

Remarks.

  • Regularity is equivalent to the following:
\[\exists x \in X : x \cap X = \varnothing\]
  • Those marked by (*) can be derived from the Separation.

  • Those marked by (**) can be derived from the Replacement.

Replacement is strictly stronger than Separation:

  • Separation can be stated as: If $X$ is a set and $f$ is a function, then $f[X]$ is a set.
  • Replacement can be stated as: If $X$ is a set and $f$ is a class function, then $f[X]$ is a set.

The proof of following theorems require Choice.

  • If $f: X → Y$ is surjective, there exists a subset $Z$ of $X$ such that $f\vert_Z$ is bijective.
  • If $\varnothing \not\in \lbrace X_i\rbrace$, then $\prod X_i \neq \varnothing$.
  • Well-ordering Principle. Every set can be well-ordered.
  • Zorn’s Lemma. If every chain of $(X, <)$ is bounded in $X$, $X$ has a maximal element.

The proof of following theorems require Replacement.