Rename `cardinal.omega`

Stream: general

[Violeta Hernández]

I want to rename cardinal.omega to either cardinal.aleph_zero or cardinal.aleph₀, for two reasons

• Pretty much every single reference on set theory (as far as I'm aware) uses ω exclusively for the first infinite ordinal, while using ℵ₀ for the first infinite cardinal.
• Since the notation ω is registered on cardinals, which are almost always used alongside ordinals, it can't be used on ordinals.

[Violeta Hernández]

Apart from asking whether this is a welcome change (particularly to the ordinal coauthors, @Floris van Doorn and @Mario Carneiro), I wanted to ask what cardinal.omega should be renamed to. As mentioned, I see cardinal.aleph_zero and cardinal.aleph₀ as options. I personally prefer the latter for two reasons

• ℵ₀ would not be def-eq to aleph 0, which might cause confusion when spelled out in full.
• It's just shorter.

[Mario Carneiro]

cardinal.aleph_0 is also an option, makes it look less like a subscript

[Violeta Hernández]

How do you make polls in Zulip?

[Violeta Hernández]

/poll Rename cardinal.omega to
cardinal.aleph_zero
cardinal.aleph₀
cardinal.aleph_0
Don't rename it

[Violeta Hernández]

I've opened PR #14467.

[Violeta Hernández]

I'd like to apologize for the huge diff... I swear it's mostly uncontroversial

[Reid Barton]

FWIW, in the category theory/logic literature, it is normal to use $\omega$ for the first infinite cardinal and $\omega_1$ for the first uncountable cardinal

[Reid Barton]

which I found odd at first, but have gotten used to

[Reid Barton]

e.g. an indication of this can be found already at the start of the PR:

/-- A language is countable when it has countably many symbols. -/
class countable : Prop := (card_le_omega' : L.card ≤ ℵ₀)

[Reid Barton]

Maybe we can keep cardinal.omega as an alias or something? I'm less concerned about notation, people can just define whatever local notation they like

[Gabriel Ebner]

I don't think the countable class is a convincing argument for using omega. The card_le_omega' field was just following the naming convention. (It should obviously be renamed to card_le_aleph_0' now.)

[Reid Barton]

Perhaps, but in any case the normal notation for this in model theory is in fact $\omega$

[Violeta Hernández]

Note that model theory and set theory more broadly adopt the convention that cardinals are just a special case of ordinals (which arise from the von Neumann construction), which isn't the case in type theory!

[Violeta Hernández]

And I very strongly oppose having the alias cardinal.omega, since it would make all of the theorems on ℵ₀ unfit for rewriting – unless you were to rewrite that to cardinal.aleph_0, defeating the purpose

[Violeta Hernández]

If the notation ω is used in model theory (and you don't need to talk about ordinals ever), then you can just introduce that as a local notation

[Anne Baanen]

I can't find a coercion ordinal → cardinal, would introducing that help the situation at all?

[Yaël Dillies]

Shouldn't the coercion go the other way around, rather?

[Anne Baanen]

This way you can write ω : cardinal without opening locales. But the other way would make more mathematical sense indeed!

[Eric Wieser]

Violeta Hernández said:

• Since the notation ω is registered on cardinals, which are almost always used alongside ordinals, it can't be used on ordinals.

If this is the motivation, another option would be a has_omega notation class

[Reid Barton]

Violeta Hernández said:

And I very strongly oppose having the alias cardinal.omega, since it would make all of the theorems on ℵ₀ unfit for rewriting – unless you were to rewrite that to cardinal.aleph_0, defeating the purpose

I don't follow--aren't aliases sufficiently transparent to avoid problems?

[Reid Barton]

Violeta Hernández said:

If the notation ω is used in model theory (and you don't need to talk about ordinals ever), then you can just introduce that as a local notation

Yes, this seems like a reasonable approach.

[Violeta Hernández]

We have cardinal.ord and ordinal.card to convert ordinals to cardinals and viceversa. I think making them into coercions might be a bit dangerous, since operations on ordinals and cardinals are quite different!

[Violeta Hernández]

And my understanding is that aliases aren't syntactically equal (unlike notations), which leads to the rewriting problems I'm talking about