In chapter 1 § 5 of Set theory by Kenneth Kunen. Kunnen explains that a naive attempt for formalizing Axiom of Comprehension would look like $\exists y \forall x (x \in y \leftrightarrow \phi)$.
But the book claim it is incorrect because when we define $\phi$ as $x \notin x$ we can have the following deduction $\forall x (x \in y \leftrightarrow x \notin x)$,And when $x = y$ we get $(y \in y \leftrightarrow y \notin y)$.
So instead the book suggests the correct Axiom to be $\exists y \forall x (x \in y \leftrightarrow x \in z \wedge \phi)$.
But when I tried following the exact same step I ended up with $(y \in y \leftrightarrow y \in z \wedge y \notin y)$.
If $y \in z$ evaluated to true, we will end with the exact same predicate as with the naive Axiom of comprehension. I know that Russell's paradox should not work in ZF set theory, but I cannot figure out what is wrong with my reasoning.
Best Answer
I think there is a flaw in my my proof and when I tried to write the proof formally I think I was able to see why the paradox does not hold.
The proof is Gentzen style (which the book does not use) and it was the only way I was able to follow.
The Full Axiom of Comprehension says that: For each formula $\phi$ with free variables among $x, y, z, w_1, ..., w_n$ $$ \forall z \forall w_1, ..., w_n\exists y \forall x (x\in y \leftrightarrow x \in z \wedge \phi) $$
We assume $\phi$ is $x \notin x$ so we no longer need $w_1,....w_n$
The proof will look like following:
$$ \dfrac { \dfrac{ \dfrac{ \dfrac{ \dfrac{ \dfrac{}{z, x, x \in z \vdash x \in z \wedge x \notin x}\text{*} } {z, x \vdash (x\in z \rightarrow x \in z \wedge x \notin x)} ~~~~~~~ \dfrac{ \dfrac{}{z, x, x \in z, x \notin x \vdash x \in z}(assumptions)} {z, x \vdash x \in z \wedge x \notin x \rightarrow x \in z} (\text{introuce the hypothesis}) }{ z, x \vdash x\in z \leftrightarrow x \in z \wedge x \notin x }(\text{split equivalence})}{z \vdash \forall x (x\in z \leftrightarrow x \in z \wedge x \notin x)} ( \text{introduce } x) } {z \vdash \exists y \forall x (x\in y \leftrightarrow x \in z \wedge x \notin x)} (\text{exists }z) } {\vdash\forall z \exists y \forall x (x\in y \leftrightarrow x \in z \wedge x \notin x) } (\text{introduce } z) $$
The continuation of proof of
*is:1- Proving that $z, x, x \in z \vdash x \in z$ which is trivial by assumptions.
2- Proving that $z, x, x \in z \vdash x \notin x$. which is the same as $z, x, x \in z, x \in x \vdash false$. I struggled there for a bit but I learned that this is a direct consequence from Foundational Axiom which will be discussed later in chapter 3.