How to avoid a Russell-style paradox in ZF?
The Zermelo-Fraenkel system, by not using a theory of types, does not prevent us from posing Russell's paradoxical scheme. Only when the argument is replaced by the set being defined, the resulting statement is false, not paradoxical.
Set R in Frege's system:
By the axiom of unrestricted comprehension:
∃y ∀x ( x ∈ y ) ⟺ F(x)
... where F (x) is any well-formed formula of the system. Replacing the formula, and the existential by the name of the defined set:
∀x ( x ∈ R ) ⟺ ( x ∉ x )
Instantiating the variable x with R:
( R ∈ R ) ⟺ ( R ∉ R )
Set R in the ZF system:
By the axiom of specification (also called separation):
∀z ∃y ∀x [ ( x ∈ y ) ⇔ ( x ∈ z ) ∧ F(x) ]
Replacing the schema of the formula with a concrete formula, and the existential one with the name of the defined set:
|1|: ∀z ∀x [ ( x ∈ R ) ⟺ ( x ∈ z ) ∧ ( x ∉ x ) ]
We cannot replace x by R, because there is no set z of which it is a member, therefore the second member of the equivalence does not hold.
The ZF system also allows defining the R’s complement independently, that is, without using the set R in its definition, but simply as the set M of all self-belonging sets, those that are members of themselves.
∀z ∀x [ ( x ∈ M ) ⟺ ( x ∈ z ) ∧ ( x ∈ x ) ]
Then you can build the complement of M, which is the complement of the complement of R, without in principle its double complement condition being evident:
∀z ∀x [ ( x ∈ MC ) ⟺ ( x ∈ z ) ∧ ( x ∉ M ) ]
Then instantiating in the formula |1|:
∀z [ ( MC ∈ R ) ⟺ ( MC ∈ z ) ∧ ( MC ∉ MC ) ]
But MC is the complement of the complement of R, so that it can be shown that:
( MC ⊆ R ∧ R ⊆ MC ) ⟹ ( R ≡ MC )
That is, MC and R are two names for the same set; thus:
∀z [ ( R ∈ R ) ⟺ ( R ∈ z ) ∧ ( R ∉ R ) ]
If we assume that R ∈ R, then:
( R ∈ R ) ⟹ ∀z ( R ∈ z ) ∧ ( R ∉ R ) ∀z ( R ∈ z ) ∧ ( R ∉ R ) [ by Modus Ponens ] ( R ∉ R ) [ conjunction elimination ]
If we assume that R ∉ R, then:
∀z ( R ∈ z ) ∧ ( R ∉ R ) ⟹ ( R ∈ R )
If we suppose that R is a member of all sets it is easily followed that it is a member of itself, by Modus Ponens.
If we assume that R is not a member of some set, R would not be defined, contrary to what we had assumed in the formula |1|.
For all of which:
( R ∈ R ) ⟺ ( R ∉ R )
I assume there will be a way to disprove this reasoning, but at the moment I can't get a glimpse of it.
[![Explanation of W.v.O. Quine, about the axiom scheme][1]](https://i.stack.imgur.com/OqDjF.png)
This is a nice example of the subtlety of existential instantiation (replacing an existentially-quantified variable with a constant symbol). Specifically:
You cannot instantiate while bound by a universal quantifier.
To see what I mean, consider the following. The sentence $$\forall u\exists v(u<v)$$ is obviously true in $\mathbb{N}$. However, if we try to instantiate $v$, we get $$\forall u(u<C)$$ (here "$C$" is our new constant symbol) which is clearly false in $\mathbb{N}$ no matter how we interpret $C$.
In your argument, this is exactly what you do e.g. when you write
the sentence "$\forall z\color{red}{\exists y}\forall x[x\in \color{red}{y}\leftrightarrow (x\in z\wedge x\not\in x)]$" is provable from separation but the sentence "$\forall z\forall x[x\in \color{red}{R}\leftrightarrow (x\in z\wedge x\not\in x)]$" is completely unjustified, and indeed $\mathsf{ZF}$ disproves the existence of an $R$ having that property.
There is a way to correctly instantiate inside a universal quantifier: introduce a function symbol taking as input the variables corresponding to universal quantifiers outside the relevant existential quantifier. Thinking of constant symbols as $0$-ary function symbols, this generalizes the version of existential instantiation we're used to in the case where there are no "outside universals."
This transformation is actually extremely useful - it's Skolemization. But that doesn't lead to a contradiction here: we just wind up building the function $z\mapsto \{x\in z: x\not\in x\}$, which is in fact $z\mapsto z$ by regularity.