Editing Zermelo–Fraenkel set theory (section)

== Axioms ==
{{See also|Axiom}}

There are many equivalent formulations of the ZFC axioms.<ref>{{harvnb|Fraenkel|Bar-Hillel|Lévy|1973}}</ref> The following particular axiom set is from {{harvtxt|Kunen|1980}}. The axioms in order below are expressed in a mixture of [[first-order logic]] and high-level abbreviations.
<!-- **NOTE TO EDITORS** The symbolic axioms are taken from Kunen and should not be changed without discussion on the talk page.  Making up a new set of axioms is original research. The English descriptions are new here and can be freely changed.  The choice of Kunen instead of Jech or some other author was arbitrary and is open for discussion on the talk page. -->

Axioms 1–8 form ZF, while the axiom 9 turns ZF into ZFC. Following {{harvtxt|Kunen|1980}}, we use the equivalent [[well-ordering theorem]] in place of the [[axiom of choice]] for axiom 9.

All formulations of ZFC imply that at least one set exists. Kunen includes an axiom that directly asserts the existence of a set, although he notes that he does so only "for emphasis".<ref>{{harvnb|Kunen|1980|page=10}}.</ref> Its omission here can be justified in two ways. First, in the standard semantics of first-order logic in which ZFC is typically formalized, the [[domain of discourse]] must be nonempty. Hence, it is a logical theorem of first-order logic that something exists{{snd}}usually expressed as the assertion that something is identical to itself, <math>\exists x ( x = x )</math>. Consequently, it is a theorem of every first-order theory that something exists. However, as noted above, because in the intended semantics of ZFC, there are only sets, the interpretation of this logical theorem in the context of ZFC is that some ''set'' exists. Hence, there is no need for a separate axiom asserting that a set exists. Second, however, even if ZFC is formulated in so-called [[free logic]], in which it is not provable from logic alone that something exists, the axiom of infinity asserts that an ''infinite'' set exists. This implies that ''a'' set exists, and so, once again, it is superfluous to include an axiom asserting as much.

=== Axiom of extensionality ===
{{Main|Axiom of extensionality}}

Two sets are equal (are the same set) if they have the same elements.

<div style="margin-left:1.6em;"><math>\forall x \forall y [\forall z (z \in x \Leftrightarrow z \in y) \Rightarrow x = y].</math></div>

The converse of this axiom follows from the substitution property of [[equality (mathematics)|equality]]. ZFC is constructed in first-order logic. Some formulations of first-order logic include identity; others do not. If the variety of first-order logic in which one is constructing set theory does not include equality "<math>=</math>", <math>x=y</math> may be defined as an abbreviation for the following formula:<ref>{{harvnb|Hatcher|1982|p=138}}, def.&nbsp;1.</ref> <math>\forall z [z \in x \Leftrightarrow z \in y] \land \forall w [x \in w \Leftrightarrow y \in w].</math>

In this case, the axiom of extensionality can be reformulated as

<div style="margin-left:1.6em;"><math>\forall x \forall y [\forall z (z \in x \Leftrightarrow z \in y) \Rightarrow \forall w (x \in w \Leftrightarrow y \in w)],</math></div>

which says that if <math>x</math> and <math>y</math> have the same elements, then they belong to the same sets.{{sfn|Fraenkel|Bar-Hillel|Lévy|1973}}

=== Axiom of regularity (also called the axiom of foundation) ===
{{Main|Axiom of regularity}}

Every non-empty set <math>x</math> contains a member <math>y</math> such that <math>x</math> and <math>y</math> are [[disjoint sets]].

<div style="margin-left:1.6em;"><math>\forall x [(\exists a ( a \in x)) \Rightarrow \exists y ( y \in x \land \lnot \exists z (z \in y \land z \in x))].</math>{{sfn|Shoenfield|2001|p=239}}</div>
or in modern notation:
<math>\forall x\,(x \neq \varnothing \Rightarrow \exists y (y \in x \land y \cap x = \varnothing)).</math>

This (along with the axioms of pairing and union) implies, for example, that no set is an element of itself and that every set has an [[ordinal number|ordinal]] [[rank (set theory)|rank]].

=== Axiom schema of specification (or of separation, or of restricted comprehension) ===
{{Main|Axiom schema of specification}}

Subsets are commonly constructed using [[set builder notation]]. For example, the even integers can be constructed as the subset of the integers <math>\mathbb{Z}</math> satisfying the [[Congruence modulo n|congruence modulo]] predicate <math>x \equiv 0 \pmod 2</math>:

<div style="margin-left:1.6em;"><math>\{x \in \mathbb{Z} : x \equiv 0 \pmod 2\}.</math></div>

In general, the subset of a set <math>z</math> obeying a formula <math>\varphi(x)</math> with one free variable <math>x</math> may be written as:

<div style="margin-left:1.6em;"><math>\{x \in z : \varphi(x)\}.</math></div>

The axiom schema of specification states that this subset always exists (it is an [[axiom schema|axiom ''schema'']] because there is one axiom for each <math>\varphi</math>). Formally, let <math>\varphi</math> be any formula in the language of ZFC with all free variables among <math>x,z,w_{1},\ldots,w_{n}</math> (<math>y</math> is not free in <math>\varphi</math>). Then:

<div style="margin-left:1.6em;"><math>\forall z \forall w_1 \forall w_2\ldots \forall w_n \exists y \forall x [x \in y \Leftrightarrow (( x \in z )\land \varphi(x,w_1,w_2,...,w_n,z) )].</math></div>

Note that the axiom schema of specification can only construct subsets and does not allow the construction of entities of the more general form:

<div style="margin-left:1.6em;"><math>\{x : \varphi(x)\}.</math></div>

This restriction is necessary to avoid [[Russell's paradox]] (let <math>y=\{x:x\notin x\}</math> then <math>y \in y \Leftrightarrow y \notin y</math>) and its variants that accompany naive set theory with [[unrestricted comprehension]] (since under this restriction <math>y</math> only refers to sets '''''within'' <math>z</math>''' that don't belong to themselves, and <math>y \in z</math> has '''''not''''' been established, even though  <math>y \subseteq z</math> is the case, so <math>y</math> stands in a separate position from which it can't refer to or comprehend itself; therefore, in a certain sense, this axiom schema is saying that in order to build a <math>y</math> on the basis of a formula <math>\varphi(x)</math>, we need to previously restrict the sets <math>y</math> will regard within a set <math>z</math> that leaves <math>y</math> outside so <math>y</math> can't refer to itself; or, in other words, sets shouldn't refer to themselves).

In some other axiomatizations of ZF, this axiom is redundant in that it follows from the [[axiom schema of replacement]] and the [[axiom of the empty set]].

On the other hand, the axiom schema of specification can be used to prove the existence of the [[empty set]], denoted <math>\varnothing</math>, once at least one set is known to exist. One way to do this is to use a property <math>\varphi</math> which no set has. For example, if <math>w</math> is any existing set, the empty set can be constructed as

<div style="margin-left:1.6em;"><math>\varnothing = \{u \in w \mid (u \in u) \land \lnot (u \in u) \}.</math></div>

Thus, the [[axiom of the empty set]] is implied by the nine axioms presented here.  The axiom of extensionality implies the empty set is unique (does not depend on <math>w</math>). It is common to make a [[definitional extension]] that adds the symbol "<math>\varnothing</math>" to the language of ZFC.

=== Axiom of pairing ===
{{Main|Axiom of pairing}}

If <math>x</math> and <math>y</math> are sets, then there exists a set which contains <math>x</math> and <math>y</math> as elements, for example if x = {1,2} and y = {2,3} then z will be {{1,2},{2,3}}

<div style="margin-left:1.6em;"><math>\forall x \forall y \exists z ((x \in z) \land (y \in z)).</math></div>

The axiom schema of specification must be used to reduce this to a set with exactly these two elements. The axiom of pairing is part of Z, but is redundant in ZF because it follows from the axiom schema of replacement if we are given a set with at least two elements. The existence of a set with at least two elements is assured by either the [[axiom of infinity]], or by the {{dubious span |date=July 2023 |axiom schema of specification}} and the [[axiom of the power set]] applied twice to any set.

=== Axiom of union ===
{{Main|Axiom of union}}

The [[Union (set theory)|union]] over the elements of a set exists. For example, the union over the elements of the set <math>\{\{1,2\},\{2,3\}\}</math> is <math>\{1,2,3\}.</math>

The axiom of union states that for any set of sets <math>\mathcal{F}</math>, there is a set <math>A</math> containing every element that is a member of some member of <math>\mathcal{F}</math>:
<div style="margin-left:1.6em;"><math>\forall \mathcal{F} \,\exists A \, \forall Y\, \forall x [(x \in Y \land Y \in \mathcal{F}) \Rightarrow x \in A].</math></div>

Although this formula doesn't directly assert the existence of <math>\cup \mathcal{F}</math>, the set <math>\cup \mathcal{F}</math> can be constructed from <math>A</math> in the above using the axiom schema of specification:
<div style="margin-left:1.6em;"><math>\cup \mathcal{F}=\{x\in A : \exists Y (x \in Y \land Y \in \mathcal{F})\}.</math></div>

=== Axiom schema of replacement ===
{{Main|Axiom schema of replacement}}

The axiom schema of replacement asserts that the [[image (mathematics)|image]] of a set under any definable [[Function (mathematics)|function]] will also fall inside a set.

Formally, let <math>\varphi</math> be any [[Well-formed formula|formula]] in the language of ZFC whose [[free variable]]s are among <math>x, y, A, w_1, \dotsc, w_n,</math> so that in particular <math>B</math> is not free in <math>\varphi</math>. Then:

<div style="margin-left:1.6em;"><math>\forall A\forall w_1 \forall w_2\ldots \forall w_n \bigl[\forall x ( x\in A \Rightarrow \exists! y\,\varphi ) \Rightarrow \exists B \ \forall x \bigl(x\in A \Rightarrow \exists y (y\in B \land \varphi)\bigr)\bigr].</math></div>

(The [[Uniqueness quantification|unique existential quantifier]] <math>\exists!</math> denotes the existence of exactly one element such that it follows a given statement.)

In other words, if the relation <math>\varphi</math> represents a definable function <math>f</math>, <math>A</math> represents its [[domain of a function|domain]], and <math>f(x)</math> is a set for every <math>x \in A,</math> then the [[range of a function|range]] of <math>f</math> is a subset of some set <math>B</math>. The form stated here, in which <math>B</math> may be larger than strictly necessary, is sometimes called the [[Axiom schema of replacement#Axiom schema of collection|axiom schema of collection]].

=== Axiom of infinity ===
{{Main|Axiom of infinity}}

{| class="floatright" style="background-color: #f8f9fa; border: 1px solid #a2a9b1; margin: 0.5em 0 0.5em 1em; padding: 0.2em; color:black;" <!-- Black is *not* the default color for text (yes, really!) -->
|+ First several von Neumann ordinals
|-
! scope="row" | 0
| = || {}
| = || ∅
|-
! scope="row" | 1
| = || {0}
| = || {∅}
|-
! scope="row" | 2
| = || {0,1}
| = || {∅,{∅}}
|-
! scope="row" | 3
| = || {0,1,2}
| = || {∅,{∅},{∅,{∅}}}
|-
! scope="row" | 4
| = || {0,1,2,3}
| = || {∅,{∅},{∅,{∅}},{∅,{∅},{∅,{∅}}}}
|}

Let <math>S(w)</math> abbreviate <math>w \cup \{w\},</math> where <math> w </math> is some set. (We can see that <math>\{w\}</math> is a valid set by applying the axiom of pairing with <math>x = y = w</math> so that the set {{mvar|z}} is <math>\{w\}</math>). Then there exists a set {{mvar|X}} such that the empty set <math>\varnothing</math>, defined axiomatically, is a member of {{mvar|X}} and, whenever a set {{mvar|y}} is a member of {{mvar|X}} then <math>S(y)</math> is also a member of {{mvar|X}}.

<div style="margin-left:1.6em;"><math>\exists X \left [\exists e (\forall z \, \neg (z \in e) \land e \in X) \land \forall y (y \in X \Rightarrow S(y)  \in X)\right].</math></div>

or in modern notation:
<math>\exists X \left [\varnothing \in X \land \forall y (y \in X \Rightarrow S(y)  \in X)\right].</math>

More colloquially, there exists a set {{mvar|X}} having infinitely many members. (It must be established, however, that these members are all different because if two elements are the same, the sequence will loop around in a finite cycle of sets. The axiom of regularity prevents this from happening.) The minimal set {{mvar|X}} satisfying the axiom of infinity is the [[von Neumann ordinal]] {{mvar|&omega;}} which can also be thought of as the set of [[natural numbers]] <math>\mathbb{N}.</math>

=== Axiom of power set ===
{{Main|Axiom of power set}}

By definition, a set <math>z</math> is a [[subset]] of a set <math>x</math> if and only if every element of <math>z</math> is also an element of <math>x</math>:

<div style="margin-left:1.6em;"><math>(z \subseteq x) \Leftrightarrow ( \forall q (q \in z \Rightarrow q \in x)).</math></div>

The Axiom of power set states that for any set <math>x</math>, there is a set <math>y</math> that contains every subset of <math>x</math>:

<div style="margin-left:1.6em;"><math>\forall x \exists y \forall z (z \subseteq x \Rightarrow z \in y).</math></div>

The axiom schema of specification is then used to define the [[power set]] <math>\mathcal{P}(x)</math> as the subset of such a <math>y</math> containing the subsets of <math>x</math> exactly:

<div style="margin-left:1.6em;"><math>\mathcal{P}(x) = \{ z \in y: z \subseteq x \}.</math></div>

Axioms ''1–8'' define ZF. Alternative forms of these axioms are often encountered, some of which are listed in {{harvtxt|Jech|2003}}. Some ZF axiomatizations include an axiom asserting that the [[axiom of empty set|empty set exists]]. The axioms of pairing, union, replacement, and power set are often stated so that the members of the set <math>x</math> whose existence is being asserted are just those sets which the axiom asserts <math>x</math> must contain.

The following axiom is added to turn ZF into ZFC:

=== Axiom of well-ordering (choice) ===
{{Main|Axiom of choice|Well-ordering theorem|Zorn's lemma}}

The last axiom, commonly known as the [[axiom of choice]], is presented here as a property about [[well-order]]s, as in {{harvtxt|Kunen|1980}}.
For any set <math>X</math>, there exists a [[binary relation]] <math>R</math> which [[well-order]]s <math>X</math>.  This means <math>R</math> is a [[linear order]] on <math>X</math> such that every nonempty [[subset]] of <math>X</math> has a [[least element]] under the order <math>R</math>.

<div style="margin-left:1.6em;"><math>\forall X \exists R ( R \;\mbox{well-orders}\; X).</math></div>

Given axioms ''1''&thinsp;–&thinsp;''8'', many statements are {{not a typo|provably}} equivalent to axiom ''9''. The most common of these goes as follows. Let <math>X</math> be a set whose members are all nonempty. Then there exists a function <math>f</math> from <math>X</math> to the union of the members of <math>X</math>, called a "[[choice function]]", such that for all <math>Y\in X</math> one has <math>f(Y)\in Y</math>. A third version of the axiom, also equivalent, is [[Zorn's lemma]].

Since the existence of a choice function when <math>X</math> is a [[finite set]] is easily proved from axioms ''1–8'', AC only matters for certain [[infinite set]]s. AC is characterized as [[constructive mathematics|nonconstructive]] because it asserts the existence of a choice function but says nothing about how this choice function is to be "constructed".