Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorYimingXu
   • CommentTimeApr 28th 2022
   • (edited Apr 29th 2022)
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexI read the [[surreal number]] on nlab and it is written there: > It is a routine matter to rewrite the definitions in a more structural fashion, say within ETCS. In outline, a game is a rooted tree with no infinite branches and equipped with a labeling of each edge by a symbol $L$ or $R$. and >In this set-up, the condition of no infinite branches plays the role of a foundation axiom, and inductive arguments tend to devolve upon the use of the principle of dependent choice. But it is not the fact that any surreal number is a tree with finite depth, and many interesting results comes after depth $\omega$, therefore, it seems to me that the tree approach cannot formulate all the surreal numbers (unless we use something like a "transfinite tree", whose definition in SEAR is not obvious to me as well.) but only all the surreals which is created on day $n\in\omega$. (Thanks for correcting me if I am already wrong here.) I think there remains hope to capture "all of the surreals", using the approach [here](https://en.wikipedia.org/wiki/Surreal_number#Alternative_realizations) But again, as there is no universally approved notion of ordinals in structural set theory, we can only formulate ordinals with some base $A$, in the sense that an $A$ ordinal is an equivalence class of well-orders on $A$.I think this gives hope to formulate $A$-based surreals as functions from $A$-ordinals. Is there any suggested approach to define the whole collection of surreals in structual set theory like SEAR or ETCS? Another question is that: If we can capture surreals in SEAR perfectly, then we should be able to prove that each ordinal can be represented as a surreal. Since ordinals cannot be captured perfectly, "each ordinal can be represented as a surreal" will have an alternative statement as for surreals in SEAR. What would that statement be? Does it sound plausible to use "ordinals with some base" instead?

   I read the surreal number on nlab and it is written there:

   It is a routine matter to rewrite the definitions in a more structural fashion, say within ETCS. In outline, a game is a rooted tree with no infinite branches and equipped with a labeling of each edge by a symbol $L$ or $R$.

   and

   In this set-up, the condition of no infinite branches plays the role of a foundation axiom, and inductive arguments tend to devolve upon the use of the principle of dependent choice.

   But it is not the fact that any surreal number is a tree with finite depth, and many interesting results comes after depth $\omega$, therefore, it seems to me that the tree approach cannot formulate all the surreal numbers (unless we use something like a “transfinite tree”, whose definition in SEAR is not obvious to me as well.) but only all the surreals which is created on day $n\in\omega$. (Thanks for correcting me if I am already wrong here.)

   I think there remains hope to capture “all of the surreals”, using the approach here

   But again, as there is no universally approved notion of ordinals in structural set theory, we can only formulate ordinals with some base $A$, in the sense that an $A$ ordinal is an equivalence class of well-orders on $A$.I think this gives hope to formulate $A$-based surreals as functions from $A$-ordinals.

   Is there any suggested approach to define the whole collection of surreals in structual set theory like SEAR or ETCS?

   Another question is that: If we can capture surreals in SEAR perfectly, then we should be able to prove that each ordinal can be represented as a surreal. Since ordinals cannot be captured perfectly, “each ordinal can be represented as a surreal” will have an alternative statement as for surreals in SEAR. What would that statement be? Does it sound plausible to use “ordinals with some base” instead?

2. • CommentRowNumber2.
   • CommentAuthorHurkyl
   • CommentTimeApr 28th 2022
   • (edited Apr 28th 2022)
   • PermaLink
   Author: Hurkyl
   Format: MarkdownItexThe prohibition against infinite branches does not force the tree to have finite depth -- just that each vertex has finite depth. For example, if we consider the ordinals in surreal numbers, the ordinal $\omega + 1$ can be constructed with right set $\omega \cup \{ \omega \}$. Each of the elements of $\omega$ is a finite tree so all of the vertices below those children have finite depth. The remaining child $\omega$ has all of its elements finite trees, so all of the vertices below that child also have finite depth.

   The prohibition against infinite branches does not force the tree to have finite depth – just that each vertex has finite depth.

   For example, if we consider the ordinals in surreal numbers, the ordinal $\omega + 1$ can be constructed with right set $\omega \cup \{ \omega \}$. Each of the elements of $\omega$ is a finite tree so all of the vertices below those children have finite depth. The remaining child $\omega$ has all of its elements finite trees, so all of the vertices below that child also have finite depth.

3. • CommentRowNumber3.
   • CommentAuthorYimingXu
   • CommentTimeApr 28th 2022
   • (edited Apr 29th 2022)
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexThanks for replying! So $\omega$ is not a tree of infinite depth but a tree with infinite branches, and therefore we can only get such "horizontally transfinite tree"? How can we uniformly represent such trees in SEAR, or it is just the fact that we cannot? More precisely, in material set theory, a surreal number is a set, and what is a surreal in SEAR (what is its type? a set, an element, or an relation)? If a surreal number is realised as a tree, then I think every of such surreal should be a member of some set such that each member of this set is a tree. How can we construct such "sets of trees"? I am feeling maybe using functions from ordinals might be easier, still not so sure.

   Thanks for replying!

   So $\omega$ is not a tree of infinite depth but a tree with infinite branches, and therefore we can only get such “horizontally transfinite tree”? How can we uniformly represent such trees in SEAR, or it is just the fact that we cannot? More precisely, in material set theory, a surreal number is a set, and what is a surreal in SEAR (what is its type? a set, an element, or an relation)?

   If a surreal number is realised as a tree, then I think every of such surreal should be a member of some set such that each member of this set is a tree. How can we construct such “sets of trees”? I am feeling maybe using functions from ordinals might be easier, still not so sure.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeMay 1st 2022
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexExactly what set is a surreal number in material set theory? I think if you answer that question precisely, you'll find that the same construction works in any structural set theory. (Modulo issues of size.)

   Exactly what set is a surreal number in material set theory? I think if you answer that question precisely, you’ll find that the same construction works in any structural set theory. (Modulo issues of size.)

5. • CommentRowNumber5.
   • CommentAuthorYimingXu
   • CommentTimeMay 1st 2022
   • (edited May 1st 2022)
   • PermaLink
   Author: YimingXu
   Format: MarkdownItexIf so, I am still confused that: 1.Surreals defined before $\omega$-th day is constructed via natural number recursion, afterwards it requires transfinite recursion, how is such transfinite stuff captured in SEAR? In material set theory we can write $\forall n\in N. issurreal(n,(L,R)) \Leftrightarrow (\forall a. a\in L \implies \exists n_1,n1 \lt n\wedge issurreal(n_1,a) )\wedge (\forall a. a\in R \implies \exists n_2,n2\lt n \wedge issurreal(n_2,a))$ This will not type-check in SEAR. I am interested in how can I write this as formal as in a theorem prover. 2.Sets in material set theory have equality, which makes it possible to compare them and doing arithmetic, whereas the claim is that there is no equality between sets in SEAR, are we using bijections instead?

   If so, I am still confused that:

   1.Surreals defined before $\omega$-th day is constructed via natural number recursion, afterwards it requires transfinite recursion, how is such transfinite stuff captured in SEAR?

   In material set theory we can write $\forall n\in N. issurreal(n,(L,R)) \Leftrightarrow (\forall a. a\in L \implies \exists n_1,n1 \lt n\wedge issurreal(n_1,a) )\wedge (\forall a. a\in R \implies \exists n_2,n2\lt n \wedge issurreal(n_2,a))$

   This will not type-check in SEAR. I am interested in how can I write this as formal as in a theorem prover.

   2.Sets in material set theory have equality, which makes it possible to compare them and doing arithmetic, whereas the claim is that there is no equality between sets in SEAR, are we using bijections instead?

6. • CommentRowNumber6.
   • CommentAuthorGuest
   • CommentTimeMay 1st 2022
   • PermaLink
   Author: Guest
   Format: MarkdownItexI'm not sure about SEAR, but for ETCS I think one has to add [[universes]] and some axiom of [[transfinite induction]] or axiom of [[transfinite construction of free algebras]] in order to make the construction of surreal numbers work.

   I’m not sure about SEAR, but for ETCS I think one has to add universes and some axiom of transfinite induction or axiom of transfinite construction of free algebras in order to make the construction of surreal numbers work.

7. • CommentRowNumber7.
   • CommentAuthorHurkyl
   • CommentTimeMay 1st 2022
   • (edited May 1st 2022)
   • PermaLink
   Author: Hurkyl
   Format: MarkdownItexMind you I'm just thinking toposes rather than SEAR, but I would respond to your questions as: "how is such transfinite stuff captured in SEAR?" You have an object $\mathbb{N}$ with a well-ordering. You can extend it to a well-ordering on $\mathbb{N} \amalg 1$. There's your ordinal $\omega + 1$. You can construct an $(\mathbb{N} \amalg 1)$-indexed family of objects by constructing an $\mathbb{N}$-indexed family of objects and another $1$-indexed family of objects. It's worth remembering even in ZFC, one doesn't have a set of Surreal numbers (although if you have a universe you could talk about the set of _small_ surreal numbers). The property "is a surreal number" is not a proposition you define on a set, but is instead a property that a set might have. So you can't expect "is a surreal number" to be a proposition you define on an object of the topos. Instead, it's a property that objects might have. Or, I suppose to be more precise, a proposition that a partially ordered object in the topos might have. "Sets in material set theory have equality, which makes it possible to compare them and doing arithmetic, whereas the claim is that there is no equality between sets in SEAR, are we using bijections instead?" The sets being used to construct surreal numbers as objects in the topos are not being encoded as objects of the topos -- they're encoded as well-founded rigid rooted trees. Or something like that; I don't recall off hand what the precise notion is. In ZFC, two sets are equal iff they have isomorphic $\in$-trees. For the surreal numbers, it's not the "collection of elements" notion of a set that matters -- it's specifically the tree structure constructed from the set with its membership relation. So you work with tree objects (e.g. as objects with a partially order satisfying properties) rather than as objects.

   Mind you I’m just thinking toposes rather than SEAR, but I would respond to your questions as:

   “how is such transfinite stuff captured in SEAR?”

   You have an object $\mathbb{N}$ with a well-ordering. You can extend it to a well-ordering on $\mathbb{N} \amalg 1$. There’s your ordinal $\omega + 1$. You can construct an $(\mathbb{N} \amalg 1)$-indexed family of objects by constructing an $\mathbb{N}$-indexed family of objects and another $1$-indexed family of objects.

   It’s worth remembering even in ZFC, one doesn’t have a set of Surreal numbers (although if you have a universe you could talk about the set of small surreal numbers). The property “is a surreal number” is not a proposition you define on a set, but is instead a property that a set might have.

   So you can’t expect “is a surreal number” to be a proposition you define on an object of the topos. Instead, it’s a property that objects might have. Or, I suppose to be more precise, a proposition that a partially ordered object in the topos might have.

   “Sets in material set theory have equality, which makes it possible to compare them and doing arithmetic, whereas the claim is that there is no equality between sets in SEAR, are we using bijections instead?”

   The sets being used to construct surreal numbers as objects in the topos are not being encoded as objects of the topos – they’re encoded as well-founded rigid rooted trees. Or something like that; I don’t recall off hand what the precise notion is. In ZFC, two sets are equal iff they have isomorphic $\in$-trees.

   For the surreal numbers, it’s not the “collection of elements” notion of a set that matters – it’s specifically the tree structure constructed from the set with its membership relation. So you work with tree objects (e.g. as objects with a partially order satisfying properties) rather than as objects.

8. • CommentRowNumber8.
   • CommentAuthorMike Shulman
   • CommentTimeMay 1st 2022
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexRight, instead of talking about surreals as untyped ordered pairs related to an ordinal by a relation, you consider them as an indexed family of tree-structured sets indexed by a well-ordering.

   Right, instead of talking about surreals as untyped ordered pairs related to an ordinal by a relation, you consider them as an indexed family of tree-structured sets indexed by a well-ordering.

9. • CommentRowNumber9.
   • CommentAuthorYimingXu
   • CommentTimeMay 1st 2022
   • (edited May 1st 2022)
   • PermaLink
   Author: YimingXu
   Format: TextThank you for all of these answers! Now I think I conclude that a surreal is a surjective map A to W, such that W is a well ordered set and each fiber has a tree structure. Formally, I write, A -> W such that, for all w in W and the set sw which is the subset of A that is mapped to w, there exists a relation, which is a member of Pow (A times A), such that it is a well order when restricted to sw and for any initial segments of sw, it restrictes to a well order on that initial segment. Please correct me if I am wrong.

   Thank you for all of these answers! Now I think I conclude that a surreal is a surjective map A to W, such that W is a well ordered set and each fiber has a tree structure. Formally, I write,
   
   A -> W such that, for all w in W and the set sw which is the subset of A that is mapped to w, there exists a relation, which is a member of Pow (A times A), such that it is a well order when restricted to sw and for any initial segments of sw, it restrictes to a well order on that initial segment.
   
   Please correct me if I am wrong.