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: community: our work

Topic: Type theory vs set theory


view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 03:01):

I gave a talk last Friday in which I began by considering set theory. There are two perspectives on what set theory does. The first [more correct one] is that it's hard to give a convincing example of any mathematical concept that clearly sits outside of the comfort zone of being foundable in set theory. The second [naïve] one is that students in a typical intro to proofs course are taught set theory and then learn concepts such as functions and families and then go on to do math with these concepts, so one might think that set theory is an optimal framework for discussing such concepts

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 03:02):

The talk was titled "diagram models", and the first example that I considered was taking a model of set theory [whatever that means] and replacing it with the model in which every object now denotes a pair of sets, i.e. the model Set × Set

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 03:04):

After some discussion, the first observation made was that this "model" violates LEM. However, even if we work in a constructive set theory, I still think that this model violates extensionality, for any meaningful way that I can think of formulating extensionality with a global membership ∈ operation

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 03:05):

However, all of the basic concepts of functions and families [i.e. pi-types and universes] make sense equally well in a diagram model

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 03:06):

I then argued that type theory is the optimal framework for studying concepts like functions and families in maximal generality, such that if at any point in the future you have an idea for a new model, you automatically get All Of Mathematics Ever Written Down In Type Theory for free

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 03:09):

v.s. in set theory, it would be hard to make the case that you could not give the construction of what is meant by the structure of such a model, viz. defining what is meant by a pair of sets and what it means to be a morphism between such pairs, but you would have to manually rewrite all of the mathematics that you wanted to port to this setting as it would not be an actual semantic model of the syntax of set theory

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 03:13):

This was the intro and the rest of the talk was basically an elaboration of the concept of a Category With Families

view this post on Zulip Notification Bot (Dec 05 2023 at 04:26):

7 messages were moved here from #community: our work > Mike Shulman by Mike Shulman.

view this post on Zulip Mike Shulman (Dec 05 2023 at 04:28):

Interesting. My first question is in what sense the "model" of pairs of sets violates LEM? The topos Set×Set\rm Set\times Set is Boolean, so it satisfies LEM.

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 04:53):

We can consider a multi-modal theory whose diagram mode interprets into Set×Set\mathsf{Set} \times \mathsf{Set} and that has modalities 0\lozenge_0 and 1\lozenge_1 that land in the discrete mode. I want to say that assuming LEM as an axiom (i.e. in the global context) in the diagram mode implies contradiction in the discrete mode

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 04:54):

Consider X=(,)X = (\top, \bot)

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 04:57):

If we have  bmX \ \vdash_{bm} X \to \bot\ then  dm0X0\ \vdash_{dm} \lozenge_0 X \to \lozenge_0\bot, or equivalently  dm\ \vdash_{dm} \top \to \bot, conversely given bmX\vdash_{bm} X we get  dm1X\ \vdash_{dm} \lozenge_1 X or  dm\ \vdash_{dm} \bot. This is not an anti-classical result, but it shows that LEM cannot hold in an arbitrary context

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 05:00):

This is just an extended way of saying that there is a diamond of four truth values

view this post on Zulip Mike Shulman (Dec 05 2023 at 05:03):

No, it doesn't show that LEM can't hold. It shows that XX doesn't hold in an empty context, and that ¬X\neg X doesn't hold in an empty context, but it doesn't show that X+¬XX+\neg X can't hold in an empty context. And in fact if you work it out you can see that X+¬X(,)X+\neg X \cong (\top,\top).

view this post on Zulip Mike Shulman (Dec 05 2023 at 05:05):

This is the difference betweeen a topos being Boolean and being two-valued. A Boolean topos is one whose subobject lattices are Boolean algebras; they could have lots of different elements, but as long as they are Boolean algebras, it holds in the internal logic of the topos that "every truth value is either true or false" because for every proposition PP the proposition P¬PP\vee \neg P is equal to \top, even if PP itself is neither equal to \top nor \bot.

view this post on Zulip Mike Shulman (Dec 05 2023 at 05:07):

A two-valued topos is one with exactly two subterminal objects. This is incomparable to Booleanness in general: a topos can be Boolean without being two-valued, or two-valued without being Boolean.

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 05:07):

Oh, this is a good point. LEM would fail in Set\mathsf{Set}^\to, though, right?

view this post on Zulip Mike Shulman (Dec 05 2023 at 05:09):

Yes, LEM fails in Set\rm Set^\to, because there you have a truth value U=(01)U = (0\to 1) such that U¬U\neg \top, but ¬U=\neg U = \bot, so U¬U=UU\vee \neg U = U \neq \top.

view this post on Zulip Mike Shulman (Dec 05 2023 at 05:11):

Next question is how you were thinking of formulating extensionality. (-: One can build a model of set theory internal to any topos as well, with extensionality along with the other axioms. And in Set×Set\rm Set \times Set I think it will just result in pairs of ordinary sets.

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 05:13):

I saw that in the HoTT book there is a construction of such a model V with a membership predicate \in as a HIT, however a global extensionality axiom in the theory shouldn't be about a specific set of symbol meanings that you can construct

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 05:14):

On the other hand, there isn't really a natural interpretation of what \in means in type theory, is there?

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 05:16):

Or at least, it is wrong to interpret elements as global elements

view this post on Zulip Mike Shulman (Dec 05 2023 at 05:18):

Right, type theory doesn't have a global \in. But that's a different thing from saying that extensionality is violated; by the latter I would understand that you have fixed a meaning of \in and the resulting interpretation of the statement xy,((z.(zxzy))x=y)\forall x y, ((\forall z. (z\in x \leftrightarrow z\in y))\to x=y) is false.

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 05:22):

I guess that the original question is whether you could interpret every statement written in set theory as saying something about Set×Set\mathsf{Set} \times \mathsf{Set}

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 05:23):

What this would mean is secretly replacing every set with a pair of sets and every function with a pair of functions, as opposed to interpreting this inside of an inner model of set theory that could be constructed inside of Set×Set\mathsf{Set} \times \mathsf{Set}

view this post on Zulip Mike Shulman (Dec 05 2023 at 05:23):

I think in the case of Set×Set\rm Set\times Set you could probably do that because it's so simple.

view this post on Zulip Mike Shulman (Dec 05 2023 at 05:24):

And I think that would end up coinciding with the model of set theory constructed in the usual way inside the topos Set×Set\rm Set\times Set, just because everything you do in Set×Set\rm Set\times Set is "componentwise".

view this post on Zulip Mike Shulman (Dec 05 2023 at 05:25):

In particular, the truth value of (x0,x1)(y0,y1)(x_0, x_1) \in (y_0, y_1) would be (x0y0,x1y1)(x_0\in y_0, x_1\in y_1).

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 05:28):

Hmm, my intuitions probably came from thinking of a model of set theory as being something that looked analogous to the categorical semantics of type theory. So every set gets interpreted as an object in the category and such that you can talk about Xt:YX \vdash t : Y

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 05:29):

On the other hand, if you start constructing a model instead by explaining what \in means, I think that you can effectively restrict to an inner construction of V in the topos

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 05:31):

Having judgments in a context as being primitive is what I meant by "replacing every function with a pair of functions"

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 05:32):

It still feels to me that something is lost from the richness of Set×Set\mathsf{Set} \times \mathsf{Set} if you start with \in. What do you think about this?

view this post on Zulip Mike Shulman (Dec 05 2023 at 05:32):

Set theory as usually formulated doesn't have a notion of "term", so if you're building a model of set theory you shouldn't expect to be able to talk about Xt:YX\vdash t:Y. The fundamental structure of (membership-based) set theory is the predicate \in.

view this post on Zulip Mike Shulman (Dec 05 2023 at 05:34):

Obviously I'm not a real big fan of membership-based set theory myself for other reasons, but at a technical level I think it does capture basically all the internal logic of a topos when formulated carefully.

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 05:36):

Could Set\mathsf{Set}^\to be made into a model of constructive set theory?

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 05:40):

Astra Kolomatskaia said:

It still feels to me that something is lost from the richness of Set×Set\mathsf{Set} \times \mathsf{Set} if you start with \in. What do you think about this?

I think my intuition here is that pi-types and universes in the membership based model don't coincide with their type theoretic counterparts

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 05:41):

For pi-types, this is clear because the intro rule uses terms in a context, which we just don't have as a primitive notion

view this post on Zulip Mike Shulman (Dec 05 2023 at 05:43):

Well, when you're working in set theory, you define "pi-types" differently:

Π(A,B)={f:AaAB(a)  |  a,f(a)B(a)}.\Pi(A,B) = \left\{ f : A \to \bigcup_{a\in A} B(a) \;\middle|\; \forall a, f(a) \in B(a) \right\}.

view this post on Zulip Mike Shulman (Dec 05 2023 at 05:44):

They're characterized differently, because as you say set theory doesn't have the machinery to give type-theoretic intro/elim rules, but they turn out to be equivalent semantically.

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 05:45):

I guess that they might actually be pi-types if you derive Xt:YX \vdash t : Y as being defined in terms of \in

view this post on Zulip Madeleine Birchfield (Dec 05 2023 at 05:46):

Mike Shulman said:

Well, when you're working in set theory, you define "pi-types" differently:

Π(A,B)={f:AaAB(a)  |  a,f(a)B(a)}.\Pi(A,B) = \left\{ f : A \to \bigcup_{a\in A} B(a) \;\middle|\; \forall a, f(a) \in B(a) \right\}.

On a side note, is that how one would define dependent products in ETCS or SEAR as well?

view this post on Zulip Mike Shulman (Dec 05 2023 at 05:46):

Astra Kolomatskaia said:

Could Set\mathsf{Set}^\to be made into a model of constructive set theory?

A model of constructive set theory can be constructed from any topos. The HIT construction in the HoTT Book is a highbrow approach, but the more traditional one is to consider internal well-founded relations. This dates back to Cole, Mitchell, and Osius in the mid-20th century; I wrote a paper myself that does some systematization and comparison to category theoretic axiom systems.

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 05:47):

That makes sense

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 05:48):

Astra Kolomatskaia said:

I guess that they might actually be pi-types if you derive Xt:YX \vdash t : Y as being defined in terms of \in

Specifically XYtypeX \vdash Y \mathsf{type} means YY is a family of sets over the elements of XX and tt means a dependent function, defined set theoretically

view this post on Zulip Mike Shulman (Dec 05 2023 at 05:49):

The main limitation is that these straightforward constructions don't always "see" the whole topos: they only see the part that can be equipped with well-founded relations. In a classical topos this is all of it, but in a constructive topos it could miss part. But there's a fancier approach due to Awodey, Butz, Simpson, and Streicher that is able to "see" the whole topos.

view this post on Zulip Mike Shulman (Dec 05 2023 at 05:49):

Astra Kolomatskaia said:

Specifically XYtypeX \vdash Y \mathsf{type} means YY is a family of sets over the elements of XX and tt means a dependent function, defined set theoretically

Right: you basically start from your model of set theory and build a model of type theory in the usual way.

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 05:50):

Mike Shulman said:

The main limitation is that these straightforward constructions don't always "see" the whole topos: they only see the part that can be equipped with well-founded relations. In a classical topos this is all of it, but in a constructive topos it could miss part. But there's a fancier approach due to Awodey, Butz, Simpson, and Streicher that is able to "see" the whole topos.

So, for example, extensionality would say that (,)=(,)(\top,\bot) = (\bot,\bot), right?

view this post on Zulip Mike Shulman (Dec 05 2023 at 05:50):

Madeleine Birchfield said:

On a side note, is that how one would define dependent products in ETCS or SEAR as well?

Not exactly, because ETCS and SEAR don't have a notion of non-disjoint union. But you can do something similar using a disjoint union.

view this post on Zulip Mike Shulman (Dec 05 2023 at 05:51):

Astra Kolomatskaia said:

So, for example, extensionality would say that (,)=(,)(\top,\bot) = (\bot,\bot), right?

No. (,)(\top,\bot) has no global elements, but that doesn't mean that z,(z(,)z(,))\forall z, (z\in (\top,\bot) \leftrightarrow z\in (\bot,\bot)) holds internally.

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 05:59):

What does the argument that 1 ( z. z(,)) z. z\lozenge_1~\big(\exists~z.~z \in (\top, \bot)\big) \equiv \exists~z.~z\in\bot say, if anything?

view this post on Zulip Mike Shulman (Dec 05 2023 at 06:06):

Well, it implies that z.z(,)\exists z. z\in (\top,\bot) has no global elements, since any such global element would also yield a global element of z.z\exists z. z\in \bot in Set\rm Set.

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 06:08):

Mike Shulman said:

No, it doesn't show that LEM can't hold. It shows that XX doesn't hold in an empty context, and that ¬X\neg X doesn't hold in an empty context, but it doesn't show that X+¬XX+\neg X can't hold in an empty context. And in fact if you work it out you can see that X+¬X(,)X+\neg X \cong (\top,\top).

I guess that the argument that I gave at the start breaks down in that its casework derives contradiction in dmdm by way of using different modalities, so there is no unified modal function like (p:LEM X)(p :^\lozenge \mathsf{LEM}~X) \to \bot

view this post on Zulip Mike Shulman (Dec 05 2023 at 06:13):

I would have said it breaks down because LEM doesn't satisfy canonicity. Postulating P.P+¬P\vdash \forall P. P+\neg P doesn't tell you that for some particular XX you have either X\vdash X or ¬X\vdash \neg X.

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 06:18):

Mike Shulman said:

Astra Kolomatskaia said:

Specifically XYtypeX \vdash Y \mathsf{type} means YY is a family of sets over the elements of XX and tt means a dependent function, defined set theoretically

Right: you basically start from your model of set theory and build a model of type theory in the usual way.

Ok, then the observation is that if you start from a model of type theory, and construct an internal model of set theory, called Set\mathsf{Set}, then construct the derived model of set theory Set×Set\mathsf{Set} \times \mathsf{Set}, and construct its internal model of type theory, then that construction does not agree with the diagram model construction on two points in type theory

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 06:19):

At least not definitionally; would there be any equivalence?

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 06:22):

We can also consider the construction [set theory] -> [type theory] -> [type theory] -> [set theory]

view this post on Zulip Mike Shulman (Dec 05 2023 at 06:31):

(Is it possible to move this to a different stream?)

view this post on Zulip Astra Kolomatskaia (Dec 05 2023 at 06:35):

I don't have permission to, but pressing m gives the interface for moving a whole thread

view this post on Zulip Mike Shulman (Dec 05 2023 at 06:45):

For a general diagram construction, I think neither of these squares commutes, because the direction [type theory] -> [set theory] is lossy as I mentioned earlier. (The other direction can be lossy too for weak set theories, but not for the stronger set theories used mostly in practice; chapter 9 of my paper is about this sort of question with type theory replaced by a "structural" set theory like ETCS.)

view this post on Zulip Mike Shulman (Dec 05 2023 at 06:46):

But I think in the simple case of Set×Set\rm Set\times Set, the direction that starts with set theory is not lossy, because when a model of type theory is constructed from a model of set theory everything in it is well-founded, and that carries over to Set×Set\rm Set\times Set since everything is componentwise.

view this post on Zulip Mike Shulman (Dec 05 2023 at 13:41):

Astra Kolomatskaia said:

I don't have permission to, but pressing m gives the interface for moving a whole thread

I guess one thing we could do is move all the messages in this topic to a new one in some other stream, and rename this one back to your personal topic.