Defining initial ordinals

Stream: maths

[Pedro Sánchez Terraf]

As part of #17972 defining the Borel hierarchy, I had included a definition of the first uncountable ordinal ω₁. But after a short discussion during the PR process, we came to the realization that it would be better to have a general definition of the inital ordinals instead. This would supersede the definition of the former.

So, my proposal for implementing this definition is the following:

• Redefine ordinal.omega as a function,

  noncomputable def omega (x : ordinal.{u}) : ordinal.{u} := (aleph x).ord

• If it is required for consistency, also define the corresponding omega' using docs#cardinal.aleph'.

@Violeta Hernández suggested that the original docs#ordinal.omega could be renamed to omega_0, in analogy to ℵ₀; I would add setting up omega_1 for omega 1 (notation: ω₁) since it is very fundamental—I wish it was possible to have subscript arguments, is it? (@Junyan Xu thinks it's not, perphaps in Lean 4? Adding an underscore to the notation, then?).

I'm not sure if theorem names involving ..._omega need to be renamed to ..._omega_0, if older occurrences of ASCII omega are consistently be replaced by ω.

As suggested during the review, this proposal would be part of separare PR.

What are your thoughts?

[Reid Barton]

I would suggest leaving omega alone, and adding a new name for the new thing

[Reid Barton]

Also, not sure this is a good idea, but this does actually work...

[Pedro Sánchez Terraf]

Reid Barton said:

I would suggest leaving omega alone, and adding a new name for the new thing

Well, it seems that ordinal.initial is available (not that I like it very much :sweat_smile:). I'll think of alternatives, but I'm open to suggestions.

[Yaël Dillies]

Pedro Sánchez Terraf said:

I'm not sure if theorem names involving ..._omega need to be renamed to ..._omega_0, if older occurrences of ASCII omega are consistently be replaced by ω.

In fact, this already happened to docs#cardinal.aleph_0, so I see no reason to not do the same here.

[Reid Barton]

The difference is one writes $\aleph_0$, but never $\omega_0$.

[Pedro Sánchez Terraf]

Reid Barton said:

The difference is one writes $\aleph_0$, but never $\omega_0$.

You are right, though the notation appears in some ancient books. Also, people outside set theory seldom writes $\omega$ :smile:, at least in that sense

[Violeta Hernández]

I think that, in the face of inconsistent math conventions, we do have the power to bend things a little for our own convenience

[Violeta Hernández]

I'm an omega_0 supporter

[Reid Barton]

I don't think consistency is a great argument. Because now instead of "everyone calls it $\omega$", we would have "everyone calls it $\omega$, except mathlib that calls it $\omega_0$".

[Pedro Sánchez Terraf]

Thanks for the feedback. Change of plans then:

• Leave omega alone (sic);

• Define initial i as the ith initial ordinal (zero-based, as aleph):

  namespace ordinal
  noncomputable def initial (x : ordinal.{u}) : ordinal.{u} := (aleph x).ord
  end ordinal

• Actually, the $i$-th initial ordinal is denoted by $\omega_i$ in the literature, so I came up with:

  localized "notation (name := ordinal.initial) `ω_` := ordinal.initial" in ordinal

  somehow indicating a subscript. E.g.

  open_locale ordinal
  example : ω_ 0 = ω := by {unfold initial, simp}

Is the last bullet reasonable? (Is there a way to omit the space, as in ω_0?)

[Reid Barton]

I don't know if it is possible to make it work without the space but I think it would be sort of confusing anyways (given that ω_0 is a perfectly valid identifier).

[Violeta Hernández]

Reid Barton said:

I don't think consistency is a great argument. Because now instead of "everyone calls it $\omega$", we would have "everyone calls it $\omega$, except mathlib that calls it $\omega_0$".

I'm arguing for internal consistency, not consistency with the literature.

[Violeta Hernández]

I don't believe omega_0 should be all that contentious. We have omega_α for every other ordinal α, after all.

[Violeta Hernández]

But initial is a fine compromise.

[Pedro Sánchez Terraf]

Violeta Hernández said:

But initial is a fine compromise.

What should I do now? A different approach to what I suggested during my old PR review is to PR just this, wait for it to be merged, and then git merge master borel_hierarchy to update my branch with this change.

Is this reasonable?