defining surreal numbers

Stream: new members

[Jon Ezeiza]

Hello there, not sure if this is the right stream to ask this, but hopefully someone can point me in the right direction, I'm new to the community.

I'm going through Donald Knuth's lovely book on Surreal Numbers and formalizing it as a learning exercise. In short, a surreal number is composed of a pair of sets of surreal numbers, and I'm struggling to express this in a simple way in Lean.

Recursive structures don't seem to be supported. I then tried this:

inductive surreal
| mk : (set surreal) → (set surreal) → surreal

But it throws: arg #1 of 'surreal.surreal.mk' has a non positive occurrence of the datatypes being declared

It seems like this is fundamentally contradictory, which is fair enough.
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/question.20about.20game.20theory/near/162067308

I then instead tried this:

import data.finset

inductive surreal
| mk : (finset surreal) → (finset surreal) → surreal

But it also throws this, which I don't entirely understand: inductive type being declared can only be nested inside the parameters of other inductive types

I am aware the surreal numbers are already defined in mathlib. They are defined as a quotient type of pre-games, which is defined as a pair of sets of arbitrary type (the are not actually sets but (t: Type*) -> pgame constructors).

But for the time being, I'd like to make my own isolated definition of surreal numbers. Is there a simpler way to do this without having to resort to this rather convoluted pre-game construction?

[Jon Ezeiza]

I suppose a more abstract type will always be needed, since surreal numbers are not just a set of two sets of surreal numbers. All the left numbers need to be smaller than all the right numbers. This is defined in mathlib as pgame.numeric. And there's also an equivalence relation which can be naturally modelled as a quotient.

Still it would be more ergonomic to have something like (just roughly):

inductive surreal (l: set surreal) (r: set surreal)
| mk : (l < r → Prop) → surreal

[Kyle Miller]

inductive type being declared can only be nested inside the parameters of other inductive types has to do with how Lean handles these sorts of nested types. It transforms the inductive type you're defining to be an equivalent one that doesn't mention the other inductive type. The problem with finset is that it's got a quot nested in there, which I guess it can't handle.

For example, if you used ordered finite sets (a.k.a. lists) it works

inductive surreal
| mk : (list surreal) → (list surreal) → surreal

[Kyle Miller]

I think this should be equivalent to your finset-based surreal:

inductive presurreal
| mk : list presurreal → list presurreal → presurreal

inductive presurreal_eqv : presurreal → presurreal → Prop
| perm (x x' y y' : list presurreal) (hx : x ~ x') (hy : y ~ y') :
  presurreal_eqv (presurreal.mk x y) (presurreal.mk x' y')

def surreal := quot presurreal_eqv

[Kyle Miller]

Oh, right, I forgot non-duplication

[Notification Bot]

Jon Ezeiza has marked this topic as unresolved.

[Jon Ezeiza]

I've kept persisting and trying many alternatives (most not workable), this is the best I've come up with so far, let me know what you think.

/-
Rule 1: Every number corresponds to two sets of previously created numbers, such that no member of
the left set is greater than or equal to any member of the right set.

Rule 2: One number is less than or equal to another number if an only if no member of the first
number's left set is greater than or equal to the second number, and no member of the second
number's right set is less than or equal to the first number.
-/

def is_surreal (α: Type*) [has_le α] (left right: α → set α) : Prop :=
  ∀ (s : α) (l ∈ left s) (r ∈ right s), ¬(l ≥ r)

namespace surreal

def le
  {α: Type*} [has_le α] [has_lt α] {left right: α → set α} {h: is_surreal α left right} (x y: α)
: Prop := (∀ (l ∈ left x), ¬(l ≥ y)) ∧ (∀ (r ∈ right y), ¬(r ≤ x))

end surreal

It's quite a mess, maybe someone can propose some ways to make it less verbose.

I've kept pushing because I feel like there is nothing fundamentally complex about the two rules that define surreal numbers. I'm trying to understand why they are so hard to encode directly in Lean, without having to define rather abstract auxiliary mathematical objects like pgame from mathlib.

I understand that the core challenge is that the definition of the type requires a defined ordering, which in turn requires the type to be defined. It's hard to bootstrap it without another underlying type.

I wonder if it is possible to define an inductive type whose constructors can only output valid surreal numbers with some smart composition operators. I've tried a few drafts but nothing conclusive so far. I still feel like there should be a way to express the two rules directly, they would be needed anyways to prove that such an inductive type works as intended.

[Kyle Miller]

It might be easier to define a set in docs#Set (ZFC sets). With ZFC sets, at least on paper, it's easy to make a set that's closed with respect to containing all ordered pairs of subsets. (You define a family of sets indexed by the natural numbers, each the closure of the previous, then take the union of all of these.)

[Kyle Miller]

Type theory doesn't have this sort of union, which seems to be the main difficulty.

I guess you could use some of the category theory library for this, since you could take the colimit of a sequence of types that each have an inclusion into the next...

[Jon Ezeiza]

Interesting, I'm not familiar with ZFC, I will take a look.

So it is a fundamental limitation of type theory? Why do these two simple rules require anything more than the simple axiomatic definition of a set?

[Kyle Miller]

A type of surreal numbers exists, as evidenced by mathlib's surreal type. It can just be tricky getting to it; for example, the inductive command does what it can to try to create a type for you given your specification, but it's somewhat conservative. In principle, I think (in my ignorance as a non-type-theory-expert) there could be a more complicated command that could handle quot nesting.

[Jon Ezeiza]

Damn it :sweat_smile:, just wanted to have a chill time formalizing the nice Surreal Numbers book
https://www-cs-faculty.stanford.edu/~knuth/sn.html

It's rather simple maths in itself, but I understand it might be tricky to link it to the axiomatic foundations of Lean.
I think I'll just stop being stubborn, use the mathlib type and prove the books theorems on it, instead of trying to define it from scratch.

[Kyle Miller]

I'm just suggesting that in ZFC it might be easier because you can do unions of any set of sets. In type theory, you can't even ask whether two types are disjoint or not, so plain unions don't make sense.

[Kyle Miller]

I haven't looked at the book -- does Knuth really prove that surreals exist? Or is it just convincing enough that you bought into them?

[Reid Barton]

Kyle Miller said:

it's easy to make a set that's closed with respect to containing all ordered pairs of subsets.

I'm not sure I understand this; say the set is $S$; then $S$ is a subset of $S$, so that we should have for instance $(S, S) \in S$?

[Reid Barton]

Did you mean finite subsets?

[Jon Ezeiza]

Can you critique the last draft I proposed. I can feel it's not right, but can you tell me what are the issues with it?

[Junyan Xu]

Kyle Miller said:

I think bogosort is when you randomly try permutations. This one is more principled, you try all of them :smile:

docs#list.decidable_perm works by iterating through elements in the first list and for each element, looking for it in the second list, and removing it from both lists when found (and return false when not found). I think this is O(n^2) rather than O(n*n!).

[Junyan Xu]

@Jon Ezeiza If you use finset or list I think you only get the dyadic rationals, not even all rational numbers.

[Jon Ezeiza]

Kyle Miller said:

I haven't looked at the book -- does Knuth really prove that surreals exist? Or is it just convincing enough that you bought into them?

I don't think so, I haven't finished it. It's not an academic book, it's framed as a conversation between two students. They find the definition "in an ancient inscription" and they have some fun developing the concept and proving a bunch of theorems. I thought it would be a pleasant introduction to the field, so I can bootstrap my knowledge to read the more formal works on surreal numbers, and possibly expand mathlib's coverage of the concept.

[Junyan Xu]

Since the definition docs#Set involves quotient, I don't think you can use it to define inductive types like you can use list. (maybe I just don't understand how you intend to use docs#Set)

[Kyle Miller]

@Reid Barton Ah, I see my mistake, oops. Here's what I was thinking: set $S_0=\varnothing$ and for each $n$, set $S_{n+1}=S_n\cup \{(s,t)\mid s,t\subseteq S_n\}$. Then let $S=\bigcup_n S_n$. Then, uh, that's a set! That contains just some subset of the surreals.

[Junyan Xu]

Mario Carneiro said:

• define the surreals as well formed pgames and take a quotient to get extensionality (surreal)

Notice that the equivalence relation on docs#pgame is a ≤ b ∧ b ≤ a rather than extensionality (that's the equivalence relation on docs#pSet).

[Kyle Miller]

Kyle Miller said:

I'm just suggesting that in ZFC it might be easier because you can do unions of any set of sets.

Ah, this can't work. There's no set of all surreals (I wasn't really thinking about how they generalize ordinals).

[Kyle Miller]

In set theory, there are "bigger sets" called proper classes. In Lean's type theory, there are types in higher type universes, like Type 1 and above.

[Jon Ezeiza]

If anyone is interested, here's a great interview with Knuth about the book I'm going through
https://www.youtube.com/watch?v=mPn2AdMH7UQ

[Kyle Miller]

Hmm, I guess I don't even know how to state whether a set is a surreal number in the language of ZFC...

[Kyle Miller]

With second-order logic you can at least define what it means for a proper class to have the properties of the surreals:

import set_theory.zfc.basic

def is_surreal_class (S : set Set) : Prop :=
{∅, ∅} ∈ S ∧
  ∀ s ∈ S, ∃ (a b : Set), s = {a, b} ∧ (∀ x ∈ a, x ∈ S) ∧ (∀ y ∈ b, y ∈ S)

(and of course this doesn't actually show there is such an S)

Is there a first-order statement that says whether a given element of Set is a surreal though?

[Jon Ezeiza]

Isn't this a superset of surreals? Your class will include non-valid pairs of "recursive sets". Was that intended?

such that no member of the left set is greater than or equal to any member of the right set

[Junyan Xu]

Hmm, I guess I don't even know how to state whether a set is a surreal number in the language of ZFC...

You probably need docs#Set.has_well_founded (axiom of regularity/foundation) and docs#well_founded.fix. By the way I think you want Set.pair a b rather than {a, b} which is an unordered pair.

[Junyan Xu]

I guess that doesn't answer your question. Maybe take a look at this Wikipedia page, where the natural numbers is defined as the intersection of all inductive sets.

[Kyle Miller]

Junyan Xu said:

Maybe that doesn't answer your question. Maybe take a look at this Wikipedia page, where the natural numbers is defined as the intersection of all inductive sets.

It doesn't, but I've always liked that trick.

[Junyan Xu]

This is a definition of surreal numbers similar to the definition of natural numbers:

import set_theory.zfc.basic

universe u
def is_surreal_class' [has_lt Set.{u}] (S : set Set.{u}) : Prop :=
∀ ⦃a b : Set.{u}⦄, (∀ x ∈ a ∪ b, x ∈ S) → (∀ (x ∈ a) (y ∈ b), x < y) → Set.pair a b ∈ S

def surreal [has_lt Set.{u}] : set Set.{u} := ⋂₀ is_surreal_class' /- sorry for abusing defeq -/

[Kyle Miller]

Modulo defining the lt operation, that seems to give the set of surreals, but that's using second-order logic (it's quantifying over subsets of Set). Is there a first-order way to at least state that a given set is a surreal number?

[Junyan Xu]

I see. Your concern is whether the surreals is actually a class (i.e. definale in ZFC). The easiest way to show this I can see is to define the surreals born by dayo for every (von Neumann) ordinal o by transfinite recursion (which probably requires axiom of replacement), then take the union over all von Neumann ordinals (which is indeed definable, a fact I under-appreciated). In fact, to show is_surreal_class' isn't empty, we probably need some construction like this.

[Mario Carneiro]

Here's a really simple definition of the surreals in ZFC: https://us.metamath.org/mpeuni/df-no.html

[Mario Carneiro]

the trick is to not use sets of pairs and instead use a different definition, involving sequences of + and - indexed by an ordinal

[Mario Carneiro]

the hard part is showing that this is isomorphic to the usual definition

[Pieter Cuijpers]

Jon Ezeiza said:

Kyle Miller said:

I haven't looked at the book -- does Knuth really prove that surreals exist? Or is it just convincing enough that you bought into them?

I don't think so, I haven't finished it. It's not an academic book, it's framed as a conversation between two students. They find the definition "in an ancient inscription" and they have some fun developing the concept and proving a bunch of theorems. I thought it would be a pleasant introduction to the field, so I can bootstrap my knowledge to read the more formal works on surreal numbers, and possibly expand mathlib's coverage of the concept.

Ah, only now I reallize you are talking about Knuths book... Try "ONAG" - i.e. "On numbers and games" by Conway himself, that one provides the ground definitions (and doesn't even talk about set's - as he doesn't need much of the constructs of set theory to build games, of which the surreals form just a part).

I think ONAG is the "original", Knuth his book followed later... but I haven't checked.

[Junyan Xu]

I think Conway also take the left and right options to be sets of "already constructed" surreals/games, and transfinite recursion is the most straightforward interpretation in ZFC of such a construction, which isn't straightforward to formalize in Lean's type theory. I didn't check Knuth's book but from this thread I guess it's similar.

[Jon Ezeiza]

Indeed, Knuth says "two sets of previously created numbers", here's the initial informal definition.

Rule 1: Every number corresponds to two sets of previously created numbers, such that no member of
the left set is greater than or equal to any member of the right set.

Rule 2: One number is less than or equal to another number if an only if no member of the first
number's left set is greater than or equal to the second number, and no member of the second
number's right set is less than or equal to the first number.

[Jon Ezeiza]

Kyle Miller said:

I think ONAG is the "original", Knuth his book followed later... but I haven't checked.

Kinda, Knuth's book was technically written first. They had a lunch where Conway explained the rough ideas and wrote the axioms in a napkin, then Knuth independently derived a chunk of the theory for his informal book before Conway finished his.

The full context is explained here:
https://www.youtube.com/watch?v=mPn2AdMH7UQ