Editing Zermelo–Fraenkel set theory (section)

=== 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.