Because restricting comprehension avoided Russell's paradox, several mathematicians including Zermelo, Fraenkel, and Gödel considered it the most important axiom of set theory.
[5] One instance of the schema is included for each formula φ in the language of set theory with free variables among x, w1, ..., wn, A.
To understand this axiom schema, note that the set B must be a subset of A.
We usually denote this set using set-builder notation as
Thus the essence of the axiom is: The preceding form of separation was introduced in 1930 by Thoralf Skolem as a refinement of a previous, non-first-order[6] form by Zermelo.
[7] 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 axiom of comprehension of naive set theory.
The Alternative Set Theory of Vopenka makes a specific point of allowing proper subclasses of sets, called semisets.
Even in systems related to ZFC, this scheme is sometimes restricted to formulas with bounded quantifiers, as in Kripke–Platek set theory with urelements.
[8][a] The axiom schema of replacement says that, if a function
: To derive the axiom schema of specification, let
guaranteed by the axiom schema of replacement is precisely the set
required in the axiom schema of specification.
in the axiom schema of specification is the empty set, whose existence (i.e., the axiom of empty set) is then needed.
[8] For this reason, the axiom schema of specification is left out of some axiomatizations of ZF (Zermelo–Fraenkel set theory),[9] although some authors, despite the redundancy, include both.
[11] The axiom schema of unrestricted comprehension reads:
that is: This set B is again unique, and is usually denoted as {x : φ(x, w1, ..., wb)}.
In an unsorted material set theory, the axiom or rule of full or unrestricted comprehension says that for any property P, there exists a set {x | P(x)} of all objects satisfying P.[12] This axiom schema was tacitly used in the early days of naive set theory, before a strict axiomatization was adopted.
However, it was later discovered to lead directly to Russell's paradox, by taking φ(x) to be ¬(x ∈ x) (i.e., the property that set x is not a member of itself).
Therefore, no useful axiomatization of set theory can use unrestricted comprehension.
Passing from classical logic to intuitionistic logic does not help, as the proof of Russell's paradox is intuitionistically valid.
Accepting only the axiom schema of specification was the beginning of axiomatic set theory.
Positive formulae, however, typically are unable to express certain things that most theories can; for instance, there is no complement or relative complement in positive set theory.
that is, provided that the quantifiers in the predicate P are restricted to sets.
This theorem schema is itself a restricted form of comprehension, which avoids Russell's paradox because of the requirement that C be a set.
Then specification for sets themselves can be written as a single axiom
that is, or even more simply In this axiom, the predicate P is replaced by the class D, which can be quantified over.
This is much the same trick as was used in the NBG axioms of the previous section, where the predicate was replaced by a class that was then quantified over.
In the New Foundations approach to set theory pioneered by W. V. O. Quine, the axiom of comprehension for a given predicate takes the unrestricted form, but the predicates that may be used in the schema are themselves restricted.
The predicate (C is not in C) is forbidden, because the same symbol C appears on both sides of the membership symbol (and so at different "relative types"); thus, Russell's paradox is avoided.