Axiom schema of specification

From Wikipedia, the free encyclopedia
  (Redirected from Axiom of separation)
Jump to: navigation, search
"Axiom of separation" redirects here. For the separation axioms in topology, see separation axiom.

In axiomatic set theory and the branches of logic, mathematics, and computer science that use it, the axiom schema of specification, axiom schema of separation, subset axiom scheme or axiom schema of restricted comprehension is a schema of axioms in Zermelo–Fraenkel set theory. Essentially, it says that any definable subclass of a set is a set.



One instance of the schema is included for each formula φ in the language of set theory with free variables among x, w1, ..., wn, A. So B is not free in φ. In the formal language of set theory, the axiom schema is:

\forall w_1,\ldots,w_n \, \forall A \, \exists B \, \forall x \, ( x \in B \Leftrightarrow [ x \in A \and \varphi(x, w_1, \ldots, w_n , A) ] )

or in words:






Relation to the axiom schema of replacement[edit]


First, recall this axiom schema:

\forall A \, \exists B \, \forall C \, ( C \in B \iff \exists D \, [ D \in A \and C = F(D) ] )


For this reason, the axiom schema of separation is often left out of modern lists of the Zermelo–Fraenkel axioms. However, it's still important for historical considerations, and for comparison with alternative axiomatizations of set theory, as can be seen for example in the following sections.

Unrestricted comprehension[edit]

The axiom schema of comprehension (unrestricted) reads:

\forall w_1,\ldots,w_n \, \exists B \, \forall x \, ( x \in B \Leftrightarrow \varphi(x, w_1, \ldots, w_n) )

that is:


This set B is again unique, and is usually denoted as {x : φ(x, w1, ... wn)}.

This axiom schema was tacitly used in the early days of naive set theory, before a strict axiomatization was adopted. Unfortunately, it leads directly to Russell's paradox by taking φ(x) to be ¬(xx) (i.e., the property that set x is not a member of itself). Therefore, no useful axiomatization of set theory can use unrestricted comprehension, at least not with classical logic.


In NBG class theory[edit]


\exists D \forall C \, ( [ C \in D ] \iff [ P (C) \and \exists E \, ( C \in E ) ] ) \,,

that is,




\forall D \forall A \, ( \exists E \, [ A \in E ] \implies \exists B \, [ \exists E \, ( B \in E ) \and \forall C \, ( C \in B \iff [ C \in A \and C \in D ] ) ] ) \,,

that is,


or even more simply



\forall A \forall B \, ( [ \exists E \, ( A \in E ) \and \forall C \, ( C \in B \implies C \in A ) ] \implies \exists E \, [ B \in E ] ) \,,

that is,

"A subclass of a set is a set.".

In higher-order settings[edit]



In Quine's New Foundations[edit]
