3rd talk/ Miles Tierney: 3rd talk / 3rd talk (contd.)

0:00 How do we get a lift here in the side face? When you take this map together with this one, you get a lifting, you get a map of this in the pullback. This is the pullback, so we get a map here. Now, because this is in B, this is a tributal vibration, and this is a co-vibration.

42:30 I can state it this way, a strong system, but you need to show, for example, if you use A and B, this is the equivalences, the composition, what I've stated in the notes, factorization, given by this, various, that this, factorization, category, and then I'm going to prove it here in the second half of the lecture. So the first half of the lecture follows from, for the model U, follows from a further, we're going to make it a sixth, which says that all monomorphisms are small.

45:00 You can see that quite easily right here. If you have a set here, A, then the class gives you a monomorphism anyway, so here A is a bound, the mono is small, but now small and small means that this one is small. So that gives you what you see in here. This is the system of Joy-Allen-Mordyke, and that is, we add this new condition that all monos are small. In the first lecture, it's actually equivalent to the system of Doyle and Mordyke, essentially, and so that gives the theorem that we were shooting for, but in a model, a set theory, that additional condition at 6, the prima, the three algebras, that f-algebra or p-algebra, remember I said in the beginning of my lecture, the p-algebras for the three algebraic structures coincide. The three algebra U models was the kind of bogus rhetorical theorem that I began with where I started with a model of set theory and then I proved that, or I indicated that it had to be a model of set theory. Well now we've got a real proof of that. We've got the axiomatic frame and we've shown that without assuming that we started from a model of set theory that we actually do reflect our knowledge. C is the issue of collection. Are they also have collection? ISAT app has collection.

47:30 Has collection instead of replacement. Okay, well thank you for that question because that's the next topic that I'm going to talk about is adding collection. So maybe this is ISAT app with replacement instead of collection. So the Joy-on Mordek, actually the Joy-on Mordek is a little bit different so they need collection right away. But I'm going to show you how to do collection right now. This system, the John and Wartek system, with the additional condition S6, can be modeled in any Grotendieck topos, and the result is essentially the same as the Orman interpretation that Peter Fry was talking about in discussing independence proofs for set theory. The algebraic set theory in a Grotendieck topos satisfies this additional condition S6. The result is the form and interpretation of set theory into growth-deep topos that was done in the 80s, I think. So the algebraic set theory in that sense subsumes the previous work on set theory models and toposes. There's a similar result using instead of growth-deep topos, All of these are realisability toposes, and you can make algebraic models in realisability toposes, and the result there agrees with previous realisability models that were given by David McCartney. The form and interpretation into the realisability topos was McCartney's realisability model, and that also is assumed by all of us. Before I go on to the collection, I want to say a little bit of something in a weaker direction. That is, I want to say something about predicative set theories. I'm going to weaken the axioms rather than strengthening them. By a predicative set theory, I just mean set theory with no power set, which is maybe according to Bill's conception to be derived from Cantor, hardly set theory at all if you throw away a power set. But it's a kind of leech notion of set theory.

50:00 What we're going to do in order to model such predicative systems of set theory is this. In the category of classes C, we will drop the condition which I call P2, which said that if A is a small class, a set, then also its power set, which exists anyway by P1, is also small. The set will no longer be a topos as it was under the previous notions, instead now it will be a heightened pretopos. I'm not saying we require that, I'm saying it follows from the other axioms. The axioms stay the same except for this, and then we prove, before we prove the category of sets is then a topos, here the category of sets becomes a heightened pretopos, and the set theory that's modeled We'll still model a set theory, but now instead of modeling the set theory that I had before, it'll model, instead of this, it'll model a kind of predicative intuitionistic set theory. Wow, that's not a very nice word, is it? So let's call it basic constructives, which is essentially the elementary set theory that we had before, but without the power set. Still has full replacement, but no power set. We can, actually there's a slight variation on here that I might as well discuss. In graph P2, we lose the exponentiation of small objects by small objects. If we add that condition, we add that a and b small Then we get a slight strengthening in between these two. The category of sets becomes a locally Cartesian closed tritopos, and the elementary set theory becomes, well, this CST, which is essentially this plus class of all functions between two sets is again a set.

52:30 This situation is roughly the one that Benno was talking about yesterday in the predicative topos, the pi, w, pre-topos stuff that he was talking about. So here's an algebraic set theory that essentially captures the framework that he was working in and actually these conditions on small maps now are essentially... The fact that this works, I'd like to sketch very briefly what makes this work, because it's a non-trivial fact. If you remember how we had the following, I want to emphasize this is a fundamental credit to do. When we had a topos, we constructed the power ideal as an ideal. How did we construct the power ideal, PC? Well, we said we want it to be ideal continuous. And so we just said, let's take this, the ideal, y, e, that will make it ideal continuous, and then we'll define this, the power ideal for a representable, simply by saying p, y, e is the representable of the topos power object of e.

55:00 Topos, we can do it. And finally, we have the function of the function of the function of the function of the function of the function of the function of the function of the function of And now the basic fact is that this functor on the board, I'll put it right here, PE, defined in that way, is E, is a hyphen, is, you check that this functor is so defined, is one, a sheaf, and two, has a small diagonal. And that small diagonal can be an ideal for any tree topology, and the hyphen condition you really need in order to prove that this thing works. So it's a very nice exercise. I'll leave that for you as an exercise. Now given that, backwards here, so this one's an ideal now. The collimative monomorphism is an ideal, is again an ideal.

57:30 And now we have a power object bunker on the category of ideals for any hiding pretopos. Hiding pretopos, including here any locally cartoon post pretopos, we still have that power object I was talking about before. It satisfies the x in P1. It simply no longer satisfies the x in P1. And that's what gives us the rest of the screen. People have asked me, since the last talk, how can it be that every topo satisfies unbounded replacement? That seems so strange. I mean, let's think about the topos of finite sets, or hereditarily finite sets. Of course, that satisfies replacement because if you have a function defined on a finite set, you know... So the images are finite. Then again, when you take the set containing the unions of all the images, then that's again going to be finite. That's no problem, because finite is not finite. But what if you take, for example, the sets, S1, the sets less than omega plus omega. So we take the sets. And then we take an infinite set, and then we start iterating the power set function again, and we close off, but that's it, we stop there. That's a topos, right? It seems like in that topos, well, we have this infinite set omega is in there, and then we have all the iterates of its own power set, and so on. And now it seems like, well, this is defined on omega and into the universe. And so if we have replacement, we should be able to gather these guys all up, right?

1:00:00 All the iterates by replacement. I've said something fishy going on here. How can this topos satisfy unbounded replacement? Because here this would kick us outside the topos for a minute. He already has a proposal for an answer. Not Michael or Henry. Anyone see what the problem is here? That the image has to make it. You mean this? No, no. This is not definable. This is not definable. This certainly is definable in the ambient category. If I take S and I consider it in the ambient category of sets, then fine. The statement that every topos satisfies the full axiom scheme of replacement, the unbounded scheme of replacement, means this. Every topos occurs as a category of sets in a category of classes. It's such a way that replacement is satisfied. But the satisfaction of replacement depends on that ambient category of classes for the interpretation of the unbounded variables in the axiom. They have to vary over something in an unbounded way, and that interpretation depends on the way this thing is sitting inside some ambient category. So, although it does satisfy replacement inside of its ideal completion, It doesn't satisfy replacing these here, and the reason is, as Peter just correctly pointed out, when we put this thing into the ideal completion, this natural numbers object, omega, is still a natural numbers object in here with respect to sets, but it's no longer a natural numbers object with respect to arbitrary classes. And so even though we have each of these iterals, we cannot define the full function on omega, this function on omega, using the

1:02:30 So that's the solution, as it were, to this puzzle. It emphasizes the fact that the satisfaction of certain set theoretic formulas, such as replacement, is very sensitive to the embedding of the sets into the ambient category of classes. Another example of this kind is the axiom scheme of collection. The axiom scheme of collection, which I'll tell you about in a moment, actually also holds in all of these categories of ideals. It doesn't hold in general in the class categories as I've defined them, only replacement does. Collection also holds in these ideal models, so let me just say a word. The scheme of collection says this. So informally, collection says, if I have a set, And I have a relation defined on that set into the universe, and the relation is total on set A. Then I can find another set in the image of the relation set, such that if I restrict the relation down to B, the result is still O. I restrict the relation down to B. The result is now total on B, because B was in the image of the relation I said, but it's still total. So there's a peace sign diagram from the case.

1:05:00 The axiom scheme of the collection says, implicitly or intuitively, there's a better categorical formulation in class categories. It says that the power object functor, the small power object functor, C, preserves regular ethnomorphism. And the idea here is that if this is a regular epimorphism and this is small, then you want to find a pre-image of the total small sub-object on this. The total sub-object on this is small, and so there should be a pre-image back up here, a small thing, which under that projection hits this. If this one is small, then you can find some small one up here. The image of which is still this. This is preservation by P of regular epimorphisms. So now if this one is small, and this is a quotient of it, I just factor this composite out into the image. If this one is small, then this one is small. So that's why the preservation of regular epimorphisms gives you this proposition that in fact, the category of ideals always has collection in it. It has collection in it. It's hard to see that it does. Because the ideals are sitting inside of sheaves, and this is basically a sheave property, if I have some arbitrary covering here of a small thing, A, in the category of sheaves, well, then I can find a small cover, B, of A, and a factorization up here through this arbitrary regular, this arbitrary epimorphism, right? Move back on a cover and lift it up here across this cover.

1:07:30 But now, because this one is small, I can factor out its image, and that will still be small, and here, then, will be my small sub-cover. This one's epic, so that one's epic. This is my small sub-cover of R. Purely, the sheets and ideals are sitting inside the sheets. It makes that nice and true. So, situation. If we were interested in the logic that's satisfied by ideal models, Models of algebraic set theory as they occur in categories of appeals. Then, of course, we would want to add an axiom scheme of collection to our set theory. The point here is, as I said, that the set theory that is satisfied by a topos depends on the ambient category of classes. Sometimes it satisfies this, sometimes it satisfies that, depending on how it's sitting in the classes, but there is a canonical class category structure on any topos, that's the ideal class category over the topos, and so we want to know what is the set theory that holds in there, in the canonical class category structure over the topos, and the fact here is that if we take the basic intuitionistic set theory and we add collection... Then, as I just indicated, this holds in all E, E for this, such ideal categories, and that's quite actually a surprising, I think, and strong result that, moreover, if a formula is satisfied for any ideal, every topos E, then, in fact,

1:10:00 It's provable from basic intuitionistic set theory of collection. Kind of complete axiomatization there of the set theory of ideals. And a proof of this from the following theorem, which I'll spend the rest of the lecture telling you about, this theorem essentially tells us that we have the axioms for classic categories right. At least with respect to ideal completions. It tells us that the ideal completions of toposes are in a sense the typical class categories and the axioms for class categories are complete with respect to those typical ones, the ideal completions. It says that if you give me an arbitrary class category, abstract, satisfying, those C, S, T, U axioms, then I can embed it conservatively. Class categorically, preserving all the class category structure, into a category of ideals on a topos, where you see a conservative, a functor, into ideals on a topos for some, we have nailed down what the classes are. I'd like to give you a little bit of a sketch of the proof of that. So you see how it implies this one, right? Because we knew that, I have to put you in collection, thank you. Every class category with collection, I've shown here. Ideals always have a collection in this. So I want to add that one more condition. You can't quite see that, can I? Every class category, only if you want it to be complete here, you would respect the ideal model.

1:12:30 But yeah, you might as well have proof of this in the notes of this theorem. Oh wait, sorry. And so I'll just kind of give you a sketch of the basic ingredients and the proof. I want to, before I go on, indicate how this one follows because I'm not going to come back. So this one follows from this one because we know that this syntactic theory is complete with respect to abstract class category models, and we did that in the last lecture, or at least I indicated how to do it using a syntactic category construction. It is just the syntactic category, the first order classifying category for these set theories, gives you automatically a class category There is a collection, if you put collection into a theory, which has a generic model, a set theory in it, in the sense that it has all the... And now, since we can embed in particular that generic one into ideals and topos, we have then, by the kind of reasoning that Peter was using in his last lecture, where you can embed everything into a category, into a particular family of restricted objects, a kind of completeness with respect to those restricted objects. So that's the way you get this one. From this one, I should probably, I'll mention, I may not have time to come back to it at the end, I want to mention that, in fact, this, the fact that when you can start a syntactic category out of a theory, you get a class category, is actually related in such a way that they're essentially algebraic, and this was formulated, and which has the important consequence, Class categories are closed under all kinds of operations from other areas. Class categories are closed under taking of all limits. Class categories are closed under taking of filtered coordinates. Class categories have free algebras. There are free class categories, and the free one was exactly the syntactic one.

1:15:00 So that's a kind of... Maybe since it's the end of the week, it's okay to kind of summarize some lessons, a good lesson of categorical logic is when you do logic categorically, you're doing things in a way that is essentially algebraic, and so the categories that correspond to logical theories are algebras in this sense that they respect all of these operations. I spent this banquet last night in my delicious local spirits, late at night, before I went to bed, Peter Pryde gave me a class category. He said, so, tomorrow morning, I want to see this thing embedded into ideals on a topos. So I was up all night trying to invent this thing, ideals on a topos, and here's how it goes. Any class category embeds it. You give me a class category, I give you a topos. That's the game, right? Well, there's one obvious topos around to try, right? There's the sets inside the class category. Let's try that first and see how far we get. So, the sets are sitting in here. So here's C. Here are the sets going in. If you think about the definitions here, this was a regular category with dual images and binocular projects. And we require this to have all the same structure, and moreover, to sit in there fully and preserve all that same structure. So in fact, this is a morphism of sites.

1:17:30 When we take the respective Yomita Kibbetis, let's just say, first of all, it appreciates, without it being a morphism of sites, there's a restriction puncture here on the upper star, and it's two adjoints, a tree which commutes with I, which is the right one. We know that the sheaves are sitting right here, and the ideals are right here. This is factoring the elimination embedded through ideals. And the most obvious thing to do here is to say, well, let's just restrict this data embedding here along I. That is, let's compose through here with the restriction. That gives us this part. This one, restricted along I, homing into C. We homing into it just from small objects. Look at all the mathematical sets in C. Well, this is, of course, a sheet because anything like this is always a sheet. It takes financial products to find a product and it takes equalizers to cope. But moreover, it's an ideal. Why is that an ideal? Well, it's an ideal because in the category of classes, we already required small diagonals. And the embedding, these other functors preserve all the diagonals, the finite products. So they preserve the finite products, say, going over here, but we have the small diagonal condition down here, and that implies a small diagonal condition. So let me call that functor D, which takes C, the ideal completion of S, this extension, D.

1:20:00 And now the proposition here, it's not going to be this easy, but it's almost this easy. It says that the function D preserves the coproducts, because basically these were procured in sheaves in the U.N.A. It preserves the, moreover, small maps. I'm not going to check those, but you can check them. It's in the notes. And it's kind of slick that it works. In fact, I think it tells us something interesting about class categories, that class categories really are actually . So this function preserves all of this structure in a fairly routine way. So what we need is just a little bit more. If small covers, description of this in a moment, of course, if this is small and this covers a small sub-cover, we prime with this one

1:22:30 small. That's small. Small generator says if this is any sub-object In classes, neither of them is small, then if it's not proper, then there exists a small sub-object which does not matter. So if every small sub-object at C is contained in D, then D is all of us. So this, in a sense, in a fairly obvious sense, says that the small objects generate the category. Because if you have two maps out of C which differ, then you take an equalizer and that will not be total, and then you can separate the two maps by a small sub-object of C that won't be equalized. So the small objects generate. This one basically says that every cover of a small thing by a big thing has a refinement by a cover of a small thing. So that will give us the two preservation properties. I don't think I would really take the time to prove this, but I'll indicate that it's a connection, but I won't prove this. I'll show you what the connection is. If you take the small covers, small covers is morally collection. It's what I told you was collection before. Well, it's collection of actual global existence coming from internal existence. So the issue here is simply that something internally can be supposed to exist, but not actually exist because you can't take a global section of something that has global support. So given collection, one holds if one is projected, given collection, one is projected, which we are assuming.

1:25:00 Yes, so, sorry, what I really mean is this condition is small. I shouldn't say, listen, this implies this is part of the problem. Now I'm saying, the condition one, so I should say small covers holes, right? Is that what you had in mind? Small covers holes, if one is projected, small generators holes, if one is projected. Well, it's actually, there's a subtlety here which you'll read about in the notes, okay? Because, let's just look at that one. If we have D and C, Then we have P of D proper in P of C. P of C has global support even if C doesn't because there's zero sub-objects in here. And so the strongly projected is what Peter already defined, I think. And if you have a proper sub-object of a well-supported object, then there exists a section which doesn't factor through. That's what we call strongly projected. It's not just that everything with global support has a section, but it has enough sections to distinguish the sub-object. The global sections function is conservative. So we'll have this if one is strongly projected, but then this S here is a small sub-object of C, isn't it? But it doesn't factor through D, because if it did, this S would factor with you.

1:27:30 And now the only thing we need in order to prove this using another proposition is the following lemma. We just need to force these things to happen, but we can force them to happen by making one strongly projected machine. What we need to do is take our arbitrary class category, send it over in a conservative class category way into another one where one is projected, and then we do this to it. And then we take his ideal embedding of it. Every class category, C, has a conservative... He already did all the work for us. Well, you have to check the rules for all the class categories structure too. But the technique is essentially the one that Peter already showed you. You take C, you take an object with global support, and you slice C over it, You can take your co-limit here, and depending on how big your class category was, you can take that co-limit, C, slice over the successive things here, I, well, that's C star, oh, sorry, not yet, that's C sharp. Because now what you've done is you've added sections for everything that they've always supported you with. So as Peter said, now you have to do it all over again. And now you just keep on going. You take C, you take C into C star, into C star star, and so on. You do that again until the end of time. And eventually, I'm sorry, sharp.

1:30:00 And eventually, you get this. So we put everything together and we prove the theorem like this. We say start with C, put it into C star. Extract the small sets out of C star and then put this one, ideal, in C star. I want to indicate this whole setup has been very kind of schematic, right? I was looking at topos and this and the particular class category actions that I gave you. I indicated a couple of places where you can tweak this and get predicative set theory, tweak that and get full intuitionistic or even full setup set theory. What I want to do now is make some more general remarks about possibilities for taking this program that I've shown you and taking it in a couple of further different directions. Maybe this afternoon at the discussion we'll have time to discuss some open problems, but if we don't, I want to make sure to mention at least a few here in case you're interested in them. So here are, as it were, some open problems. And so, if we take the universe here, then there are two different things going on here. There's the small power class function that we made in the ideal, but there's also the full power sheet of U, and this one embeds into this one. And using the full power sheet of U up here, the sheet, you can model a kind of a higher order set theory.

1:32:30 And this higher-order set theory, because this map is monic, essentially, is going to be conservative over the first-order set theory that we were looking at before. So already, Henrik Forcel, a student who's here, has shown that intuitionistic Morse-Kelley set theory is conservative over intuitionistic F set theory, which is a fact that I believe, well, it's not true, classically. And it's interesting to see that it's true intuitionistically, and we have a pretty nice sheaf here at Proust just using this machine. But that's as far as we've got. We haven't done much more with it, and a lot more, I think, could be done. So that's one direction. Study this. Study the higher order set theory as relating to the elementary set theory. This was actually a question of the importance of closure under sheaves. I guess we don't really know what happens if we take a topology here on sheaves. And then consider what happens to the ideals if that induces another ideal category here in the sheaves, and a specific case that would be nice to look at, I think, is the duplication topology on here, hit a kind of classical class category of ideals in order to model a classical set theory. Not sheaves in ideals on a Boolean book of p. And the way to do that would be to drop the placement in set theory, you have to cook up the small maps a little bit differently, change the definition of small map, drop the placement, in the set theory you have to tweak the small map axioms, and the category of sets then could be a regular locally-croped and closed category, replacement comes from exact, and it's basically because if you have an equivalence relation on a class

1:35:00 If you have a set, you can use replacement to build the equivalence classes for the equivalence. But if you don't have exactness anymore, you can divide it by replacement. And this would be nice, I think, because there are examples of regular LCCs that are not exact, and it would be nice to be able to find the set theory of such things in exactly the way that this was the set theory. That should work. W-times. I have not said anything about W-times. I dropped the power set axiom. I didn't consider replacing it with any kind of other machinery that is a consequence of power. W-times are a consequence of power. You could consider putting the W-times back into the pre-cocos and then seeing what happens with small maps of the ideals and the class category. This is close to what Benno and... I have a study, but I think it would be quite nice to study it from this, within this framework that I've developed. In particular, the question would be, if you take the ideal completion of a pi precircle with w times, do you have w times in here? Maybe you don't take the ideal completion, maybe you should instead take something slightly bigger in here. And then, of course, you can ask for preservation of w times by the principal. A fascinating possibility that we've only just scratched the surface of is proving what Peter was talking about before, the existence and disjunction properties for intuitionistic set theory. Intuition is accepted here as well. In particular, we can prove it for bits using Peter Fry's method, using the Fry code.

1:37:30 So that is the method that I told you about. If you glue a class category, you get a class category. That's the point. If you glue a class category, you get a class category. Take the free class category, which I told you about before. You can also syntactically glue it along its global sections puncture and you get a cover of it by another class category in which the epi is split, in which one is projective and decomposable, and that gives you existence in this juncture in basic intuitionistic set theory. My student Michael Warren has done this along with some other related things. This is the only case we've looked at. An open question right now is that the constructive set theorists are scrambling to solve and they have some very arcane methods. They have only led to partial results is to do this or see them.