Conway's Surreal numbers

[Richard Penner]

Ordinal numbers were developed by Cantor in 1897; Surreal numbers were largely developed between 1965 and 1976, with work continuing currently. Scott Fenton has been working on introducing Surreal numbers in his Mathbox.since 2011 and I think its about time to move them to a new Part 15 between Basic Real And Complex Functions and Elementary Geometry.

Primary definitions are:

• df-no (The class of functions from any of the ordinals to a particular two-element set called signs. This is called the sign expansion representation.)
• df-slt (A linear ordering on the above.)
• df-bday (A function which acts as a synonym for dom f for any element of the above class)

Following Alling, he then proceeds to abstract out the sign expansion representation for the four "axioms" of Alling:

• sltso (The slt relation totally orders the class No.)
• bdayfo (The bday function is onto the class of ordinals.)
• nodense (Between two distinct surreals with the same value of bday, there exists a surreal with a lesser value of bday.)
• noeta (If two sets of surreals are separated, there exists a surreal between them.) 

From these axioms, the Conway construction is introduced with new definitions building on Alling's axioms:

• df-sle (Because less-than or equals is too important in Conway's treatment not to abbreviate.)
• df-sslt (The set-wise separation relation. Because a relation is a class of ordered pairs, it follows that this relation is actually the class of Conway forms of surreal numbers.)
• df-scut (The Conway cut operator, an onto mapping from sslt to No)

Then arithmetic begins with the introduction of 0, 1, set-valued functions that return subsets of No based on birthday and ordering with respect to their argument, induction theorems, and definitions for the operations for addition, negation, and subtraction.

But because the sign expansion is equivalent to the Conway construction, we should be able to close the loop from Conway to the sign expansion. I would argue that if we did this, we could then use sign-expansion, Alling axioms, or Conway constructions freely. Historically, Scott seems to prefer to stick with Conway constructions for future main development.

With the primary definitions (and supporting work on recusion. etc) we could:

• abstract out the functional definition with symbols for the + and - signs and a sign-at operator which gives ( f ` x ) for x e. bday f. (Abstraction is good, I would define + as ( 1s sign-at (/) ) and - as ( ( -us ` 1s ) sign-at (/) .)
• define a pair of successor operators, suc+ and suc– using Conway's construction and show that each results in a sign expansion with a domain that is the successor of the argument
• show that the negation operator simply flips all the signs
• show that the sign expansion of a dyadic proper fraction ( 2 k + 1 ) / 2^n with 0 < 2 k + 1 < 2^n is +, -, followed by the binary representation of k.
• define subclasses of No corresponding to the Ordinals, and the Reals.
• show that adding ordinals gives a constant function to + with a domain that is the natural (Hessenberg) sum of the domains,
• show that for natural number N and dyadic proper fraction F is the sign expansion of N followed by the sign expansion of F
• that the ordinals and reals are isomorphic to our existing constructions of ordinals and reals
• etc

I've got about 89 new theorems dating back to 2023 I would like to add to my Mathbox but cannot since they depend on work in Scott's mathbox. It's a problem compounded by the ordering of the mathboxes, which brings us back to Cantor's 19th century work on order types and ordinal numbers. :)

[Scott Fenton]

I am +1 on this with the caveat that the field operations are probably not ready for prime time yet. Getting natural addition on ordinals should get us there though. 

On Jan 8, 2025, at 8:31 AM, Richard Penner <richar...@gmail.com> wrote:

Ordinal numbers were developed by Cantor in 1897; Surreal numbers were largely developed between 1965 and 1976, with work continuing currently. Scott Fenton has been working on introducing Surreal numbers in his Mathbox.since 2011 and I think its about time to move them to a new Part 15 between Basic Real And Complex Functions and Elementary Geometry.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/93b136fb-7d2d-47f5-a0f7-41fa02aa65e7n%40googlegroups.com.

[Jim Kingdon]

On 1/8/25 05:31, Richard Penner wrote:

> I've got about 89 new theorems dating back to 2023 I would like to add
> to my Mathbox but cannot since they depend on work in Scott's mathbox.

That's reason enough for me to move the surreal number theorems to main.
Our practice is to do so once we have two mathboxes that want to use a
set of theorems.

> It's a problem compounded by the ordering of the mathboxes, which
brings us back to Cantor's 19th century work on order types and ordinal
numbers. :)

Heh, in set.mm we cut this Gordian know by not allowing dependencies
between mathboxes regardless of their order. Pretty sure we have tooling
to check that.