Cantor Normal Form in set.mm

[sctfn]

So, for further work on surreals, I need to define natural ordinal addition (see https://en.m.wikipedia.org/wiki/Ordinal_arithmetic#Natural_operations) Using my frecs, I can define this as

A+B = |^| { x e. On | ( A. b e. B ( A + b ) e. x /\ A. a e. A ( a + B ) e. x ) }

However, the more usual definition is in terms of the Cantor Normal Form of A and B (see https://en.m.wikipedia.org/wiki/Ordinal_arithmetic#Cantor_normal_form). There is a lot of machinery needed to state, let alone prove, CNF in Metamath. This issue is for either me or someone else to take up developing that machinery.

In particular, we need an analog of sum for _om. Since ordinal addition is non-commutative we need to take some care in defining this.

[icecream17]

is df-oadd for ordinal arithmetic not suitable?

and (df-sum but using df-rdg or df-secom, or df-gsum) might be useful in the summation of several ordinals

[sctfn]

The problem with using +o is that I need an addition that is strictly increasing in both arguments, not just the second.

I can't use gsum for CNF because it adds on the right, whereas CNF needs addition on the left to avoid absorption. Anyway, I'd like to avoid using the complex number naturals here if possible - one of the things this is leading to is an alternative construction of the reals.

Yeah, a sum using rdg is my general thought, there's just a lot of work between here and there.

[icecream17]

without fully looking into it, I would think that for natural (finite) ordinals specifically, one could use commutativity of addition to show addition is strictly increasing in both arguments

[digama0]

I added CNF to metamath a long time ago because it was needed for the proof of GCH implies choice. See ~df-cnf and related theorems.

[sctfn]

Cool! I missed that. I'll give it a look.

[jkingdon]

I'm assuming we should close this issue in light of df-cnf existing. I suppose I'll do that if no one objects.