IsInaccesible definition

Stream: maths

[Violeta Hernández]

Currently, docs#Cardinal.IsInaccessible explicitly excludes 0 and ℵ₀ from being inaccessible. Does it make sense to include one or both of these?

[Violeta Hernández]

My reasoning: I'm planning to formalize some basic stuff on Grothendieck universes, particularly the result that they are exactly the sets V_o with IsInitial o and o.card.IsInaccessible... or o = 0 or o = ω.

[Violeta Hernández]

@Nir Paz

[Violeta Hernández]

I know that Metamath counts ℵ₀ as an inaccessible:
https://us.metamath.org/mpeuni/omina.html

[Violeta Hernández]

Many definitions of "inaccessible" explicitly disallow ω as an inaccessible cardinal, but this choice allows us to reuse our results for inaccessibles for ω.

[Violeta Hernández]

I'm not quite sure what the results in question are, though

[Violeta Hernández]

Nir Paz mentioned in DMs that inaccessibles other than 0 or ℵ₀ are fixed points of the aleph and beth functions, though I guess it should be noted both 0 and ℵ₀ are fixed points of docs#Cardinal.preAleph

[Violeta Hernández]

(Also, there is a proper class of other non-inaccessible fixed points)

[Nir Paz]

Violeta Hernández said:

My reasoning: I'm planning to formalize some basic stuff on Grothendieck universes, particularly the result that they are exactly the sets V_o with IsInitial o and o.card.IsInaccessible... or o = 0 or o = ω.

You mean you're going to prove this about ZFSetss? I haven't seen the new V hierarchy in there, I guess it's indexed by Ordinal ordinals and not ZFSet ordinals?

[Nir Paz]

If that's the case than another theorem is that V_o is a model of ZFC for an inaccessible o (not 0 or omega)!

[Violeta Hernández]

The V hierarchy is still a pending PR #17027. Its precursor #15793 has been stuck for about two months now.

[Violeta Hernández]

And yes, it's defined as a function Ordinal → ZFSet. I think it makes more sense to use ZFSet only when the specific data structure of sets is relevant, and to use Lean types for everything else.

[Violeta Hernández]

Nir Paz said:

If that's the case than another theorem is that V_o is a model of ZFC for an inaccessible o (not 0 or omega)!

But V_ω is a model of ZFC - Infinity (and V_0 is a model of ZFC - Infinity - Empty)

[Violeta Hernández]

I guess there is a pattern of 0 and ω being special cases of sorts, so perhaps it makes sense to separate them out

[Floris van Doorn]

The mathematical (set theoretic) notion of inaccessible almost uniformly excludes ℵ₀, so I would be unhappy to change the definition to include them. I'm happy to add a new notion IsPreinaccessible (IsPreInaccessible?) that includes ℵ₀ (or both) (similar to IsPreconnected) if that is often useful.

[Violeta Hernández]

Hm, alright. I guess I'll get to proving theorems and see if that comes up particularly often.