ZFC's Axiom Schema of Separation/Specification Implies Contradiction?

The Axiom Schema of Separation is: $\forall a \forall \Psi (x) \exists x \forall y (y \in x \leftrightarrow y \in a \space \land \Psi (y))$. If we make $a:=\{\emptyset\}$, $\Psi (x) :\leftrightarrow \lnot y \in x$, $x:=x$ and $y :=\emptyset$, we get the following: $y \in x \leftrightarrow y \in \{\emptyset\} \space \land \lnot y \in x$. This in turn implies: $y \in x \leftrightarrow \lnot y \in x$, which is contradictory and should negate the Axiom due to Modus Tollendo Tollens. Where am I wrong?

The genuine axiom scheme of separation requires that the formula used to specify the elements of the "separated" set does not refer to that set.

A correct statement of the scheme is

$$\forall z_1\cdots \forall z_k\forall a\exists x\forall y(y\in x\leftrightarrow y\in a\land \Psi(y,z_1,\ldots,z_k))$$

where $\Psi(y,z_1,\ldots,z_k)$ is a formula whose free variables are drawn from $y,z_1,\ldots,z_k$.

• ... and the condition is necessari exactly to avoid the above "misuse"; see Patrick Suppes, Axiomatic set theory (1960), page 21 for the same example. – Mauro ALLEGRANZA Sep 22 '15 at 11:35
• ...hey, nice reference! – mmw Sep 22 '15 at 12:03
• Then, why is the Axiom Schema of Abstraction ($(\forall \psi (x) \exists y \forall a)(a \in y \iff \psi (a))$) replaced by a the Axiom Schema of Separation, when it could only be extended to saying that the property $\psi (x)$ cannot refer to the set being constructed? – Jonathan Ginsburg Oct 9 '15 at 7:34
• Sorry for being so ignorant in this topic and thanks for your answer. – Jonathan Ginsburg Oct 9 '15 at 7:35
• I didn't say that naive comprehension could be rescued by adding that proviso alone. E.g. naive comprehension under the proviso still leaves Russell's paradox. By the way, note that putting a quantification over properties as you do makes the statement no longer a first-order schema but a second-order formula. – mmw Oct 9 '15 at 10:44