@robjohn Well, when I do these things (vote out of fun of hitting a cap, or helping someone to a nice 80k) I would either vote for answers I can read or answers which have high vote count to begin with.
In a way, it is like the real numbers, only instead of basing them on the natural numbers (add negatives, fractions, completion) we do that on the class of ordinals.
Now, since it is perfectly fine not to assume the existence of any infinite set (or even that the natural numbers form a set), we can ask ourselves... what would be the class of the surreal numbers if we not allow infinite sets?
Well, since the ordinals are now just the natural numbers, you would expect the result to be the rationals, or something similar.
In ZF-Infinity, it is even less than the rationals. It is exactly the dyadic numbers.
@AsafKaragila I saw it now. Being mostly ignorant of surreal numbers (I've seen a definition once, but don't remember details), I mostly appreciated the by-the-way notion that NBG is the same as ZF, except that we stop constructing collections at alpha+1 rather than already at alpha.
In NBG, which is a "nice" extension of ZF which allows proper classes as objects of the universe, we can have the field as the rationals or the algebraic numbers (and so on) depending on how and what we allow in the language of the definition (order, addition, multiplication, etc)
Aha, since their question is posed in R and not R^n the biconditional holds. I missed that it was in R before, and so I missed the biconditional. In R^n the biconditional does not necessarily hold.