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 or .
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 , 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 . (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 , in the sense that an ordinal is an equivalence class of well-orders on .I think this gives hope to formulate -based surreals as functions from -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?
]]>