Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: category theory

Topic: Algebraic set theory

Julius Hamilton (May 26 2024 at 16:43):

This is a side-question from a different thread.

It’s more of an invitation to a discussion than a question.

It seems that [[algebraic set theory]] pursues certain goals that I find of prime interest.

Namely, there are many different set theories, but perhaps that is a way to define “a set theory” in a way that finds the commonality between all of them.

I have only two small questions to hopefully initiate a conversation.

1. There are so many formal systems one can choose to work in - homotopy type theory, Zermelo-Fraenkel set theory, lambda calculus, etc. Are there examples of people using algebraic set theory as the formalism in which they develop a mathematical theory in?

2. I heard that an elementary topos can be seen as an abstraction of the category of sets. Does algebraic set theory necessarily make use of topos theory?

Thanks.

Todd Trimble (May 26 2024 at 18:54):

There are so many formal systems one can choose to work in - homotopy type theory, Zermelo-Fraenkel set theory, lambda calculus, etc. Are there examples of people using algebraic set theory as the formalism in which they develop a mathematical theory in?

Not really as such, as far as I know.

Either algebraic set theory or ZFC could function something like a "machine language" in which the referents of a theory are encoded, and if one is super-serious about fully formal mathematics, one could attempt to work with ZFC or GBN or MK or whatever at a foundational level, and build up a library of results from the bedrock there. I think I've heard that something like this is the basis of Mizar, for example. But if you take a textbook on some random mathematical theory, like the theory of several complex variables say, then you'll never find any such set theory invoked at a formal level. You might find some lip service, or some preliminary discussion at the level of "naive set theory" in some cases, but that's about it.

Todd Trimble (May 26 2024 at 18:54):

Does algebraic set theory necessarily make use of topos theory?

I'd say "not really". It does make substantial use of category theory. Closer to the point, it does make use of pretopos theory, which has features in common with topos theory, except that you don't have "function space objects" like you do in topos theory. Basically, in algebraic set theory, one wants to discuss categories of classes (thinking here of a class/set distinction), where you can manipulate classes with first-order logic operations but not higher-order operations, such as attempting to take the class of all functions from one class to another. Pretopos theory gives you the first-order fragment of topos theory, roughly speaking.

But I'll go on to say that I would not recommend any of this as part of a pedagogical program to learn mathematics from the ground up. I would have to regard it as way too hard and way too niche to be any sort of entry-level subject.

John Onstead (May 26 2024 at 19:34):

Algebraic set theory sounds interesting, but I'm not sure how well-founded it is. For instance, the nlab page cites "Instead of focusing on categories of sets AST focuses on categories of classes." But this is impossible by the very definition of a class! If you recall, a class is defined to be a collection of things that can't be an element of another collection of things. But if you were to somehow have a category of classes C, then you'd also have a class Ob(C) whose elements are not only other classes, but all classes! That shouldn't be possible!

Todd Trimble (May 26 2024 at 19:51):

@John Onstead You should check out NBG for example, where classes are part of the object language.

Todd Trimble (May 26 2024 at 19:54):

(What's that quote? “There are more things in heaven and earth, Horatio, than are dreamt of in your philosophy.”)

Todd Trimble (May 26 2024 at 21:16):

But seriously, on occasions when I want to go outside the confines of ordinary ZFC (because I want to consider, for example, functor categories between "large" categories), I often adopt "Mac Lane foundations" and posit a single strongly inaccessible cardinal $\alpha$ in my model of set theory. Sets of cardinality less than $\alpha$ are then called "small sets", and otherwise we can just say "sets". The category of small sets, let's call it $\mathrm{set}$, well you could call it a "large" category if you want, but in this framework it has a set of morphisms -- just not a small set of morphisms -- and the functor category construction for categories as structures interpreted within this model can be performed with impunity, so that we can speak of for example $\mathrm{set}^\mathrm{set}$ and $\mathrm{set}^{(\mathrm{set}^\mathrm{set})}$ and so on. This maneuver is a bit more dramatic than what is furnished by NBG, but from the viewpoint of professional set theorists, it would be considered just about the most piddlingly small "large cardinal hypothesis".

John Onstead (May 26 2024 at 22:16):

This sounds like Grothendieck universes where we define a U-small set to be some set within a particular Grothendieck universe U. In this case, the universe U might in some way be related to the strongly inaccessible cardinal alpha- maybe it helps us build what this universe is. Then any set larger than this cardinal would not be in the U universe and so would be U-large sets. So in this case, a set, class, and Ob(C) for the category of those classes would all exist on different universes, each "larger" than the last.
Actually, I just re-checked the Grothendieck universe page on nlab and indeed here it does discuss this relationship!

Todd Trimble (May 26 2024 at 22:17):

Yes, this is exactly the idea.

James E Hanson (May 26 2024 at 22:38):

I don't really know the scope of what algebraic set theory talks about, but I think it's going to be hard to really write down a treatment of 'all set theories.'

Like with type theory, there really isn't a solid consensus regarding what 'a set theory' even is. Aside from the extremely broad notion of 'a set is a "collection" of objects,' I don't know if there are any absolute commonalities:

• There are set theories in which membership is not binary. Obviously there's constructive set theory, but then there's also $[0,1]$-valued set theory which has been studied in various forms for at least around 70 years at this point. People have also looked at set theories in the context of various sub-intuitionistic logics.
• There are many set theories without extensionality. In some cases because it's actually inconsistent with other principles that people are looking at (such as unrestricted comprehension in the context of $[0,1]$-valued Łukasiewicz logic). There's also double extension set theory, which I don't even really know how to characterize.
• There are obviously plenty of set theories with atoms, such as $\mathsf{ZFA}$, $\mathsf{NFU}$, and $\mathsf{KPU}$, but there's also set theories like $\mathsf{ETCS}$ in which sets are not elements of other sets.
• There are set theories in which there are other kinds of compound objects. Obviously some set theories add classes as first-class objects, but there's other stuff too. One of Bourbaki's treatments of set theory took ordered pairs as primitives and in Randall Holmes's $\mathsf{NFU}$ set theory textbook he did the same.
• There are set theories where the induced category of sets in not particularly nice. Famously $\mathsf{NF}$-sets aren't cartesian closed (and I suspect this is true of $\mathsf{NFU}$ as well, but I'm not finding a reference at the moment), but there's also $\mathsf{GPK}^+_\infty$, where in natural models the lattice of sets looks like the lattice of closed subsets of a topological space, rather than the lattice of open sets, as is roughly the case in something like $\mathsf{IZF}$. There's even at least one paper about a set theory in which the partial order of subsets doesn't always have meets (although this is my fault).