Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
The following sentence was at inaccessible cardinal:
A weakly inaccessible cardinal may be strengthened to produce a (generally larger) strongly inaccessible cardinal.
I have removed it after complaints by a set theorist, and in light of the below discussion box, which I have copied here and removed.
Mike: What does that last sentence mean? It seems obviously false to me in the absence of CH.
Toby: It means that if a weakly inaccessible cardinal exists, then a strongly inaccessible cardinal exists, but I couldn't find the formula for it. Something like is strongly inaccessible if is weakly inaccessible (note that then), but I couldn't verify that (or check how it holds up in the absence of choice).
Mike: I don’t believe that. Suppose that the smallest weakly inaccessible is not strongly inaccessible, and let be the smallest strongly inaccessible. Then is a model of set theory in which there are weakly inaccessibles but not strong ones. I’m almost certain there is no reason for the smallest weakly inaccessible to be strongly inaccessible.
JCMcKeown: Surely has cofinality at most , so it can’t be regular. Maybe the strengthening involves some forcing or other change of universe? E.g., you can forcibly shift for , and then by weak inaccessibility, etc… I think. Don’t trust me. —- (some days later) More than that: since the ordinals are well ordered, if there is any strongly inaccessible cardinal greater than , then there is a least one, say . Then is a universe with a weakly inaccessible cardinal and no greater strongly inaccessible cardinal. Ih! Mike said that already… So whatever construction will have to work the other way around: if there is a weakly inaccessible cardinal that isn’t strongly inaccessible, and if furthermore a weakly inaccessible cardinal implies a strongly inaccessible cardinal, then the strongly inaccessible cardinal implied must be less than . And that sounds really weird.
I was also supplied with a AC-free proof that weakly inaccessibles are -fixed points:
First, a quick induction shows that is always true. If is a limit cardinal, then the set of cardinals below is unbounded; but since it’s also regular there are of them. So , and equality ensues.
I can edit this into the page if desired.
Andrej Bauer writes concerning
An inaccessible cardinal is a regular strong limit cardinal. Here, is regular if every sum of cardinals, each of which is , is itself ; is a strong limit if implies , where is the set of truth values.
that
The use of instead of looks like misdirected ideology (hello, constructive people, cardinals don’t make any sense without LEM.
Worth changing then?
hello, constructive people, cardinals don’t make any sense without LEM
Sure they do, the type of cardinals is the set-truncation of in homotopy type theory, regardless if LEM holds or not. What breaks without LEM is defining regular strong limit cardinals, because no longer forms a strict total order without LEM so the current definition using doesn’t work.
Also regarding Andrej Bauer’s statement, it is rather ordinals which are not well-defined absent LEM, not cardinals. There are at least 3 separate definitions of ordinals in constructive homotopy type theory, the higher inductive ordinals in the HoTT book, brouwer ordinal trees, and cantor normal forms, as written up in:
So there are multiple inequivalent definitions of Ord absent LEM, and it is also no longer true that Card is equivalent to any single one of the Ord definitions without LEM.
There is an actual mistake in the article: 1 is not a strong limit cardinal, so cannot be inaccessible.
This claim was added in Revision 3.
While is regular, it's not a limit, so it shouldn't have been listed as one of the trivial examples; I fixed that. (This is what started the recent discussion on Twitter, not the bit about vs .)
Although it's not true that cardinals make no sense without LEM, this page doesn't make sense of them that way; it assumes LEM, so it would just be misleading to say . I don't think that we really even need an apology for using , but I did edit the current one to clarify that we're not just assuming LEM in this article, but even full AC.
By the way, I'm the one who introduced this error (in Revision 3), not Mike in Revision 2.
I don’t see what the problem is to define, in a constructive setting, a cardinal (i.e. a set) being a strong limit if the corresponding category of sets isomorphic to subsets of it has power objects (which would be better than stating it contains for all and ). Clearly, as there are different notions of size of sets (injections, subquotients etc), there would be a variety of such notions of strong limit, but it’s nothing new that constructivity leads to separation of concepts. I’m happy to be corrected. The negative condition of not being isomorphic is clearly a point of weakness, more so than just demanding an injection to
The category of sets with an injection to a fixed set and not isomorphic to it at least has the feature that is the ’class of all sets’, and in the ambient category of all sets, where we can have , we can build a universal family at least of all subsets of , not quite sure off the top of my head if we can carve out the subset of consisting of those things not isomorphic to , but it seems reasonable. If we can get this ’small powerobject’, then we are getting close to a model of a fragment of algebraic set theory.
Aren’t having inaccessible cardinals equivalent to having models of ETCS?
ETCS is a bit weaker. A strong limit cardinal is enough: https://golem.ph.utexas.edu/category/2021/06/large_sets_2.html
@DavidRoberts #10:
I think that the correct approach here is not to speak of properties of cardinals/sets themselves, but rather properties of classes of cardinals. Assuming AC, every cardinal determines the class of those cardinals less than it, which is downward-closed and small; and conversely, every downward-closed small class of cardinals is determined in this way. Without AC, and especially without LEM (but already somewhat without AC even with LEM), it's not clear what ‘less’ and so ‘downward-closed’ mean, so we get a variety of notions (as you noted), and we don't get the converse theorem for (as far as I can tell) any of them. So since it's the closure properties of the class of cardinals that we really want, we should just talk about those.
You can see this done at regular cardinal. We could do the same thing here, but it wouldn't just be a matter of changing to ; it would probably have to be a separate section like it is there.
So from a structural perspective on we should really be talking about families of sets instead of individual sets, and in type theory one should be talking about Tarski universes
How does the definition of strong limit cardinal even work in weakly predicative mathematics? There is no subobject classifier but there is still a set with two elements and function sets.
@Toby
The standard definition of strong limit and inaccessible are already about properties of classes of cardinals, from where I stand, it’s just that the class is defined from the given original cardinal in passing through the definition: “The cardinal is called [blah] if the class [blah2] has the property [closure condition on blah2]”. It might be that the definition of the class is inappropriate in a constructive setting, or that one should consider classes not (informally speaking) definable from a single cardinal. But one can easily drop the restriction of classes [blah2] as being just those arising from a single cardinal in any of the proposed ways. But I don’t think we are disagreeing, here.
I agree about the page structure suggestion.
There is an interesting question, though, and that might be shades of inner models vs other models (eg gound model of forcing models): one could ask that the subcategory of sets in question has some closure properties with respect to the overall -category of sets, where the tight maps are the literal set inclusions, and the loose maps are the arbitrary functions. So, for instance, being closed under subsets in the usual material sense. And similarly with something like powersets, finite products and so on. Or else one could have a more structural view, and ask that the subcategory is merely a model of eg ETCS in its own right, with no reference to the ambient category of sets.
I don’t have any well-formed thoughts, it just occurred to me, if one is trying to capture some observed phenomena, there might be something (small) to say here.
added pointer to:
1 to 18 of 18