Formalize these definitions about surreal numbers

Question

Please formalize these word definitions about surreal numbers into the language of ZFC/FOL (no classes if possible).

Definition 1. A surreal number is a pair of sets of previously created surreal numbers. The sets are known as the “left set” and the “right set”. No member of the right set may be less than or equal to any member of the left set.

Definition 2. A surreal number x is less than or equal to a surreal number y if and only if y is less than or equal to no member of x’s left set, and no member of y’s right set is less than or equal to x.

Source here (p. 6-7)

Answer 1

The standard way of formalizing notions by recursion is by introducing a rank. We then talk, for $\alpha$ an ordinal, of "surreals of rank at most $\alpha$", and define an ordering (that also depends on $\alpha$) among them. In terms of this notion, a surreal is, by definition, "a surreal of rank at most $\alpha$ for some ordinal $\alpha$". Also, we say that something is "a surreal of rank smaller than $\beta$" if and only if it is a surreal of rank at most $\alpha$ for some $\alpha<\beta$, and that it is "a surreal of rank $\alpha$" if and only if it is a surreal of rank at most $\alpha$ but not one of rank smaller than $\alpha$.

Specifically, we would say that a surreal number of rank at most $\alpha$ is a pair of sets of surreal numbers of rank smaller than $\alpha$. "Pair" here means ordered pair, but instead of the usual notation $(L,R)$, the book writes this as $\{L\mid R\}$. Note that if $\alpha\le\beta$, any surreal of rank at most $\alpha$ is also a surreal of rank at most $\beta$.

We define $x\le_\alpha y$, for $x=\{L_x\mid R_x\}$ and $y=\{L_y\mid R_y\}$ surreal numbers of rank at most $\alpha$, if and only if there is no $\beta<\alpha$ and $z\in L_x$ of rank at most $\beta$ such that $y\le_\beta z$, and there is no $\gamma<\alpha$ and $w\in R_y$ of rank at most $\gamma$ such that $w\le_\gamma x$. One checks the compatibility requirement that if $\alpha\le\delta$ and $x,y$ are surreals of rank at most $\alpha$, then $x\le_\alpha y$ if and only if $x\le_\delta y$. So, for $x,y$ surreals, we say that $x\le y$ if and only if $x\le_\alpha y$ for some $\alpha$, and the compatibility requirement ensures that this definition is independent of $\alpha$, that is, it either fails for all $\alpha$, or it holds from some $\alpha$ on.

This sort of definition may look somewhat technical the first time it is encountered, but I want to emphasize that it is really standard. Well-foundedness and ranks pervade just about every aspect of set theory. To mention a reference: Kunen's book on set theory treats recursion carefully and has several examples of definitions of this sort.

Answer 2

Here is a formalization of Conway's rules:

Define $(\mathbf{S},\mathcal{O})$, where $\mathcal{O} \subset \mathbf{S} \times \mathbf{S}$ represents the relation $\leq$, as the inductive structure defined by the rules:

1) If $L,R$ are sets with $L \times R \subset \mathcal{O}$ and $(R \times L) \cap \mathcal{O}=\varnothing$, then $(L,R)$ lies in $\mathbf{S}$.

2) Given such sets $L,R$ and $L',R'$, if $(\{(L',R')\} \times L) \cap \mathcal{O}= (R' \times \{(L,R)\}) \cap \mathcal{O} = \varnothing$, then $((L,R),(L',R'))$ lies in $\mathcal{O}$.

This means that $(\mathbf{S},\mathcal{O})$ is the smallest system satisfying those two rules. Its existence can be derived by defining $(\mathbf{S},\mathcal{O})$ inductively as the union of set-sized systems $S_{\alpha},O_{\alpha}$ of rank $\alpha$ for any ordinal $\alpha$. Define $S_0=O_0=\varnothing$ and take unions at limit ordinals. For successor $\alpha=\beta+1$, define $S_{\alpha}$ as the union of $S_{\beta}$ with all elements $(L,R)$ satisfying rule 1) with $L,R \subseteq S_{\beta}$ and $O_{\alpha}$ as the union of $O_{\beta}$ and all elements $((L,R),(L',R'))$ satisfying rule 2 with $L,R,L',R' \subseteq S_{\beta}$.

Then one has to take the quotient of $\mathbf{S}$ under the relation $\mathcal{O} \cap \mathcal{O}^{-1}$ to obtain $\mathbf{No}$. The order is compatible with this quotient and yields the usual order on $\mathbf{No}$.

---

If you are looking for other definitions, there's Harry Gonshor's presentation in terms of sign sequences, Norman Alling's construction using Hahn series and his axiomatic characterization, Philip Ehrlich's characterization as a class-sized saturated real-closed field and also the latter's stronger characterization (up to unique isomorphism) as a lexicographically ordered tree.