Timeline for Can Category theory be founded in set theory using worldly cardinals instead of inaccessibles?
Current License: CC BY-SA 4.0
10 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
Jul 1, 2022 at 7:00 | vote | accept | Zuhair Al-Johar | ||
Jun 26, 2022 at 20:53 | comment | added | Zuhair Al-Johar | @TimothyChow,Wojowu, Good point! I see now a kind of convinience gain with universes technically speaking, I don't know how much this weighs in founding Categories as sets, but its a clear point! | |
Jun 26, 2022 at 20:46 | comment | added | Timothy Chow | @ZuhairAl-Johar Wojowu's example is a good one. Shulman's article gives other examples where you have to check how much Replacement you're using. I wouldn't call any of these a "main concern" or a decisive consideration; it's just a matter of what sorts of things you find annoying and what sorts of things you are happy to tolerate. If you share Muller's preferences then you may like his approach, but others who want to minimize checking technicalities and aren't bothered by "superabundancy" may prefer universes. | |
Jun 26, 2022 at 20:31 | comment | added | Wojowu | I'm afraid I am unfamiliar with Muller's ideas. I'm only commenting on the usual pragmatic use of universes in category theory. Universes dispense essentially all worries. If you use worldlies, then they should too, but strictly speaking you are then required to check. | |
Jun 26, 2022 at 20:19 | comment | added | Zuhair Al-Johar | @TimothyChow, are you suggesting that working with worldly stages for example is involved with more logical fuss? Why? I understand that working with universes has already been found convinient, but I'm not seeing the point of where it edges the worldly approach from the convinience side? By the way intuitively speaking worldly stages are kind of universes, though not necessarily inaccessible, actually universes are universes because they are worldly! | |
Jun 26, 2022 at 20:13 | comment | added | Zuhair Al-Johar | @Wojowu, well is that a main concern from the Category theory side? If so, then why do Muller suggests his theory ARC? Clearly, his subworld (as well as any of the iterative powers over it) won't assure that for the indefinable sequences you've alluded to? The impact of this point on work in Category theory needs to be emphasized if it is a main concern, since this virtually almost invalidates Muller's claims. | |
Jun 26, 2022 at 19:47 | comment | added | Wojowu | @ZuhairAl-Johar A priori you need more than just them satisfying ZFC. For instance you want all sequences of elements from $V_\kappa$ of length smaller than $\kappa$ to have a bound in $V_\kappa$. Worldliness only guarantees this for sequences which are definable in $V_\kappa$. If you used worldlies, then you would always need to worry about such issues of definability. But if you do worry about strength, then as the answer explains, already ZFC is enough | |
Jun 26, 2022 at 19:47 | comment | added | Timothy Chow | Universes are convenient because you can just simply invoke another universe when you want to go up another level, with a minimum of logical fuss. Practitioners, for the most part, aren't bothered by questions of exact logical strength, which they typically regard as being pedantry. But they will get annoyed if you tell them they have to fuss around with technical protocols in order to obey proper hygiene. | |
Jun 26, 2022 at 19:43 | comment | added | Zuhair Al-Johar | Yes, but why not do matters with less assumptions, I mean if worldly stages can do the job, then why not stick to them, why go to inaccessibles? Is there a specific gain from doing so? I mean the Category theoriest went to those universes because they model ZFC and the powers are absolute and so on.., but this is the same with worldly stages? So why use extra-material if the same gain is there, why for instance it is more convient to use the universes approach? You see the question repeats itself even at practicality spheres. | |
Jun 26, 2022 at 19:34 | history | answered | Timothy Chow | CC BY-SA 4.0 |