>>499
つづき

The axiom schema of unrestricted comprehension reads:
∀ w_1,・・・ ,w_n,∃ B,∀ x,(x∈ B←→ φ (x,w_1,・・・ ,w_n))
that is:
There exists a set B whose members are precisely those objects that satisfy the predicate φ.
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 ¬(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 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. Most of the other Zermelo?Fraenkel axioms (but not the axiom of extensionality, the axiom of regularity, or the axiom of choice) then became necessary to make up for some of what was lost by changing the axiom schema of comprehension to the axiom schema of specification ? each of these axioms states that a certain set exists, and defines that set by giving a predicate for its members to satisfy, i.e. it is a special case of the axiom schema of comprehension.

It is also possible to prevent the schema from being inconsistent by restricting which formulae it can be applied to, such as only stratified formulae in New Foundations (see below) or only positive formulae (formulae with only conjunction, disjunction, quantification and atomic formulae) in positive set theory. Positive formulae, however, typically aren't able to express certain things that most theories can; for instance, there is no complement or relative complement in positive set theory.

つづく