6 ms·
Category Theory Illustrated – Types
- throwway262515 6mo ago[flagged]
- MORPHOICES 6mo ago[dead]
- layer8 6mo agoRegarding 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.
- xanderlewis 6mo agoWhy is it ill-defined? As you said, there's no contradiction. Also, in the usual ZF set theory, it's empty.
- Koshkin 6mo ago... and, as such, it doesn't contain itself!
- layer8 6mo agoIt’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.
- jesuslop 6mo agoI think "Foundation" axiom F forbids your recursive set, and there are models of both core set theory satisfying either F or ¬F, so F is independent of core set theory (core -> not including F or ¬F). F is normally assumed in set theory, but Aczel has worked with "ill" founded (¬F) set theory models. Just as with the axiom of choice. No religion wars, just people pushed to be explicit with assumptions.
- Koshkin 6mo ago> 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...
- bombcar 6mo agoThe set of all sets that contain itself ;)
- Koshkin 6mo agoExcept such set is empty and thus does not contain itself.
- impact-basin 6mo agoI 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.
- Koshkin 5mo ago> category theory can use set theory, but does not depend on it But aren't, say, the morphisms between two objects necessarily a set (termed "hom-set")?
- igravious 6mo ago> > 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
- ece 6mo agoReminded me of this veritasium video: https://youtu.be/_cr46G2K5Fo?si=0MfbE8c99sUckT03 https://youtu.be/_cr46G2K5Fo?si=0MfbE8c99sUckT03
- chromacity 6mo agoIt'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.
- deleted 6mo ago[deleted]