Consider the following demonstration whose first line is the assumption called the axiom of unrestricted comprehension.
- ∀F∃y ∀x[x ∈ y iff F(x)] [OSC1]
- ∀F∃y [α ∈ y iff F(α)] [UI]
- ∃y [α ∈ y iff α ∉ α] [UI]
- α ∈ x1 iff α ∉ α [EI]
The only way to get Russell's paradox is if alpha must be a general constant. But, in universal Instantiation, alpha is either a general constant or a specific constant. Therefore
- ∀x[x=α] ∨ ∃! x[x=α]
If ∀x[x=α] then you get Russell's paradox. But you aren't done, because line 5 is a disjunction, so
- ∃! x[x=α] [5; DS]
Thus alpha is a specific constant. If alpha equals x1 then you get Russell's paradox, so
x1 ≠ α
[α ∈ x1 iff α ∉ α] ∧ x1 ≠ α [4,7; conj]
∀F∃y[α ∈ y iff F(α) ∧ y ≠ α]
Since alpha is a specific constant you can't universally generalize on it, you can only existentially generalize on it.
- ∃x ∀F∃y[x ∈ y iff F(x) ∧ y ≠ x]
Closing the scope of the first assumption, line 1 implies line 10.
The point is, Russell's paradox is not a consequence of Gottlob Frege's axiom of unrestricted comprehension. This isn't surprising since Russell didn't understand the nuances of universal Instantiation in 1901. It wasn't until 1929 that Goedel proved the first order function calculus is complete, and I'm not sure if he knew the nuances of Universal Instantiation. In fact Leon Henkin's proof FOL is complete is the one I'm familiar with, and that proof came out in 1949. And it isn't clear to me that Henkin knew the nuances of Universal Instantiation either.
What do you think?