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.
I think you're taking this point a little too forcefully; this is meant to informally motivate Russell's paradox, in my reading - which is exactly the title of the section you're referencing.
The point here is a little more subtle; category theory doesn't necessarily rely on sets; the definitions of categories that you often see (involving sets of objects and sets of morphisms) is more axiomatically forceful than the more general definition, which uses the notion of classes; category theory can use set theory, but does not depend on it.
The point here is that type theory offers just such another way to design in an avoidance of Russell's paradox.
You might also want to read about e.g. Grothendieck universes - they're quite relevant here.
> Yes -- in set theory sets can contain themselves
Which set theory? ZFC doesn't permit this.
Non-well-founded set theories are so non-standard that I think it's wrong, or at least misleading, to claim that unqualified "set theory" permits this.
to justify my claim with an excerpt from the article:
““
What is type theory
“Every propositional function φ(x)—so it is contended—has, in addition to its range of truth, a range of significance, i.e. a range within which x must lie if φ(x) is to be a proposition at all, whether true or false. This is the first point in the theory of types; the second point is that ranges of significance form types, i.e. if x belongs to the range of significance of φ(x), then there is a class of objects, the type of x, all of which must also belong to the range of significance of φ(x)” — Bertrand Russell - Principles of Mathematics
In the last section, we almost fell in the trap of explaining types as something that are “like sets, but… “ (e.g. they are like sets, but a term can only be a member of one type). However, while it may be technically true, any such explanation would not be at all appropriate, as, while types started as alternative to sets, they actually ended up being quite different. So, thinking in terms of sets won’t get you far. Indeed, if we take the proverbial set theorist from the previous section, and ask them about types, their truthful response would have to be:
“Have you seen a set? Well, it has nothing to do with it.” [<=== important bit]
So let’s see how we define a type theory in its own right.
””
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.
Why is it ill-defined? As you said, there's no contradiction.
Also, in the usual ZF set theory, it's empty.
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.
... and, as such, it doesn't contain itself!
> a set can contain itself
Can 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...
The system works according to its defined rules.
In one system, a set can contain itself, in another system it can't.
So it doesn't really make sense to ask 'can it?'
If you allow sets to contain themselves, you also have to talk about sets which do not contain themselves, which yields Russell's paradox.
If you disallow sets (or types) from containing themselves then you can't construct Russell's paradox, which is why it follows.
I think you're taking this point a little too forcefully; this is meant to informally motivate Russell's paradox, in my reading - which is exactly the title of the section you're referencing.
The point here is a little more subtle; category theory doesn't necessarily rely on sets; the definitions of categories that you often see (involving sets of objects and sets of morphisms) is more axiomatically forceful than the more general definition, which uses the notion of classes; category theory can use set theory, but does not depend on it.
The point here is that type theory offers just such another way to design in an avoidance of Russell's paradox.
You might also want to read about e.g. Grothendieck universes - they're quite relevant here.
The set of all sets that contain itself ;)
Except such set is empty and thus does not contain itself.
> > a set can contain itself
> Can it?
Yes -- in set theory sets can contain themselves
> > a term can have only one type... Due to this law, types cannot contain themselves
> Doesn't look like one follows from the other...
types are not sets and sets are not types therefore it makes no sense to link these two statements/judgements in the way you are linking them
> Yes -- in set theory sets can contain themselves
Which set theory? ZFC doesn't permit this.
Non-well-founded set theories are so non-standard that I think it's wrong, or at least misleading, to claim that unqualified "set theory" permits this.
TFA is right. Parent comment is not really rebutting in any meaningful way. Your rebuttal makes less sense.
>> "a term can have only one type... Due to this law, types cannot contain themselves"
> types are not sets and sets are not types therefore it makes no sense to link these two statements/judgements in the way you are linking them
to justify my claim with an excerpt from the article:
““ What is type theory
In the last section, we almost fell in the trap of explaining types as something that are “like sets, but… “ (e.g. they are like sets, but a term can only be a member of one type). However, while it may be technically true, any such explanation would not be at all appropriate, as, while types started as alternative to sets, they actually ended up being quite different. So, thinking in terms of sets won’t get you far. Indeed, if we take the proverbial set theorist from the previous section, and ask them about types, their truthful response would have to be: So let’s see how we define a type theory in its own right. ””Oof. If sets and types aren't the same, then sets and barbers are definitely not the same!