1
$\begingroup$

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).

$\endgroup$
  • 1
    $\begingroup$ See the proof of Russell's Paradox for an explanation of how it is engendered by Comprehension and how it is avoided by Separation. $\endgroup$ – Mauro ALLEGRANZA Feb 2 '18 at 11:08
  • 1
    $\begingroup$ If we assume that the set of all sets $V$ exists, we can apply Separation to it $\{ x \in V \mid x \notin x \}$ and we derive the contradiction. Thus, we use Reductio to conclude from the contradiction that the assumption that $V$ exists is unteneable. Conclusion: $V$ does not exist. $\endgroup$ – Mauro ALLEGRANZA Feb 2 '18 at 11:10
  • $\begingroup$ @MauroALLEGRANZA Thanks a lot for the reference, which is very nice! Now I have to metabolise it. However, I have a question concerning what I call Russel's Property, i.e., being not a member of itself. Can we say that the only occurrence of it is in Russel's result in the sense that it is a property that a fortiori leads there. Hence, yes, we can formulate it in ZF (from Hurkyl's answer), but it's not really interesting. [I am trying to deal with the discomfort I would feel by finding in a random paper/book something like $A \in A$, which just looks wrong (same with the negation)]. $\endgroup$ – Kolmin Feb 2 '18 at 12:25
  • 1
    $\begingroup$ The issue is: every "property" expressible with the resources of the language is Ok. Thus, also Russell's one: $x \notin x$, is. What is not right is the (previously "obvious") assumption that for every property there is a "collection" (i.e. set) of all and only those objects satisfying the property. $\endgroup$ – Mauro ALLEGRANZA Feb 2 '18 at 13:14
  • $\begingroup$ @MauroALLEGRANZA I think I start to see what's going on. Allow me to write down a comment I put under Hurkyl's answer which summarises my understanding. It is fine to write $X \in X$ in ZF, however this does not work with an hierarchy of types which – and this is the important point! – is actually independent of ZF. Still, this hierarchy (even if logically independent from ZF) is how we actually deal with set as mathematical objects in practice and that's why this looks wrong to the practitioner, but not to the set theorist! (Of course, feel free to correct me if something sounds wrong) $\endgroup$ – Kolmin Feb 3 '18 at 10:21
1
$\begingroup$

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$).

$\endgroup$
  • $\begingroup$ Thanks a lot for your answer! Concerning the very last paragraph, I think this does hit my problem. Thus – correct me if I got it wrong – essentially you are telling me that $X \in X$ is not wrong in ZF since we can actually write it but it does not work with an hierarchy of types which – and this is the important point – is actually independent of ZF. Still, this hierarchy (even if logically independent from ZF) is how we actually deal with set as mathematical objects in practice and that's why this looks wrong to the practitioner, but not to the set theorist! Hope I made myself clear. :-) $\endgroup$ – Kolmin Feb 2 '18 at 12:30
0
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.