0
$\begingroup$

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)

$\endgroup$
  • $\begingroup$ These are straightforward (if messy) definitions by simultaneous transfinite recursion - is there a particular point which is causing difficulty? $\endgroup$ – Noah Schweber Dec 19 '19 at 17:27
  • $\begingroup$ @NoahSchweber I would just like to do some formal proofs about surreal numbers and can't think of how to get started. I need some formal definitions. It looks somewhat circular to my untrained eye. A link to such definitions would be nice. $\endgroup$ – Dan Christensen Dec 19 '19 at 17:32
  • 2
    $\begingroup$ The point is that we can proceed "rank-by-rank" - we define by transfinite recursion for each ordinal $\alpha$ a set $S_\alpha$ of "surreals of level $\alpha$" and an ordering $\trianglelefteq_\alpha$ on $S_\alpha$. At limit stages we take unions, and we start with $\emptyset$ for both $S_0$ and $\trianglelefteq_0$; at successor stages, we use $S_\alpha$ and $\trianglelefteq_\alpha$ to build new surreals and an ordering on those. (I didn't downvote btw.) $\endgroup$ – Noah Schweber Dec 19 '19 at 17:35
  • $\begingroup$ @NoahSchweber Umm... OK. Thanks. $\endgroup$ – Dan Christensen Dec 19 '19 at 17:36
  • $\begingroup$ Are you familiar with the precise definition of the cumulative hierarchy (that is, the construction of a formula $\theta(x,y)$ intuitively saying "$x$ is the set of sets of rank $y$" together with the proof that for each ordinal $y$ there is exactly one $x$ such that $\theta(x,y)$)? That's a simpler example of the same idea. $\endgroup$ – Noah Schweber Dec 19 '19 at 18:27
4
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$

Not the answer you're looking for? Browse other questions tagged or ask your own question.