Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limit limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory subobject superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 19th 2016

    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 κ\beth_\kappa is strongly inaccessible if κ\kappa is weakly inaccessible (note that κ=κ\aleph_\kappa = \kappa 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 κ\kappa be the smallest strongly inaccessible. Then V κV_\kappa 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 κ\beth_\kappa has cofinality at most κ\kappa, so it can’t be regular. Maybe the strengthening involves some forcing or other change of universe? E.g., you can forcibly shift 2 λ=λ +2^\lambda = \lambda^+ for λ<κ\lambda \lt \kappa, 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 κ\kappa, then there is a least one, say θ\theta. Then V θV_\theta 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 κ\kappa. And that sounds really weird.

    I was also supplied with a AC-free proof that weakly inaccessibles are ()\aleph_{(-)}-fixed points:

    First, a quick induction shows that αω α\alpha\leq\omega_\alpha is always true. If κ\kappa is a limit cardinal, then the set of cardinals below κ\kappa is unbounded; but since it’s also regular there are κ\kappa of them. So ω κκω κ\omega_\kappa\leq\kappa\leq\omega_\kappa, and equality ensues.

    I can edit this into the page if desired.

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 28th 2022

    Andrej Bauer writes concerning

    An inaccessible cardinal is a regular strong limit cardinal. Here, κ\kappa is regular if every sum of <κ\lt\kappa cardinals, each of which is <κ\lt\kappa, is itself <κ\lt\kappa; κ\kappa is a strong limit if λ<κ\lambda\lt \kappa implies |Ω| λ<κ\vert\Omega\vert^\lambda\lt\kappa, where Ω\Omega is the set of truth values.


    The use of |Ω||\Omega| instead of 22 looks like misdirected ideology (hello, constructive people, cardinals don’t make any sense without LEM.

    Worth changing then?

    • CommentRowNumber3.
    • CommentAuthorGuest
    • CommentTimeSep 28th 2022

    hello, constructive people, cardinals don’t make any sense without LEM

    Sure they do, the type of cardinals CardCard is the set-truncation of SetSet in homotopy type theory, regardless if LEM holds or not. What breaks without LEM is defining regular strong limit cardinals, because CardCard no longer forms a strict total order without LEM so the current definition using <\lt doesn’t work.

    • CommentRowNumber4.
    • CommentAuthorGuest
    • CommentTimeSep 28th 2022

    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:

    • Nicolai Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu, Connecting Constructive Notions of Ordinals in Homotopy Type Theory, Mathematical Foundations of Computer Science (MFCS) 2021, p. 70:1-70:16

    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.

    • CommentRowNumber5.
    • CommentAuthorDmitri Pavlov
    • CommentTimeSep 28th 2022
    • (edited Sep 29th 2022)

    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.

  1. Adding reference


    diff, v22, current

  2. replaced Ω\Omega by 22 in the definition and added an explanation for the usage of 22 instead of Ω\Omega


    diff, v22, current

    • CommentRowNumber8.
    • CommentAuthorTobyBartels
    • CommentTimeSep 28th 2022

    While 11 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 Ω\Omega vs 22.)

    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 Ω\Omega. I don't think that we really even need an apology for using 22, but I did edit the current one to clarify that we're not just assuming LEM in this article, but even full AC.

    diff, v23, current

    • CommentRowNumber9.
    • CommentAuthorTobyBartels
    • CommentTimeSep 28th 2022

    By the way, I'm the one who introduced this error (in Revision 3), not Mike in Revision 2.

    • CommentRowNumber10.
    • CommentAuthorDavidRoberts
    • CommentTimeSep 29th 2022

    I don’t see what the problem is to define, in a constructive setting, a cardinal (i.e. a set) XX 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 Ω Y\Omega^Y for all YXY\hookrightarrow X and Y¬XY\not\simeq X). 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 XX

    The category of sets YY with an injection to a fixed set XX and not isomorphic to it at least has the feature that XX is the ’class of all sets’, and in the ambient category of all sets, where we can have PXPX, we can build a universal family at least of all subsets of XX, not quite sure off the top of my head if we can carve out the subset of PXPX consisting of those things not isomorphic to XX, 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.

    • CommentRowNumber11.
    • CommentAuthorGuest
    • CommentTimeSep 29th 2022

    Aren’t having inaccessible cardinals equivalent to having models of ETCS?

    • CommentRowNumber12.
    • CommentAuthorDavidRoberts
    • CommentTimeSep 29th 2022

    ETCS is a bit weaker. A strong limit cardinal is enough:

    • CommentRowNumber13.
    • CommentAuthorTobyBartels
    • CommentTimeSep 30th 2022

    @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 22 to |Ω||\Omega|; it would probably have to be a separate section like it is there.

    • CommentRowNumber14.
    • CommentAuthorGuest
    • CommentTimeOct 1st 2022

    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

    • CommentRowNumber15.
    • CommentAuthorGuest
    • CommentTimeOct 1st 2022

    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.

    • CommentRowNumber16.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 2nd 2022


    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 xx 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 MM-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.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeJan 22nd 2023

    added pointer to:

    diff, v25, current