nLab
axiom of separation

Idea

In set theory, the axiom scheme of separation aka specification states that, given any set $X$ and any property $P$ of the elements of $X$, there is a set

$$\{X\mid P\}=\{a\in X\mid P(a)\}$$\{ X | P \} = \{ a \in X \;|\; P(a) \}

consisting precisely of those elements of $X$ for which $P$ holds:

$$a\in \{X\mid P\}\leftrightarrow a\in X\wedge P(a).$$a \in \{ X | P \} \;\leftrightarrow\; a \in X \;\wedge\; P(a) .

Note that $\{X\mid P\}$ is a subset of $X$.

It is important to specify what language $P$ can be written in. This connects the axiom to logic and the foundations of mathematics. Arguably, first-order logic developed in order to explain the meaning of Ernst Zermelo's axiom of separation (although Zermelo himself disagreed with the interpretation that this gave). Separation is (usually) given as an axiom scheme because there is one axiom for each way to state a property in the language. (We also allow parameters in $P$.)

Statements

From weaker to stronger:

• For bounded separation aka restricted separation aka ${\Delta }_0$-separation, $P$ must be written in the language of first-order set theory and all quantifications must be guarded by a set: of the form $\forall x\in A$ or $\exists x\in A$ for some set $A$.

• For limited separation aka ${\Delta }_0^{𝒫}$-separation, $P$ must be written in the language of first-order set theory and all quantifications must be guarded by a set or a power class: of the form $\forall x\in A$, $\exists B\subseteq A$, etc. Limited separation trivially implies bounded separation, while bounded separation implies limited separation if power sets exist.

• For full separation aka simply separation, $P$ must be written in the language of first-order set theory, but otherwise anything goes; in a class theory?, $P$ must be guarded by a class. Full separation trivially implies limited separation.

• For large separation, $P$ must be written in the language of first-order class theory; of course, this only makes sense in a class theory. The difference in strength between the class theories $\mathrm{MK}$ and $\mathrm{NBG}$ is precisely that the former has large separation but the latter does not.

• Separation is sometimes called restricted comprehension; for full comprehension aka simply comprehension, no set $X$ needs to be given ahead of time. Full comprehension was proposed by Gottlob Frege?, but leads to Russell's paradox. However, full comprehension can sometimes be allowed if the ambient logic is nonclassical, such as linear logic or paraconsistent logic.

• For stratified comprehension, no set $X$ is given, but $P$ is restricted to stratified formulas, in which each variable $x$ can be given a consistent natural number $\sigma (x)$ (its stratification) such that $x\in y$ appears in the formula only if $\sigma (y)=\sigma (x)+1$. This is used in Van Quine?'s New Foundations?.

In structural set theory

Set theory is usually given in material form, with a language based on a global membership relation $\in$, and we have implicitly followed this above. However, separation makes sense also in structural set theory (although full comprehension does not, except in a structural class theory with a class of all sets?, where it again leads to paradox). The conclusion of the axiom is the existence of a set

$$\{X\mid P\}=\{a:X\mid P(a)\}$$\{ X | P \} = \{ a\colon X \;|\; P(a) \}

and an injection $i_P:\{X\mid P\}\to X$ such that

$$\exists b:S,a=i_P(b)\leftrightarrow P(a).$$\exists b\colon S,\; a = i_P(b) \;\leftrightarrow\; P(a) .

Note that $\{X\mid P\}$, equipped with $i_P$, is a subset of $X$ in the structural sense.

The structural axioms can of course be stated even in a material set theory, where they are actually weaker than the corresponding material axioms; however, the material axioms follow (as usual) from the structural axioms using restricted replacement, which is quite weak (and also follows from the material form of bounded separation).

If a structural set theory is given by stating axioms for the category of sets, then restricted separation amounts to the property that this category is a Heyting category. If it is an elementary topos, then since it satisfies the power set axiom, this implies limited separation as well. Full separation is somewhat less natural to state category-theoretically, but the combination of full separation with the structural axiom of collection is equivalent to saying that the category of sets is autological?.

Axiom or axiom scheme?

Although usually presented as an axiom scheme, in many cases, all instances of separation follow from finitely many special cases (which can then be packaged into a single axiom, using conjunction, although this is probably pointless). This is the case, for example, in ETCS (a structural set theory that satisfied bounded separation) and NBG (a material class theory that satisfies full separation). In type-theoretic foundations of mathematics, separation is usually invisible, but again some form (generally only bounded) can again be proved from a few specific axioms or constructions.

Relation to the axiom of replacement

Full separation follows from the axiom of replacement and the principle of excluded middle (along with the axiom of the empty set). Therefore, the axiom is often left out entirely of a description of ZFC (the usually accepted foundation of mathematics). In versions of set theory for constructive mathematics, however, we often have replacement but only bounded or limited separation, and in any case separation must be listed explicitly.

category: foundational axiom