Editing Axiom schema of specification (section)

== Statement ==
One instance of the schema is included for each [[Well-formed formula|formula]] <math>\varphi</math> in the language of set theory with [[free variables]] among ''x'', ''w''<sub>1</sub>, ..., ''w''<sub>''n''</sub>, ''A''. So ''B'' does not occur free in <math>\varphi</math>. In the formal language of set theory, the axiom schema is:
:<math>\forall w_1,\ldots,w_n \, \forall A \, \exists B \, \forall x \, ( x \in B \Leftrightarrow [ x \in A \land \varphi(x, w_1, \ldots, w_n , A) ] )</math>

or in words:
: Given any [[Set (mathematics)|set]] ''A'', [[Existential quantification|there is]] a set ''B'' (a subset of ''A'') such that, given any set ''x'', ''x'' is a member of ''B'' [[if and only if]] ''x'' is a member of ''A'' [[logical conjunction|and]] <math>\varphi</math> holds for ''x''. 
Note that there is one axiom for every such [[predicate (mathematics)|predicate]] <math>\varphi</math>; thus, this is an [[axiom schema]].

To understand this axiom schema, note that the set ''B'' must be a [[subset]] of ''A''. Thus, what the axiom schema is really saying is that, given a set ''A'' and a predicate <math>\varphi</math>, we can find a subset ''B'' of ''A'' whose members are precisely the members of ''A'' that satisfy <math>\varphi</math>.  By the [[axiom of extensionality]] this set is unique.  We usually denote this set using [[set-builder notation]] as <math>B = \{x\in A | \varphi(x) \}</math>. Thus the essence of the axiom is:
: Every [[Subclass (set theory)|subclass]] of a set that is defined by a predicate is itself a set.

The preceding form of separation was introduced in 1930 by [[Thoralf Skolem]] as a refinement of a previous, non-first-order<ref>F. R. Drake, ''Set Theory: An Introduction to Large Cardinals (1974), pp.12--13. ISBN 0 444 10535 2.</ref> form by Zermelo.<ref>W. V. O. Quine, ''Mathematical Logic'' (1981), p.164. Harvard University Press, 0-674-55451-5</ref> The axiom schema of specification is characteristic of systems of [[axiomatic set theory]] related to the usual set theory [[ZFC]], but does not usually appear in radically different systems of [[alternative set theory]].  For example, [[New Foundations]] and [[positive set theory]] use different restrictions of the [[#Unrestricted comprehension|axiom of comprehension]] of [[naive set theory]]. The [[Alternative Set Theory]] of Vopenka makes a specific point of allowing proper subclasses of sets, called [[semiset]]s.  Even in systems related to ZFC, this scheme is sometimes restricted to formulas with bounded quantifiers, as in [[Kripke–Platek set theory with urelements]].