5 ms·

> On the other hand, I've not seen a rigorous set of axioms for category theory that didn't presuppose a notion of set or category or "collection". I'm no expe

by Twisol 4y ago

> On the other hand, I've not seen a rigorous set of axioms for category theory that didn't presuppose a notion of set or category or "collection". I'm no expert, but I do want to point out that you'll never see a set of axioms for set theory that doesn't also presuppose some realm from which sets themselves are drawn. The question is not whether sets exist; it's whether the collection of them can be represented within the theory. It is well-known (in certain circles...) that the realm of all sets cannot itself be described by a set. In the same way, category theory may assume the existence of collections of objects and arrows, but these collections are not themselves represented within category theory. The category of all categories encounters exactly the same size issues as does the set of all sets. There are different ways around these size issues. I think a lot of people go with something like Russell's stratified hierarchy of universes -- but this is also done in set theory, like with the alternative to ZFC based on sets and classes. (But what is the class of all classes!? You just keep building bigger universes.)

lmm 4y ago
> I'm no expert, but I do want to point out that you'll never see a set of axioms for set theory that doesn't also presuppose some realm from which sets themselves are drawn. Huh? Of course you do; ZFC itself is such a set of axioms. There's no particular requirement on objects that can be members of sets (at least, nothing really goes wrong if they're not all sets), so the theory doesn't depend on anything else, in a very intuitive sense.
- Twisol 4y ago
  To get a little bit technical, the axioms of ZFC, as a "first-order theory", make use of universal and existential quantifiers. These quantifiers have to quantify over some universe, whose constituents we call "sets". Take the axiom of the empty set as an example: exists x. forall y. y not in x The meaning of the "exists" quantifier is that it runs over the universe of entities; the formula it quantifies over must be true when instantiated on at least one such entity. The meaning of the "forall" quantifier is similar, except it must be true for every such instantiation. Notably, since the universe of all sets is not a set on pain of paradox, the universe itself cannot be a set. It is a primitive "sort", part of the logical signature of the theory. These quantifiers only "work" when there's a universe of entities to run over. This universe is not internal to set theory as an axiomatic system; the whole point of "non-standard models" is that we're looking for universes where the axioms of set theory hold, and yet are not what we normally think of when we reason using those axioms (e.g. "large cardinal" models). Category theory can also be framed as a first-order theory. In its most common incarnation, it's a two-sorted first-order theory, with separate universes for objects and for arrows. This isn't essential; we can actually dispense with objects and work only with arrows. (Objects are then encoded as their identity arrows.) But it's a first-order theory either way; all the axioms of a category can be given with quantified formulas. Group theory is also a first-order theory. When you specify a particular group, you give the universe over which its axioms quantify, and then prove(!) that those axioms hold on that universe. If you interpret group theory internal to set theory, then your universe will be a set; but the axioms don't care as long as quantification can be interpreted appropriately.
  - lmm 4y ago
    The idea that you can do category theory over any kind of thing as an arrow may be true as a matter of formal mathematical logic, but it's very much not intuitive in the way that it is for sets. If we wanted to work with tables, chairs, and beer mugs, it's very natural and easy to think about forming sets of beer mugs - a beer mug might either be a member of a set, or not, and this doesn't seem to require anything of it. For a group you need a binary operation and inverses, so this feels a bit more complex and abstract than a set (indeed the way I was taught, a group is a set plus some additional structure), but it's still fairly direct and understandable what kind of things satisfy the group axioms (if I had some rule for merging two beer mugs, and some kind of inverse - obviously this is unphysical, but it's at least imagineable). Whereas for a category it's just impossible to get started - should my beer mugs be objects or arrows? Presumably objects (since beer mugs are objects in the conventional sense), but then what are the arrows?
    - drdeca 4y ago
      What kind of relationships between beer mugs are you interested in? "can contain more beer than"? "is both at least as deep and at least as wide"? What about beer mugs are you trying to model?
      - lmm 4y ago
        I'm not trying to model anything about beer mugs. I'm trying to construct some nontrivial, intuitively understandable categories to play around with.
        Twisol 4y ago
        I like to take example categories from order theory, like with lattices and preorders and such. All such orders are also categories; the objects are the elements of the order, and the arrows are the relationships. However, if x <= y in the order, then there's only one arrow x -> y -- the order doesn't distinguish the different ways two objects can be related, only the mere fact that they are. (This is the difference between an order and a category: categories do allow us to distinguish the multiple ways two things can be related.) Lots of category theory has direct analogues in order theory. Functors are monotone functions, for instance; monads are closure operators; and presheafs are lower sets. But since there's at most one arrow between any two objects, you don't have to worry about all the coherence conditions you end up seeing in category theory. Their whole purpose is to make sure that you pick "the right" arrow in various circumstances; but when there's only one arrow, it is trivially the right one.

by Twisol 4y ago

lmm 4y ago

> I'm no expert, but I do want to point out that you'll never see a set of axioms for set theory that doesn't also presuppose some realm from which sets themselves are drawn. Huh? Of course you do; ZFC itself is such a set of axioms. There's no particular requirement on objects that can be members of sets (at least, nothing really goes wrong if they're not all sets), so the theory doesn't depend on anything else, in a very intuitive sense.

Twisol 4y ago
To get a little bit technical, the axioms of ZFC, as a "first-order theory", make use of universal and existential quantifiers. These quantifiers have to quantify over some universe, whose constituents we call "sets". Take the axiom of the empty set as an example: exists x. forall y. y not in x The meaning of the "exists" quantifier is that it runs over the universe of entities; the formula it quantifies over must be true when instantiated on at least one such entity. The meaning of the "forall" quantifier is similar, except it must be true for every such instantiation. Notably, since the universe of all sets is not a set on pain of paradox, the universe itself cannot be a set. It is a primitive "sort", part of the logical signature of the theory. These quantifiers only "work" when there's a universe of entities to run over. This universe is not internal to set theory as an axiomatic system; the whole point of "non-standard models" is that we're looking for universes where the axioms of set theory hold, and yet are not what we normally think of when we reason using those axioms (e.g. "large cardinal" models). Category theory can also be framed as a first-order theory. In its most common incarnation, it's a two-sorted first-order theory, with separate universes for objects and for arrows. This isn't essential; we can actually dispense with objects and work only with arrows. (Objects are then encoded as their identity arrows.) But it's a first-order theory either way; all the axioms of a category can be given with quantified formulas. Group theory is also a first-order theory. When you specify a particular group, you give the universe over which its axioms quantify, and then prove(!) that those axioms hold on that universe. If you interpret group theory internal to set theory, then your universe will be a set; but the axioms don't care as long as quantification can be interpreted appropriately.
- lmm 4y ago
  The idea that you can do category theory over any kind of thing as an arrow may be true as a matter of formal mathematical logic, but it's very much not intuitive in the way that it is for sets. If we wanted to work with tables, chairs, and beer mugs, it's very natural and easy to think about forming sets of beer mugs - a beer mug might either be a member of a set, or not, and this doesn't seem to require anything of it. For a group you need a binary operation and inverses, so this feels a bit more complex and abstract than a set (indeed the way I was taught, a group is a set plus some additional structure), but it's still fairly direct and understandable what kind of things satisfy the group axioms (if I had some rule for merging two beer mugs, and some kind of inverse - obviously this is unphysical, but it's at least imagineable). Whereas for a category it's just impossible to get started - should my beer mugs be objects or arrows? Presumably objects (since beer mugs are objects in the conventional sense), but then what are the arrows?
  - drdeca 4y ago
    What kind of relationships between beer mugs are you interested in? "can contain more beer than"? "is both at least as deep and at least as wide"? What about beer mugs are you trying to model?
    - lmm 4y ago
      I'm not trying to model anything about beer mugs. I'm trying to construct some nontrivial, intuitively understandable categories to play around with.
      - Twisol 4y ago
        I like to take example categories from order theory, like with lattices and preorders and such. All such orders are also categories; the objects are the elements of the order, and the arrows are the relationships. However, if x <= y in the order, then there's only one arrow x -> y -- the order doesn't distinguish the different ways two objects can be related, only the mere fact that they are. (This is the difference between an order and a category: categories do allow us to distinguish the multiple ways two things can be related.) Lots of category theory has direct analogues in order theory. Functors are monotone functions, for instance; monads are closure operators; and presheafs are lower sets. But since there's at most one arrow between any two objects, you don't have to worry about all the coherence conditions you end up seeing in category theory. Their whole purpose is to make sure that you pick "the right" arrow in various circumstances; but when there's only one arrow, it is trivially the right one.