It's a great introduction, but I find the premise a bit funny. It starts with Russell's paradox, insinuates that solving it within set theory makes set theory complex (it doesn't, you basically just restrict what can be used to build a set), and then introduces a system that is fundamentally more complex.
Regarding Russell’s paradox, its dual is also interesting: Consider the set D := { s | s ∈ s }, the set of sets that do contain themselves. Does D contain itself? It might or it might not, neither causes a contradiction. Tnis shows that you don’t need an antinomy for a set comprehension to be ill-defined.
It’s ill-defined in the sense that it doesn’t uniquely define the set. There are at least two different sets that D could be (one containing it and one not containing it), hence the expression doesn’t denote a well-defined set. (*)
The axioms of ZF do not allow to form that expression, so the set doesn’t exist in ZF.
(*) This is from a universist view. In a pluralist view, one wouldn’t say that the fact of the matter of whether D contains itself or not is independent from naive set theory, and that there are set universes where it is the case and others where it isn’t. But I would hold that naive set theory starts from a universist view.
22 comments
Also, in the usual ZF set theory, it's empty.
The axioms of ZF do not allow to form that expression, so the set doesn’t exist in ZF.
(*) This is from a universist view. In a pluralist view, one wouldn’t say that the fact of the matter of whether D contains itself or not is independent from naive set theory, and that there are set universes where it is the case and others where it isn’t. But I would hold that naive set theory starts from a universist view.
>
a set can contain itselfCan it?
> a term can have only one type... Due to this law, types cannot contain themselves
Doesn't look like one follows from the other...