Axiom Schema of Separation in ZF and phrasing Russel's Property

Question

I am reading Jech's "Set Theory" and I got into troubles at page 4 (doh...). Here there is the framework with the question.

The next is the definition of an (axiom) schema of Naive Set Theory that is proved to be false via what is known as Russell's Paradox.

Axiom Schema of Comprehension: If $P$ is a property, then there exists a set $Y := \{ x : P(x)\}$.

Jech writes:

"The safe way to eliminate paradoxes of this type is to abandon the Schema of Comprehension and keep its weak version, the Schema of Separation:

If $P$ is a property, then for any $X$ there exists a set $Y =\{ x \in X : P(x) \}$."

Then he goes on to write:

"Once we give up the full Comprehension Schema, Russell’s Paradox is no longer a threat; moreover, it provides this useful information: The set of all sets does not exist."

These last two statements are the ones that I do not really get. Below my questions.

---

QUESTION:

I always thought that the problem of Naive Set Theory comes from the lack of an hierarchy of sets. By replacing Comprehension with Separation and defining $P(x)$ as the property of not being a member of itself, we can still write something like $X \notin X$. The thing is that I do not really understand this expression, i.e., I thought that essentially it is not allowed (does not make any sense) to write such an expression in ZF.

Hence, what am I missing?

[Mind that I found this vary nice answer by Asaf Karagila to a previous question where – at the end – Russell's paradox is seen as a theorem. I know and understand that once we accept ZF the paradox becomes (has to) a theorem: the problem is I don't think I actually understand how we can still phrase this theorem in ZF]

Any feedback will be more than welcome.

Thank you for your time.

PS: In the title I write "Russell's property" exactly because that is my problem (and the paradox obtained via that property becomes a theorem in ZF).

Answer 1

The universe of sets described by ZF only has one type of object, and membership is a binary relation on this type of object.

If $X$ denotes a set, there is nothing disallowing you from writing $X \notin X$; it is a perfectly meaningful predicate. (and always true, due to the axiom of foundation)

---

Your exposition gives me the impression that you are thinking of higher order logic (HOL), which does indeed stratify the types, and requires that the left argument to $\in$ have strictly lower order than the right argument (and thus you cannot write $X \notin X$).

Answer 2

It doesn't matter if you can still writte $X\not\in X$, the important thing is that the axiom of separation does not allow you to say that $\{X|X\not\in X\}$ is a set, it tells you that if you want to transform a predicate into a set you need an upper bound for that set, i.e a set $A$ (you must already know $A$ is a set) containing it. In other words, it tells you that given a set $A$ any predicate defines a subset of that set.
For instance you can say that $\{x\in \mathbb{N}\ |\ x\not\in x\}$ is a set and that does not lead you to a contradiction.