surreals (but in parallel to Knuth book)

Stream: Is there code for X?

[Simon DeDeo]

Hello Lean Community,

I was wondering if anyone had tried to do the surreal numbers in Lean but following the exposition in Knuth’s book?

We have them as part of the combinatorial games library (amazing), but I was curious if there was a nice way to develop them in Knuth.

Presumably the first attempts using Sets would founder eventually (?) because the surreals get pretty surreal. But doing that refactor would be a nice pedagogical exercise.

If anyone has tried this and wants to share their experience I’d be very grateful! Again this is largely a pedagogical exercise for me.

Simon

[Ruben Van de Velde]

Our resident expert on surrealism is @Violeta Hernández

[Violeta Hernández]

Simon DeDeo said:

I was wondering if anyone had tried to do the surreal numbers in Lean but following the exposition in Knuth’s book?

I'm not knowledgeable on the specifics of Knuth's book. Are there any notable differences in his treatment of the topic compared to Conway?

[Violeta Hernández]

Regarding sets: one could in theory re-implement CGT#IGame in terms of docs#ZFSet, as a subtype of Kuratowski pairs. But frankly ZFC's treatment of ordered pairs has always seemed to me like a bit of a hack.

[Violeta Hernández]

And this wouldn't let us as readily talk about loopy games.

[Anthony Wang]

Simon DeDeo said:

I was wondering if anyone had tried to do the surreal numbers in Lean but following the exposition in Knuth’s book?

I tried a few weeks ago, but using lists instead of sets:

structure PseudoNumber where
  l : List PseudoNumber
  r : List PseudoNumber

Then I defined ≤ for pseudonumbers and defined surreal numbers as a subtype of pseudonumbers. Unfortunately this approach using lists can't represent surreal numbers where one of the lists should be infinite, but it'll at least get you through the first few chapters of Knuth's book.

[Anthony Wang]

My code is at http://git.unnamed.website/miscelleaneous/tree/Surreal.lean but it's very unpolished and low-quality.

[Violeta Hernández]

This is not at all dissimilar from what the CGT codebase does. There's some category theory black magic hiding the fact, which is necessary for some very technical reasons, but morally IGame is just defined as follows:

inductive IGame : Type (u+1)
  | ofSets (s t : Set IGame) [Small.{u} s] [Small.{u} t] : IGame

That is to say, a game (up to identity) is defined as a docs#Small set of other games. In Lean, small sets are basically the same things as just sets in ZFC (large sets would be proper classes).

[Violeta Hernández]

Just took a look through the codebase. I think everything in there is covered already by Game/IGame.lean and Game/Surreal.lean. Though a very important caveat is that the way that you defined surreals doesn't have the "correct" equality, since you'll have e.g. ⟨[0, 1], []⟩ ≠ ⟨[1], []⟩.

[Simon DeDeo]

Thank you both! Knuth is very informal — it's literally a dialogue, with a lot of informal set theory talk. I thought it might be a fun pedagogical exercise to interleave that dialogue with the way Lean might set things up.

@Anthony Wang your file is lovely! I mean, can't follow it much, because it has a lot of Lean that I don't know — the reason I thought of this idea was as a way to get more comfortable with Lean. But it looks like you're following Knuth and his T1, T2, and so on.

I see you begin with the pseudonumbers, which arise a bit later in the dialogue.

I'm also curious about your use of lists instead of sets (you mention it can cause paradoxes). I think Violeta is saying that you can get around these by using small sets.

Just in the back of my mind all of this seems like great pedagogical material for getting someone familiar with how Lean works. In any case, if I do something with this I'll be sure to mention it here. And if anyone has played out Knuth a bit further, perhaps with more exposition, I'd love to see it.

[Anthony Wang]

I used lists because Lean rejects the naive definition of

structure PseudoNumber where
  l : Set PseudoNumber
  r : Set PseudoNumber

(See #Is there code for X? > Surreal numbers @ 💬, although note that that thread is old and uses Lean 3 instead of Lean 4)

I defined the pseudonumbers first because the definition of surreal numbers requires ≤ defined already, but defining ≤ requires surreal numbers defined already. My solution was to define ≤ for pseudonumbers and then use that instance of ≤ in the definition of surreal numbers to break the cycle. I first tried using a mutual block but that didn't work because Lean doesn't allow defining both a structure and a function def inside the same mutual block.

[Simon DeDeo]

Thank you! — that's a very helpful thread as well (I like how it's Johan who is like, I'm not sure how to pull this off!)

[Violeta Hernández]

Simon DeDeo said:

I'm also curious about your use of lists instead of sets (you mention it can cause paradoxes). I think Violeta is saying that you can get around these by using small sets.

I can elaborate on this point. Lean does not let you define an inductive type like this:

inductive Bad : Type
  | mk : (Bad -> Prop) -> Bad

The reason is that constructors of inductive types are required to be injective, which is not possible here due to Cantor's theorem. Note that Set X = X -> Prop.

[Violeta Hernández]

The way we sidestep this is quite technical. We basically have to use the internal theory of inductive types (as initial F-algebras of a functor) to prove that, when you restrict to small sets, the desired inductive type actually exists. But once you have that the rest of the theory proceeds as normal.

[Violeta Hernández]

You can accomplish the same by first defining an "auxiliary" type of games

inductive PGame : Type (u+1)
  | mk (a b : Type u) (l : a -> PGame) (r : b -> PGame) : PGame

and taking the quotient by some complicated relation. This is what an older version of our codebase did. Works, but ends up being more tedious.

[Snir Broshi]

Violeta Hernández said:

I can elaborate on this point. Lean does not let you define an inductive type like this:

inductive Bad : Type
  | mk : (Bad -> Prop) -> Bad

The reason is that constructors of inductive types are required to be injective, which is not possible here due to Cantor's theorem. Note that Set X = X -> Prop.

Is this related to Curry's paradox? I heard something like "the number of function arrows to the right of the type used recursively must be odd"

[Matt Diamond]

@Snir Broshi I believe it is, based on the Positivity, strict and otherwise page on counterexamples.org

[James E Hanson]

Violeta Hernández said:

Regarding sets: one could in theory re-implement CGT#IGame in terms of docs#ZFSet, as a subtype of Kuratowski pairs. But frankly ZFC's treatment of ordered pairs has always seemed to me like a bit of a hack.

What would the actual technical issues with this approach be?

[Aaron Liu]

technically it would be very annoying

[Timothy Chow]

Everything in ZFC seems like a hack, if you're not used to it. If all you have to work with are sets, then you have to "hack" everything else. I think James Hanson is asking whether there is anything more to the complaint about Kuratowski pairs than "set theory is icky and I don't like working with it."

[Aaron Liu]

For example, if everything is a set then ext will tell you to show they're equal by they have the same elements, but what you really want is to show a pair is equal to another pair by showing the components are equal

[Timothy Chow]

Aaron Liu said:

For example, if everything is a set then ext will tell you to show they're equal by they have the same elements, but what you really want is to show a pair is equal to another pair by showing the components are equal

I don't understand this comment. The Kuratowski pair definition is designed exactly for this purpose.
{{x},{x,y}} = {{x'},{x',y'}} as sets (i.e., if and only if they have the same elements) if and only if x=x' and y=y'.

[Aaron Liu]

You want ext to take you to x = x' and y = y' but what it will do is it will introduce a new variable and if you name it with ext s instead of just ext then you will have the goal s ∈ {{x},{x,y}} ↔ s ∈ {{x'},{x',y'}}

[Timothy Chow]

But that's not how you would do it, is it? I admit I have no experience with ZFSet but I see that there exists something called ZFSet.pair which I would presume smooths over some of these basic interface issues.

[Aaron Liu]

That doesn't solve the problem since you will still get something like s ∈ pair x y ↔ s ∈ pair x' y', what we really want is x = x' and y = y'

[Timothy Chow]

Okay, again I have no experience with ZFSet, but my intuition is that if this is causing problems then it's because ZFSet.pair is not implemented as well as it could be, not because there's something intrinsically technically difficult about working with sets. But I will have to defer to more knowledgeable people.

[James E Hanson]

Aaron Liu said:

That doesn't solve the problem since you will still get something like s ∈ pair x y ↔ s ∈ pair x' y', what we really want is x = x' and y = y'

How is this any different from any other kind of working with lemmas on defined notation? You introduce notation for the ordered pair, you prove a lemma that the ordered pair works, and then you proceed.

[Kenny Lau]

how is {{x},{x,y}} "badly implemented", it's like the standard definition (at least the one that's actually good) of ordered pairs inside set theory

[Kenny Lau]

it's the usual stuff about ordered pairs in set theory that is hard, nothing to do with the implementation of ZFSet. the proof that {{x},{x,y}} is correct in set theory is already a bit messy

or rather, it's set theory itself that's messy, that's why we all switched to type theory

[Timothy Chow]

Kenny Lau said:

the proof that {{x},{x,y}} is correct in set theory is already a bit messy

I don't understand why this is relevant. Shouldn't the proof be buried in the library as a lemma somewhere so that users don't have to worry about it? As James Hanson said, I don't see how this is different from working with any other defined notion.

[Timothy Chow]

Kenny Lau said:

or rather, it's set theory itself that's messy, that's why we all switched to type theory

This is definitely not true, as Larry Paulson and John Harrison and Bohua Zhan and even Jeremy Avigad will assure you.

[Timothy Chow]

By the way, in the same discussion that I quoted above, Larry Paulson briefly describes how to work with Kuratowski pairs in Isabelle. If there's something klunky with the Lean implementation of ZFSet then I suspect we could ask Larry Paulson for advice, since he has a lot of experience with working with sets inside a type-theoretic proof assistant.

[Aaron Liu]

James E Hanson said:

Aaron Liu said:

That doesn't solve the problem since you will still get something like s ∈ pair x y ↔ s ∈ pair x' y', what we really want is x = x' and y = y'

How is this any different from any other kind of working with lemmas on defined notation? You introduce notation for the ordered pair, you prove a lemma that the ordered pair works, and then you proceed.

Usually when working with ordered pairs you can tell from the type whether a term is a pair or not

[Aaron Liu]

but with ZFSet it's all sets

[Violeta Hernández]

Timothy Chow said:

I think James Hanson is asking whether there is anything more to the complaint about Kuratowski pairs than "set theory is icky and I don't like working with it."

Not really. I just happen to believe that the fact sets can embed so many structures doesn't mean they're the most natural way to describe said structures.

[Bhavik Mehta]

Aaron Liu said:

You want ext to take you to x = x' and y = y' but what it will do is it will introduce a new variable and if you name it with ext s instead of just ext then you will have the goal s ∈ {{x},{x,y}} ↔ s ∈ {{x'},{x',y'}}

I don't think you do want ext to do this though. With Lean's (type-theoretic) ordered pairs, if I have the goal (x, y) = (x', y'), then I don't expect ext to take me to x = x' and y = y'; I expect simp or similar to do that. And similarly I'd wouldn't expect ext on ZFSet.pair x y = ZFSet.pair x' y' to take me to x = x' and y = y'; I expect simp to do that. And this is something that already happens: docs#ZFSet.pair_inj.
So, as others have said, I'm not entirely sure there's a technical difficulty with working with zf sets in Lean, except for the usual difficulties you get when embedding one theory in another, and peoples' personal taste

[Aaron Liu]

Maybe not for pairs, but surely for functions you would want ext to do something nice. But I expect this won't happen for the ZFSet encoding of functions, whatever that may be, since I think it will use the generic ext lemma instead of the one for the encoded functions.

[Aaron Liu]

so this is what happens when everything is the same type, is that you lose typing information that may be useful

[Kenny Lau]

well some people wanted ext to be more customisable
(i think i remembered that wrong, but it would be nice)

[Violeta Hernández]

I'd like to point out that if you want to work in pure ZFC you want Metamath, not Lean.

[Robert Maxton]

Bhavik Mehta said:

I don't think you do want ext to do this though. With Lean's (type-theoretic) ordered pairs, if I have the goal (x, y) = (x', y'), then I don't expect ext to take me to x = x' and y = y'; I expect simp or similar to do that. And similarly I'd wouldn't expect ext on ZFSet.pair x y = ZFSet.pair x' y' to take me to x = x' and y = y'; I expect simp to do that. And this is something that already happens: docs#ZFSet.pair_inj.
So, as others have said, I'm not entirely sure there's a technical difficulty with working with zf sets in Lean, except for the usual difficulties you get when embedding one theory in another, and peoples' personal taste

If that's not what you expect ext to do, then what should it ever do? It's admittedly not often that I equate data structures in Lean, but when I do, I absolutely expect ext to convert an equality of structures into a conjunction of equalities for each projection, which in this case is x = x' and y = y'. That's not simp's job, and in fact simp is bad at opening goals like that.

And indeed,

example {α} (a b c d : α) : (a, b) = (c, d) := by
  ext

leaves you with the two goals (a, b).fst = (c, d).fst, (a, b).snd = (c, d).snd.

[Timothy Chow]

Robert Maxton said:

I absolutely expect ext to convert an equality of structures into a conjunction of equalities for each projection, which in this case is x = x' and y = y'.

I'm not familiar with ext, so some of the nuances of this discussion are going over my head. But let's suppose I agree with you. Given that ZFSet.pair already exists in mathlib, and that ext "should" behave the way you indicate here, what's standing in the way of making it behave that way?

[Aaron Liu]

well ext only looks at the type of the terms, so it can't use one lemma for generic sets and another lemma for sets that represent a pair

[Kevin Buzzard]

To expand on what Aaron is saying -- I can't remember the details but someone once showed me a very cute construction of ordered pairs in set theory whereby every set becomes an ordered pair (edit: Gemini found it, it's the Quine-Rosser definition ). Say mathlib had used that encoding. Then faced with a goal a = b of ZFSets, the ext tactic doesn't know whether to turn it into "z is an element of a iff it's an element of b" or "a.1 = b.1 and a.2 = b.2". In type theory when faced with a goal a = b of ordered pairs you can look at the type of a and see it's X x Y (every term has a unique type in type theory) and then you know which extensionality lemma to use.

[Timothy Chow]

Okay, I think I'm beginning to understand, but now my inclination is to agree with Bhavik that for sets, I would not expect a tactic named ext to reduce equality of a Kuratowski ordered pair to equality of the components.

For a different kind of example, suppose H and K are subgroups of a group G, and my goal is to prove H = K. If I have a set-theoretic mindset, then what might I naively expect a tactic named ext to do to my goal? My first instinct is that it would reduce my goal to two goals, the first showing that if x is in H then x is in K, and the second showing that if x is in K then x is in H. If you buy that, then ext should do something similar with Kuratowski ordered pairs.

That's not to say that it wouldn't be useful to have some tactic that reduces equality of Kuratowski ordered pairs to equality of the "components," just that it's not obvious to me that such a tactic should be named ext.

[Aaron Liu]

Timothy Chow said:

For a different kind of example, suppose H and K are subgroups of a group G, and my goal is to prove H = K. If I have a set-theoretic mindset, then what might I naively expect a tactic named ext to do to my goal? My first instinct is that it would reduce my goal to two goals, the first showing that if x is in H then x is in K, and the second showing that if x is in K then x is in H.

In this example, ext will introduce a new variable of type G, and if you name it by writing ext x instead then you will have the goal x ∈ H ↔ x ∈ K

[Aaron Liu]

Timothy Chow said:

If you buy that, then ext should do something similar with Kuratowski ordered pairs.

What does this mean? What is the similar thing that it should do? Why are you specifying Kuratowski ordered pairs do you not expect this for some other kind of ordered pairs?

[Timothy Chow]

It means that it should reduce to two goals. The first is that if z is in {{x},{x,y}} then z is in {{x'},{x',y'}}, and the second is that if z is in {{x'},{x',y'}} then z is in {{x},{x,y}}.

I'm not sure what you mean by "some other kind of ordered pairs." I'm using the name "Kuratowski" for emphasis only. In set theory, there is no other kind of ordered pair.

[Violeta Hernández]

a) We already have a tactic that does this. It's called simp.
b) There are a lot of potential ordered pair definitions. Products in the category of sets are far from unique. Kuratowski just happened to catch on as semi-standard convention.

[Timothy Chow]

Ah, now I see what Aaron Liu might have meant by "other kinds of ordered pairs." If that is what is meant, then yes, I'm just saying what my instincts are for Kuratowski ordered pairs. If we're talking about some kind of categorical product, then I'm not sure what I would expect ext to do.

[James E Hanson]

Kevin Buzzard said:

every term has a unique type in type theory

Strictly speaking this depends on the type theory in question. Some type theories have subtyping (e.g., universe subtyping in Rocq).

[James E Hanson]

Violeta Hernández said:

semi-standard convention.

Why do you say 'semi-standard'? I feel like it's fairly established as the standard definition in set theory.

[James E Hanson]

Kevin Buzzard said:

"z is an element of a iff it's an element of b" or "a.1 = b.1 and a.2 = b.2"

These are pretty directly equivalent goals for the Quine-Rosser pair though.

[James E Hanson]

Specifically, a.1 = b.1 is equivalent to "for any $z$ not containing $\varnothing$, $z \in a$ iff $z \in b$" and a.2 = b.2 is equivalent to "for any $z$ containing $\varnothing$, $z \in a$ iff $z \in b$".

[Timothy Chow]

Violeta Hernández said:

a) We already have a tactic that does this. It's called simp.

I'm trying to understand why Robert Maxton says that this sort of thing is not what simp is supposed to do; it's what ext is supposed to do. (At least, that's what I think he's saying.) If ext is supposed to be reminiscent of the axiom of extensionality in set theory, then I do have some intuitions about that, as I have indicated above.

But without understanding the philosophy behind simp I can't intelligently comment on what it "should" be doing. I have used simp a few times, but only as a sorcerer's apprentice, uttering magical incantations without really knowing what I'm doing.

[Kevin Buzzard]

I don't see how Lean's ext tactic as it stands can do anything for ZFSet other than applying set extensionality, because its behaviour depends solely on the type of the objects in the goal. No doubt one can write a different extensionality tactic which is specific to ZFSet, but that's not ext, it's something else.

Whether a.pair b = a'.pair b' <-> a = a' \and b = b' should be a simp lemma will depend on how the ZFSet part of the library is designed. In the part of mathlib which I do understand, I will typically know what the "simp normal form" of an expression is. Whether you want simp to start messing with a.pair b will depend a lot on how this term is used in practice. These questions are delicate. For example when one is making the basic API for complex numbers it's super-useful to have the simplifier turning z = w into z.re = w.re \and z.im = w.im because that's how you're proving every ring axiom for the complexes. However the moment you're beyond this, simp turning z = w into z.re = w.re \and z.im = w.im would be a disaster, because if one is doing some complicated calculation with complex numbers then probably the last thing you want to do is to start comparing real and imaginary parts.

What is absolutely clear is that a.pair b = a'.pair b' <-> a = a' \and b = b' should be a lemma, and rewriting that lemma is a perfectly satisfactory way of making progress here. Making it a simp lemma could perhaps be something which one could experiment with, and it might be more of a sociological experiment than anything else -- one will probably discover pretty quickly whether one wants the simplifier to do this or not.

[Violeta Hernández]

James E Hanson said:

Violeta Hernández said:

semi-standard convention.

Why do you say 'semi-standard'? I feel like it's fairly established as the standard definition in set theory.

I've seen ⟨a, b⟩ = {a, {a, b}} about as often. I've seen people omit either definition much more. It's ultimately just an implementation detail.

[Timothy Chow]

Violeta Hernández said:

I've seen ⟨a, b⟩ = {a, {a, b}} about as often.

This definition doesn't work properly in the absence of the axiom of foundation, does it? Can't you have something like a = {a',b'} and a' = {a,b} so that {a, {a,b}} = {a', {a',b'}} without a = a' and b = b'?

[Aaron Liu]

So you're saying it works when we have the axiom of foundation

[Kevin Buzzard]

See the comments on $(a,b)_{short}$ at https://en.wikipedia.org/wiki/Ordered_pair#Variants

[Timothy Chow]

Aaron Liu said:

So you're saying it works when we have the axiom of foundation

Yes, it does, but the point is that it's certainly not "standard," and under most circumstances, there's no good reason to use it. Usually, when I've seen it, it's a typo, or written by someone who doesn't appreciate the subtle point about foundation. There might be some specialized circumstances where it has some definite advantages, but again, it's not "standard." Just like there are infinitely many ways that one can write down axioms for a group, but most of them are nonstandard.

[Aaron Liu]

well if it shows up a lot then it's a standard

[Timothy Chow]

Aaron Liu said:

well if it shows up a lot then it's a standard

I'm not sure what point you're trying to make. James Hanson, who is an expert in foundations and knows a lot about set theory, was trying to understand why Violeta was calling the definition "semi-standard" when in his experience (and mine, for what that's worth, though I don't know as much set theory as James does), it's standard. I would say that the alternative proposed by Violeta shows up very rarely in careful treatments of set theory. I have seen many people write it that way, but as I said, usually by mistake. By analogy, I see the spellings "accomodation" and "occurence" a lot, but that doesn't automatically make those spellings standard.

But I would be interested if you can cite (for example) several graduate textbooks in set theory that use the {x, {x,y}} definition. That would be good evidence that {x, {x,y}} is just as standard a definition as {{x}, {x,y}}.

[Violeta Hernández]

The point I was trying to make is that there are a lot of potential options. If one is preferred over the others the reasons are largely historical.

[Violeta Hernández]

I could well imagine some more categorical treatment of set theory, where one first proves "there are products in the category of sets", gives whichever construction as an example, then just uses ⟨a, b⟩ to refer to elements of an arbitrary product.

[Violeta Hernández]

Ultimately the nice thing about not working with ZFSet is that we don't have to quabble over these arbitrary choices. We have a constructor which makes a game out of two other sets of games; its implementation is for the purposes of the mathematics completely opaque.

[James E Hanson]

Violeta Hernández said:

I've seen ⟨a, b⟩ = {a, {a, b}} about as often.

Where have you seen this? I just googled 'set theory textbooks' and checked all of the books I found listed that I could get my hands on, and all of them either used the $\{\{x\},\{x,y\}\}$ Kuratowski pair definition or (in one case) took ordered pairs as a primitive notion. In particular, all of these books use that definition.

• Set Theory: An Open Introduction by the Open Logic Project.
• Elements of Set Theory by Enderton
• Set Theory by Jech
• Introduction to Set Theory by Hrbacek and Jech
• Naive Set Theory by Halmos
• Basic Set Theory by Levy
• Intermediate Set Theory by Drake and Singh
• Axioms and Set Theory: A first course in Set Theory by André

Enderton mentions the Wiener pair definition but then said that the Kuratowski pair is 'in general use today'. I also asked ChatGPT what the standard definition of ordered pairs in set theory is, and it said the $\{\{x\},\{x,y\}\}$ Kuratowski pair.

Only Book of Proof by Hammack didn't use this definition, and instead seemed to take ordered pairs as a primitive concept.

The only place I ever see the $\{x,\{x,y\}\}$ definition is in conversations about different definitions of ordered pairs or the history of set theory, on Wikipedia (which is trying to present an encyclopedic account of different definitions people have proposed), and in the one textbook (Lectures in Logic and Set Theory. Vol. 2: Set Theory by Tourlakis) and Metamath proof Wikipedia cites. (Note that Wikipedia also refers to the Kuratowski pair as the 'now-accepted definition'.) Other than that, the Quine-Rosser definition and (extremely rarely, as in literally in 2 papers I can think of, one of which is mine) the Wiener definintion show up in some places for technical reasons.

I understand that this is not that important. I understand that in the context of formalizing the surreal numbers in Lean, set-theoretic ordered pairs don't make sense. The reason I am touchy about this is that, as someone in the general cultural sphere of set theory, I find it extremely obnoxious when people outside the area insist (seemingly on the basis of vibes) that it hasn't decided on a standard definition (as Kevin quite aggressively and unpleasantly did the last time this topic came up). If you ask set theorists or classical mathematical logicians more generally whether there's a 'standard' set-theoretic ordered pair, the vast majority of them will tell you yes and say that it's $\{\{x\},\{x,y\}\}$. It is the standard definition in set theory by any reasonable social notion of 'standard definition'.

[Aaron Liu]

ok, maybe Kuratowski pairs are standard

[Aaron Liu]

does that change anything?

[James E Hanson]

Aaron Liu said:

does that change anything?

I feel like this question is not a response to my point.

[Aaron Liu]

what is your point?

[James E Hanson]

I feel like I communicated my point pretty clearly in the last paragraph of my earlier message.

[Aaron Liu]

oh yes sorry I see it now

[Violeta Hernández]

I concede that I was under the impression Kuratowski was somewhat less agreed-upon. But my use of the word semi-standard was also intended to call attention to the fact that there is no strictly mathematical reason to prefer this definition over others in the context of ZFC.

[James E Hanson]

That's not how the phrase 'standard definition' is used in math.

[James E Hanson]

(deleted)

[Violeta Hernández]

Sure, but $\{\{y\}, \{x, y\}\}$ is an equally robust definition, as is $\{\{\{x\},\varnothing\},\{\{y\}\}\}$, or perhaps $\{\{0, \{\{x\}\}\}, \{1,\{\{y\}\}\}\}$, etc.

[James E Hanson]

Sorry, I didn't see that you said ZFC specifically.

[James E Hanson]

I just don't get why set theory gets put under such an intense microscope in this context.

If we were talking about some place in algebra where there was a technically arbitrary sign convention, would you also go out of your way to refer to an established convention as 'semi-standard'?

[James E Hanson]

Or, rather, I feel like I do get why set theory is treated this way and I feel like it has to do with people thinking of it as 'not really being mathematics' (cf. Kevin's comments last time this conversation happened about basic things in set theory being 'wiring' rather than 'mathematics').

[James E Hanson]

Or your phrasing just now about 'strictly mathematical reason'.

[James E Hanson]

I had to use the Wiener pair instead of the Kuratowski pair in one of my papers for technical reasons. Was the reason I had to do that not 'mathematical'?

[James E Hanson]

Admittedly this was not in the context of ZFC, but whenever people start talking about these basic things from set theory this way, I always feel like there's a certain degree of 'set theory is not mathematics' subtext.

[Violeta Hernández]

My main gripe with set theory is that in my eyes it has a bad habit of glorifying arbitrary choices of encoding. An ordered pair can be encoded via Kuratowski just as a natural number can be encoded via Zermelo or as an ordinal can be encoded via von Neumann, but all of these choices are far from unique and very rarely relevant.

[James E Hanson]

The von Neumann definition has meaningful technical advantages when you pass to arbitrary ordinals rather than just natural numbers.

[James E Hanson]

It's not arbitrary.

[James E Hanson]

You're just insisting that it's arbitrary because you don't respect the mathematical ideas in set theory.

[Violeta Hernández]

Mathlib has a lot of work done on docs#Ordinal, and none of it depends on von Neumann's definition.

[James E Hanson]

(deleted)

[Violeta Hernández]

I respect the mathematics, my point is that the encodings themselves aren't all that important.

[James E Hanson]

You don't respect the mathematics if you insist that people in the field are thinking about it incorrectly in a fundamental way.

[James E Hanson]

Or rather you don't respect the people in the field.

[Violeta Hernández]

I apologize if any of this has come off as a personal attack. That's far from my intention.

[James E Hanson]

I am sorry for being difficult. I just find this attitude extremely frustrating.

[James E Hanson]

It's kind of condescending.

[James E Hanson]

'All these basic conventions in your field are wrong and not really mathematics.'

[James E Hanson]

Can't you see why this is maybe a bit insulting?

[James E Hanson]

Like do you know anything about inner model theory? Do you know the condensation lemma?

[James E Hanson]

There's a reason why 'structural' set theory never took off among set theorists as a formalism. It makes very basic ideas in the area extremely awkward.

[Violeta Hernández]

Well, my argument isn't that the conventions are wrong. My ultimate point is that we could have gone with any of them with largely the same result.

[James E Hanson]

I'm not talking about ordered pairs now. I'm talking about ordinals.

[James E Hanson]

The von Neumann ordinal definition is natural. It's more natural than the Kuratowski pair.

[James E Hanson]

It's a canonical notion.

[Violeta Hernández]

Model theory is an area I am somewhat interested in, but my knowledge is superficial. It does feel a bit insulting that you'd attack my intelligence rather than my actual words.

[Violeta Hernández]

James E Hanson said:

The von Neumann ordinal definition is natural. It's more natural than the Kuratowski pair.

Perhaps I can rephrase: one can develop the entirety of ordinal arithmetic without reference to an encoding. The characterizing property of ordinals is that they are a skeleton for the category of well-orders, and that's enough to get the ball rolling.

[James E Hanson]

I did not mean to attack your intelligence. I'm trying to say that there are reasons for preferring something like the von Neumann ordinal definition that you only really get to after, say, a semester of graduate set theory.

[Violeta Hernández]

I guess we're talking about different usages of the same concept

[James E Hanson]

Also, this is a common misconception, but 'inner model theory' isn't really a kind of model theory. It's just a part of set theory.

[Riccardo Brasca]

Dear all, online communication is always difficult and it's easy to misinterpret the tone or the intentions of a message. I am confident that nobody wanted to insult anybody in this discussion and I propose to keep it at a scientific level.

[Violeta Hernández]

I think I can state my point while remaining within the confines of the original discussion. It is somewhat more natural to define games as we do in the CGT repo (as an inductive type where two sets of games create a new one) than it is to define it as a subtype of ZFSet, since the latter involves a choice of pair encoding that is far from unique.

[James E Hanson]

Violeta Hernández said:

Model theory is an area I am somewhat interested in, but my knowledge is superficial.

In any case, my main area is actually model theory. It can be a hard area to learn about without talking to people already familiar with the material. If you have questions about model theory at some point in the future, I'd be more than happy to answer them.

[Violeta Hernández]

Thank you! I do actually have one question: is there some good introductory reference for the topic?

[James E Hanson]

Unfortunately, kind of no.

[James E Hanson]

The closest is maybe Maker's book, but it's notoriously full of typos and is somewhat outdated at this point.

[Violeta Hernández]

Hm, that's unfortunate. But thanks