Definition of ordinals

Stream: mathlib4

[James E Hanson]

To what extent is it considered desirable to mimic the existing terminological expectations of a given field?

The reason why I ask is that generally speaking the majority of mathematicians who actually use the word 'ordinal' are going to be expecting it to be a canonical representative of a given isomorphism class of well-order types, rather than the isomorphism type itself.

[Violeta Hernández]

I think that's an entirely orthogonal discussion to the one I'm proposing. But if you want my opinion I think redefining ordinals as the subtype docs#ZFSet.IsOrdinal would do much more harm than good.

[James E Hanson]

Violeta Hernández said:

I think that's an entirely orthogonal discussion to the one I'm proposing. But if you want my opinion I think redefining ordinals as the subtype docs#ZFSet.IsOrdinal would do much more harm than good.

I was not suggesting that. I'm just saying that the thing that is currently called Ordinal in Mathlib is closer to what I would call a 'well-order type' (as in an isomorphism class of well-orders) and the output of Ordinal.ToType is closer to what I would call an 'ordinal'.

[Aaron Liu]

Since the cardinals is the quotient of sets under isomorphism, having the ordinals be the quotient of well ordered sets under isomorphism seems like a natural choice to me

[James E Hanson]

I'm not saying it's not a reasonable choice. I'm saying it doesn't line up with the way people use the word in practice, which is why I asked "To what extent is it considered desirable to mimic the existing terminological expectations of a given field?"

[Notification Bot]

4 messages were moved here from #mathlib4 > Unbundled relations and ordinal API by Violeta Hernández.

[Notification Bot]

A message was moved here from #mathlib4 > Unbundled relations and ordinal API by Violeta Hernández.

[Violeta Hernández]

James E Hanson ha dicho:

Violeta Hernández said:

I think that's an entirely orthogonal discussion to the one I'm proposing. But if you want my opinion I think redefining ordinals as the subtype docs#ZFSet.IsOrdinal would do much more harm than good.

I was not suggesting that. I'm just saying that the thing that is currently called Ordinal in Mathlib is closer to what I would call a 'well-order type' (as in an isomorphism class of well-orders) and the output of Ordinal.ToType is closer to what I would call an 'ordinal'.

I think there's a more general tendency in pen and paper mathematics to try and understand quotients by giving some "canonical" representative out of each class. This is why you often see ℤ/nℤ described as "the numbers from 0 to n - 1", or why a group theory argument might start with "take an element out of each coset". We just find it easier to think of a single element, rather than a whole family of elements with some common property.

The same often happens to ordinals. Be it for technical or didactical reasons, one often defines an ordinal as a transitive ZFC set, well-ordered under membership. And that ensures that every ordinal corresponds to a single "canonical" linear order.

But I'd argue the benefit of doing this, at least within Lean's theory, is quite slim. By the point you're defining addition, you have to contend that x + y isn't really the lexicographic sum of x and y, but rather whichever ordinal that's isomorphic to it. And something similar ends up happening with all of the other arithmetic operations. Your initial choice of representative ends up not mattering at all.

[Violeta Hernández]

To answer your more general question, I think Mathlib is generally comfortable with deviating from the literature if it ends up making things simpler or more general. Another example within set theory: docs#Cardinal.aleph is defined in terms of some made up docs#Cardinal.preAleph. This doesn't appear in the literature, but being the proper order isomorphism between ordinals and cardinals, it makes proving its basic properties much simpler.

[James E Hanson]

Violeta Hernández said:

And that ensures that every ordinal corresponds to a single "canonical" linear order.

Why are you putting the word 'canonical' in quotes here? It is a canonical choice.

[James E Hanson]

Violeta Hernández said:

This is why you often see ℤ/nℤ described as "the numbers from 0 to n - 1",

But this is how it's done in Mathlib.

[Aaron Liu]

James E Hanson said:

Violeta Hernández said:

This is why you often see ℤ/nℤ described as "the numbers from 0 to n - 1",

But this is how it's done in Mathlib.

that's because it produces better definitional properties (two closed terms of ZMod n are equal iff they are definitionally equal)

[Yury G. Kudryashov]

James E Hanson said:

Violeta Hernández said:

And that ensures that every ordinal corresponds to a single "canonical" linear order.

Why are you putting the word 'canonical' in quotes here? It is a canonical choice.

There is no canonical choice from Lean's type theory point of view, only a choice up to an isomorphism.

[James E Hanson]

Yury G. Kudryashov said:

James E Hanson said:

Violeta Hernández said:

And that ensures that every ordinal corresponds to a single "canonical" linear order.

Why are you putting the word 'canonical' in quotes here? It is a canonical choice.

There is no canonical choice from Lean's type theory point of view, only a choice up to an isomorphism.

I don't necessarily think this would be a good definition (specifically because of universe issues), but in what way is {β : Ordinal // β < α} not a canonical realization of the order type of α?

[James E Hanson]

Also in the sentence I quoted, Violeta was talking about ordinals in the context of ZFC, not in the context of Lean.

[James E Hanson]

Violeta Hernández said:

By the point you're defining addition, you have to contend that x + y isn't really the lexicographic sum of x and y, but rather whichever ordinal that's isomorphic to it.

Ordinal addition is often defined by transfinite recursion and then it's shown as a theorem that x + y is isomorphic to the order sum of x and y.

[James E Hanson]

Would either of you care to explain what's :sad: about that?

[Aaron Liu]

I just don't like that definition very much anymore

[Aaron Liu]

if I had to come up with a concrete objection then how about "it doesn't generalize to transfinite sums" (at least I don't think it does)

[Yan Yablonovskiy 🇺🇦]

And it can't be used for general order type addition , so going by the lexicographic sum method seemed more natural to me. What is the benefit of defining it via transfinite recursion? ( are we still talking about inside ZFC? )

[James E Hanson]

Yan Yablonovskiy 🇺🇦 said:

And it can't be used for general order type addition , so going by the lexicographic sum method seemed more natural to me. What is the benefit of defining it via transfinite recursion? ( are we still talking about inside ZFC? )

This is not really a strong argument, but it fits into the general framework of transfinite recursion and works as a basic example. You do a lot of stuff with transfinite recursion in set theory, most of which doesn't seem to be doable with these kinds of definitions.

[James E Hanson]

Aaron Liu said:

if I had to come up with a concrete objection then how about "it doesn't generalize to transfinite sums" (at least I don't think it does)

It can be, although I wouldn't claim it's a cleaner definition. You define it by transfinite recursion with $\sum_{i < \beta} \alpha_i = \sup_{\gamma < \beta} \left(\left(\sum_{i < \gamma} \alpha_i\right) + \alpha_\gamma\right)$.

[Aaron Liu]

it really feels like you're hiding the intuition, which is a lexographic sum, behind some transfinite recursion for essentially no reason

[James E Hanson]

There are a lot of different constructions in set theory that are essentially transfinite compositions of operations, such as the definition of various inner models and iterated forcing extensions. At some point the correct intuition is transfinite recursion.

[James E Hanson]

The definition I wrote is just a compact way of saying that a transfinite sum of ordinals is transfinitely composing the operation of ordinal addition.

[James E Hanson]

It would probably be more conventionally written like this:

• $\sum_{i < 0} \alpha_i = 0$
• $\sum_{i < \beta + 1} \alpha_i = \left(\sum_{i < \beta} \alpha_i\right) + \alpha_\beta$
• $\sum_{i < \lambda} \alpha_i = \sup_{ \beta < \lambda} \sum_{i < \beta} \alpha_i$ for $\lambda$ a limit ordinal.

[James E Hanson]

This is a direct generalization of defining finite sums in terms of foldr, conceptually speaking.

[Violeta Hernández]

James E Hanson ha dicho:

Would either of you care to explain what's :sad: about that?

This is just a matter of taste, but I don't like limit recursion very much. It means you always have to consider three different cases separately. And often, if you put in some thought, you can find a better definition which only splits up one or two cases.

[James E Hanson]

Violeta Hernández said:

James E Hanson ha dicho:

Would either of you care to explain what's :sad: about that?

This is just a matter of taste, but I don't like limit recursion very much. It means you always have to consider three different cases separately. And often, if you put in some thought, you can find a better definition which only splits up one or two cases.

You can often get it down to just one case. $\alpha + \beta = \sup_{\gamma < \beta} \left((\alpha + \gamma) + 1\right)$.

[Violeta Hernández]

Yeah, that's what I was about to say. I was also going to bring up docs#ZFSet.vonNeumann and docs#Cardinal.beth where I managed to find definitions without the standard case splitting.

[Violeta Hernández]

Yan Yablonovskiy 🇺🇦 ha dicho:

And it can't be used for general order type addition , so going by the lexicographic sum method seemed more natural to me. What is the benefit of defining it via transfinite recursion? ( are we still talking about inside ZFC? )

I guess it's worth bringing up our plans to eventually redefine docs#Ordinal as a subtype of docs#OrderType.

[James E Hanson]

Violeta Hernández said:

Yeah, that's what I was about to say. I was also going to bring up docs#ZFSet.vonNeumann and docs#Cardinal.beth where I managed to find definitions without the standard case splitting.

This is pretty common in constructive set theory (where you can't do the zero/successor/limit case split). That said, there are a fair number of definitions by transfinite recursion where you really do need to treat limits (or certain limits) specially.

[James E Hanson]

I don't really see this as that different from how many many proofs by induction on $\mathbb{N}$ need to treat $0$ as a special case.

[Violeta Hernández]

I do also complain when I see inductive proofs separate the zero case when a strong induction would suffice.