Formulation of the Separation Axiom in Set Theory

I have a question regarding this formulation of the Separation Axiom:

I quote from the Book "Handbook of Mathematical Logic", the chapter from which this is taken could also be found here.

Now we can turn to the axioms. The first point in our analysis was that a set is entirely determined by its members. This is the content of our first axiom.

Extensionality Axiom: $\forall z(z \in x \leftrightarrow z \in y) \rightarrow x = y$.

One of th most important points established by our analysis is that certain collections of sets are sets. In translating this into our language, we face a difficulty: there is no general method of talking about collections in this language before we know that they are sets. There are, however, certain collections which we can talk about. Given a formula $\phi(x)$, we can say certain things about the collection of all sets $x$ such that $\phi(x)$. In particular, we can say that it is a set as follows: $\exists y \forall x(x \in y \leftrightarrow \phi(x))$. We abbreviate this expression to $Set\{ x : \phi(x) \}$. Our first principle of set existence is: if every member of a collection of sets belongs to the set $x$, then that collection is a set. To see this, suppose that $x$ is formed at state $S$ [...]

Separation Axiom: $\forall x (\phi(x) \to x \in y) \to Set\{ x : \phi(x) \}$.

For what is the term $\forall x (\phi(x) \to x \in y)$ in the Separation Axiom, wouldn't it be sufficient to just state $Set\{ x : \phi(x) \}$ i.e. the formulae $\exists y \forall x(x \in y \leftrightarrow \phi(x))$ as the Separation Axiom?

• The confusion, I think, lies in the difference between the formulations of the axiom given in the question and in Arthur's answer. I find the one given here to be obfuscating the fact that we want to create definable subsets; whereas the way Arthur (and indeed most, if not all, the formulations I have seen until today) wrote the axiom is much clearer. – Asaf Karagila Apr 18 '13 at 20:32

The Separation Axiom tells us that certain "definable" collections are sets. In particular, this form tells us that "definable" subfamilies of sets are themselves sets. The subformula $\forall x ( \phi (x) \rightarrow x \in y )$ is there to limit the Axiom to produce only subfamilies of collections that are already known to be sets. Without this condition it would be possible to use this form of the Axiom to conclude that $$\{ x : \neg ( x \in x ) \}$$ is a set, which is Bertrand Russell's famous paradox. Together with the condition we can only conclude that given any set $y$ the collection $$\{ x : x \in y \wedge x \notin x \}$$ is a set, from which we do not obviously derive a contradiction. (Usually this is used to prove the existence of the empty set $\varnothing$.)

Often this axiom (schema) takes a slightly different form:

If $\phi(x)$ is a formula (in which $z$ does not occur free) then $$( \forall y ) ( \exists z ) ( \forall x ) ( x \in z \leftrightarrow ( x \in y \wedge \phi (x) )$$ is an instance of the Axiom of Separation.

This form essentially tells us that collections of the form $\{ x \in y : \phi(x) \} = \{ x : x \in y \wedge \phi (x) \}$ are sets (whenever $y$ itself is a set).

Your proposal : i.e.

to assume that $Set \{x : \phi (x) \}$ stay for $\exists y \forall x( x \in y \leftrightarrow \phi (x))$

is simply the so-called "naive" Comprehension Axiom. As Arthur explained,

Russell (1901) pointed out that one could rephrase Cantor's paradox to get a really simple contradiction, directly from [it] ; define $R = \{x : x \notin x \}$. Then $R \in R \leftrightarrow R \notin R$, a contradiction.

The idea behind Comprehension Axiom is that for every condition that we can "imagine" there is a set containing all and only those objects that satisfy the condition.

Rephrased in first-order language, it becomes : for every condition that we can express in the language, i.e. for every formula $\phi(x)$ with $x$ free, there exists the set of those objects that ...

In order to avoid R's Paradox (and similar ones) different solutions are available; for example, restrict the possible "conditions" that can be used in the Comprehension Axiom.

Another solution was formulated by Zermelo (1908) and improved subsequently by Fraenkel and Skolem, based on the Separation Axiom.

His current formulation reflects the original Zermelo's idea: a "condition" can be applied to "generate" a new set only starting from an already existing set (i.e. "separating" it from the existing set).