11.6 The surreal numbers

In this section we consider another example of a higher inductive-inductive type, which draws together many of our threads: Conway’s field $\mathrm{𝖭𝗈}$ of surreal numbers [conway:onag]. The surreal numbers are the natural common generalization of the (Dedekind) real numbers (sec:dedekind-reals) and the ordinal numbers (sec:ordinals). Conway, working in classical mathematics with excluded middle and Choice, defines a surreal number to be a pair of sets of surreal numbers, written $\{L|R\}$, such that every element of $L$ is strictly less than every element of $R$. This obviously looks like an inductive definition, but there are three issues with regarding it as such.

Firstly, the definition requires the relation of (strict) inequality between surreals, so that relation must be defined simultaneously with the type $\mathrm{𝖭𝗈}$ of surreals. (Conway avoids this issue by first defining games, which are like surreals but omit the compatibility condition on $L$ and $R$.) As with the relation $\mathrm{\sim }$ for the Cauchy reals, this simultaneous definition could a priori be either inductive-inductive or inductive-recursive. We will choose to make it inductive-inductive, for the same reasons we made that choice for $\mathrm{\sim }$.

Moreover, we will define strict inequality and non-strict inequality $\le$ for surreals separately (and mutually inductively). Conway defines in terms of $\le$, in a way which is sensible classically but not constructively. Furthermore, a negative definition of would make it unacceptable as a hypothesis of the constructor of a higher inductive type (see sec:strictly-positive).

Secondly, Conway says that $L$ and $R$ in $\{L|R\}$ should be “sets of surreal numbers”, but the naive meaning of this as a predicate $\mathrm{𝖭𝗈}\to \mathrm{𝖯𝗋𝗈𝗉}$ is not positive, hence cannot be used as input to an inductive constructor. However, this would not be a good type-theoretic translation of what Conway means anyway, because in set theory the surreal numbers form a proper class, whereas the sets $L$ and $R$ are true (small) sets, not arbitrary subclasses of $\mathrm{𝖭𝗈}$. In type theory, this means that $\mathrm{𝖭𝗈}$ will be defined relative to a universe $𝒰$, but will itself belong to the next higher universe ${𝒰}^{\prime }$, like the sets $\mathrm{𝖮𝗋𝖽}$ and $\mathrm{𝖢𝖺𝗋𝖽}$ of ordinals and cardinals, the cumulative hierarchy $V$, or even the Dedekind reals in the absence of propositional resizing. We will then require the “sets” $L$ and $R$ of surreals to be $𝒰$-small, and so it is natural to represent them by families of surreals indexed by some $𝒰$-small type. (This is all exactly the same as what we did with the cumulative hierarchy in sec:cumulative-hierarchy.) That is, the constructor of surreals will have type

$$\prod _{ℒ,ℛ:𝒰}(ℒ\to \mathrm{𝖭𝗈})\to (ℛ\to \mathrm{𝖭𝗈})\to (\text{some condition})\to \mathrm{𝖭𝗈}$$

which is indeed strictly positive.

Finally, after giving the mutual definitions of $\mathrm{𝖭𝗈}$ and its ordering, Conway declares two surreal numbers $x$ and $y$ to be equal if $x\le y$ and $y\le x$. This is naturally read as passing to a quotient of the set of “pre-surreals” by an equivalence relation. However, in the absence of the axiom of choice, such a quotient presents the same problem as the quotient in the usual construction of Cauchy reals: it will no longer be the case that a pair of families of surreals yield a new surreal $\{L|R\}$, since we cannot necessarily “lift” $L$ and $R$ to families of pre-surreals. Of course, we can solve this problem in the same way we did for Cauchy reals, by using a higher inductive-inductive definition.

Definition 11.6.1.

The type $\mathrm{No}$ of surreal numbers, along with the relations and $\mathrm{\le }\mathrm{:}\mathrm{No}\mathrm{\to }\mathrm{No}\mathrm{\to }\mathrm{U}$, are defined higher inductive-inductively as follows. The type $\mathrm{No}$ has the following constructors.

• For any $ℒ,ℛ:𝒰$ and functions $ℒ\to \mathrm{𝖭𝗈}$ and $ℛ\to \mathrm{𝖭𝗈}$, whose values we write as $x^L$ and $x^R$ for $L:ℒ$ and $R:ℛ$ respectively, if , then there is a surreal number $x$.

• For any $x,y:\mathrm{𝖭𝗈}$ such that $x\le y$ and $y\le x$, we have ${\mathrm{𝖾𝗊}}_{\mathrm{𝖭𝗈}}(x,y):x=y$.

We will refer to the inputs of the first constructor as a cut. If $x$ is the surreal number constructed from a cut, then the notation $x^L$ will implicitly assume $L\mathrm{:}\mathrm{L}$, and similarly $x^R$ will assume $R\mathrm{:}\mathrm{R}$. In this way we can usually avoid naming the indexing types $\mathrm{L}$ and $\mathrm{R}$, which is convenient when there are many different cuts under discussion. Following Conway, we call $x^L$ a left option of $x$ and $x^R$ a right option.

The path constructor implies that different cuts can define the same surreal number. Thus, it does not make sense to speak of the left or right options of an arbitrary surreal number $x$, unless we also know that $x$ is defined by a particular cut. Thus in what follows we will say, for instance, “given a cut defining a surreal number $x$” in contrast to “given a surreal number $x$”.

The relation $\mathrm{\le }$ has the following constructors.

• Given cuts defining two surreal numbers $x$ and $y$, if for all $L$, and for all $R$, then $x\le y$.

• Propositional truncation: for any $x,y:\mathrm{𝖭𝗈}$, if $p,q:x\le y$, then $p=q$.

And the relation has the following constructors.

• Given cuts defining two surreal numbers $x$ and $y$, if there is an $L$ such that $x\le y^L$, then .

• Given cuts defining two surreal numbers $x$ and $y$, if there is an $R$ such that $x^R\le y$, then .

• Propositional truncation: for any $x,y:\mathrm{𝖭𝗈}$, if , then $p=q$.

We compare this with Conway’s definitions:

• If $L,R$ are any two sets of numbers, and no member of $L$ is $\ge$ any member of $R$, then there is a number $\left\{L\right|R\}$. All numbers are constructed in this way.

• $x\ge y$ iff (no $x^R\le y$ and $x\le$ no $y^L$).

• $x=y$ iff ($x\ge y$ and $y\ge x$).

• $x>y$ iff ($x\ge y$ and $y\ngeqq x$).

The inclusion of $x\ge y$ in the definition of $x>y$ is unnecessary if all objects are [surreal] numbers rather than “games”. Thus, Conway’s is just the negation of his $\ge$, so that his condition for $\{L|R\}$ to be a surreal is the same as ours. Negating Conway’s $\le$ and canceling double negations, we arrive at our definition of , and we can then reformulate his $\le$ in terms of without negations.

We can immediately populate $\mathrm{𝖭𝗈}$ with many surreal numbers. Like Conway, we write

$$\{x,y,z,\mathrm{\dots }|u,v,w,\mathrm{\dots }\}$$

for the surreal number defined by a cut where $ℒ\to \mathrm{𝖭𝗈}$ and $ℛ\to \mathrm{𝖭𝗈}$ are families described by $x,y,z,\mathrm{\dots }$ and $u,v,w,\mathrm{\dots }$. Of course, if $ℒ$ or $ℛ$ are $\mathrm{𝟎}$, we leave the corresponding part of the notation empty. There is an unfortunate clash with the standard notation $x:A|P(x)$ for subsets, but we will not use the latter in this section.

• We define ${\iota }_{\mathbb{N}}:\mathbb{N}\to \mathrm{𝖭𝗈}$ recursively by

  ${\iota }_{\mathbb{N}}(0)$ $:\equiv \{|\},$

  ${\iota }_{\mathbb{N}}(\mathrm{𝗌𝗎𝖼𝖼}(n))$ $:\equiv \{{\iota }_{\mathbb{N}}(n)|\}.$

  That is, ${\iota }_{\mathbb{N}}(0)$ is defined by the cut consisting of $\mathrm{𝟎}\to \mathrm{𝖭𝗈}$ and $\mathrm{𝟎}\to \mathrm{𝖭𝗈}$. Similarly, ${\iota }_{\mathbb{N}}(\mathrm{𝗌𝗎𝖼𝖼}(n))$ is defined by $\mathrm{𝟏}\to \mathrm{𝖭𝗈}$ (picking out ${\iota }_{\mathbb{N}}(n)$) and $\mathrm{𝟎}\to \mathrm{𝖭𝗈}$.

• Similarly, we define ${\iota }_{\mathbb{Z}}:\mathbb{Z}\to \mathrm{𝖭𝗈}$ using the sign-case recursion principle (thm:sign-induction):

  ${\iota }_{\mathbb{Z}}(0)$ $:\equiv \{|\},$

  ${\iota }_{\mathbb{Z}}(n+1)$ $:\equiv \{{\iota }_{\mathbb{Z}}(n)|\}$ $n\ge 0$,

  ${\iota }_{\mathbb{Z}}(n-1)$ $:\equiv \{|{\iota }_{\mathbb{Z}}(n)\}$ $n\le 0$.

• By a dyadic rational we mean a pair $(a,n)$ where $a:\mathbb{Z}$ and $n:\mathbb{N}$, and such that if $n>0$ then $a$ is odd. We will write it as $a/2^n$, and identify it with the corresponding rational number. If ${\mathbb{Q}}_D$ denotes the set of dyadic rationals, we define ${\iota }_{{\mathbb{Q}}_D}:{\mathbb{Q}}_D\to \mathrm{𝖭𝗈}$ by induction on $n$:

  ${\iota }_{{\mathbb{Q}}_D}(a/2^0)$ $:\equiv {\iota }_{\mathbb{Z}}(a),$

  ${\iota }_{{\mathbb{Q}}_D}(a/2^n)$ $:\equiv \{a/2^n-1/2^n|a/2^n+1/2^n\},\text{for }n>0\text{.}$

  Here we use the fact that if $n>0$ and $a$ is odd, then $a/2^n\pm 1/2^n$ is a dyadic rational with a smaller denominator than $a/2^n$.

• We define ${\iota }_{{ℝ}_{𝖽}}:{ℝ}_{𝖽}\to \mathrm{𝖭𝗈}$, where ${ℝ}_{𝖽}$ is (any version of) the Dedekind reals from sec:dedekind-reals, by

  ${\iota }_{{ℝ}_{𝖽}}(x)$

  Unlike in the previous cases, it is not obvious that this extends ${\iota }_{{\mathbb{Q}}_D}$ when we regard dyadic rationals as Dedekind reals. This follows from the simplicity theorem (thm:NO-simplicity).

• Recall the type $\mathrm{𝖮𝗋𝖽}$ of ordinals from sec:ordinals, which is well-ordered by the relation , where means that $A=B_{/b}$ for some $b:B$. We define ${\iota }_{\mathrm{𝖮𝗋𝖽}}:\mathrm{𝖮𝗋𝖽}\to \mathrm{𝖭𝗈}$ by well-founded recursion (thm:wfrec) on $\mathrm{𝖮𝗋𝖽}$:

  $${\iota }_{\mathrm{𝖮𝗋𝖽}}(A):\equiv \{{\iota }_{\mathrm{𝖮𝗋𝖽}}(A_{/a})\text{ for all }a:A|\}.$$

  It will also follow from the simplicity theorem that ${\iota }_{\mathrm{𝖮𝗋𝖽}}$ restricted to finite ordinals agrees with ${\iota }_{\mathbb{N}}$.

• A few more interesting examples taken from Conway:

  $\omega$ $:\equiv \{\mathrm{\hspace{0.17em}0},1,2,3,\mathrm{\dots }|\}\mathit{\hspace{1em}\hspace{1em}}\text{(also an ordinal)}$

  $-\omega$ $:\equiv \{|\mathrm{\dots },-3,-2,-1,0\}$

  $1/\omega$ $:\equiv \{\mathrm{\hspace{0.17em}0}|\mathrm{\hspace{0.17em}1},\frac{1}{2},\frac{1}{4},\frac{1}{8},\mathrm{\dots }\}$

  $\omega -1$ $:\equiv \{\mathrm{\hspace{0.17em}0},1,2,3,\mathrm{\dots }|\omega \}$

  $\omega /2$ $:\equiv \{\mathrm{\hspace{0.17em}0},1,2,3,\mathrm{\dots }|\mathrm{\dots },\omega -2,\omega -1,\omega \}.$

In identifying surreal numbers presented by different cuts, the following simple observation is useful.

Theorem 11.6.2 (Conway’s simplicity theorem).

Suppose $x$ and $z$ are surreal numbers defined by cuts, and that the following hold.

• for all $L$ and $R$.

• For every left option $z^L$ of $z$, there exists a left option $x^{L^{\prime }}$ with $z^L\le x^{L^{\prime }}$.

• For every right option $z^R$ of $z$, there exists a right option $x^{R^{\prime }}$ with $x^{R^{\prime }}\le z^R$.

Then $x\mathrm{=}z$.

Proof.

Applying the path constructor of $\mathrm{𝖭𝗈}$, we must show $x\le z$ and $z\le x$. The first entails showing for all $L$, which we assumed, and for all $R$. But by assumption, for any $z^R$ there is an $x^{R^{\prime }}$ with $x^{R^{\prime }}\le z^R$ hence as desired. Thus $x\le z$; the proof of $z\le x$ is symmetric. ∎

In order to say much more about surreal numbers, however, we need their induction principle. The mutual induction principle for applies to three families of types:

$A$ $:\mathrm{𝖭𝗈}\to 𝒰$

$B$ $:{\displaystyle \prod _{(x,y:\mathrm{𝖭𝗈})}}{\displaystyle \prod _{(a:A(x))}}{\displaystyle \prod _{(b:A(y))}}(x\le y)\to 𝒰$

$C$

As with the induction principle for Cauchy reals, it is helpful to think of $B$ and $C$ as families of relations between the types $A(x)$ and $A(y)$. Thus we write $B(x,y,a,b,\xi )$ as $(x,a){\xi }^{}(y,b)$ and $C(x,y,a,b,\xi )$ as $(x,a){\mathrm{⊲}}^{\xi }(y,b)$. Similarly, we usually omit the $\xi$ since it inhabits a mere proposition and so is uninteresting, and we may often omit $x$ and $y$ as well, writing simply $ab$ or $a\mathrm{⊲}b$. With these notations, the hypotheses of the induction principle are the following.

• For any cut defining a surreal number $x$, together with

  1. for each $L$, an element $a^L:A(x^L)$, and

  2. for each $R$, an element $a^R:A(x^R)$, such that

  3. for all $L$ and $R$ we have $(x^L,a^L)\mathrm{⊲}(x^R,a^R)$

  there is a specified element $f_a:A(x)$. We call such data a dependent cut over the cut defining $x$.

• For any $x,y:\mathrm{𝖭𝗈}$ with $a:A(x)$ and $b:A(y)$, if $x\le y$ and $y\le x$ and also $(x,a)(y,b)$ and $(y,b)(x,a)$, then $a{=}_{{\mathrm{𝖾𝗊}}_{\mathrm{𝖭𝗈}}}^{A}b$.

• Given cuts defining two surreal numbers $x$ and $y$, and dependent cuts $a$ over $x$ and $b$ over $y$, such that for all $L$ we have and $(x^L,a^L)\mathrm{⊲}(y,f_b)$, and for all $R$ we have and $(x,f_a)\mathrm{⊲}(y^R,b^R)$, then $(x,f_a)(y,f_b)$.

• $$ takes values in mere propositions.

• Given cuts defining two surreal numbers $x$ and $y$, dependent cuts $a$ over $x$ and $b$ over $y$, and an $L_0$ such that $x\le y^{L_0}$ and $(x,f_a)(y^{L_0},b^{L_0})$, we have $(x,f_a)\mathrm{⊲}(y,f_b)$.

• Given cuts defining two surreal numbers $x$ and $y$, dependent cuts $a$ over $x$ and $b$ over $y$, and an $R_0$ such that $x^{R_0}\le y$ together with $(x^{R_0},a^{R_0}),(y,f_b)$, we have $(x,f_a)\mathrm{⊲}(y,f_b)$.

• $\mathrm{⊲}$ takes values in mere propositions.

Under these hypotheses we deduce a function $f:{\prod }_{(x:\mathrm{𝖭𝗈})}A(x)$ such that

$f(x)$ $\mathrm{\hspace{0.33em}}\equiv f_{f[x]}$ (11.6.3)

$(x\le y)$ $\mathrm{\hspace{0.33em}}\Rightarrow (x,f(x))(y,f(y))$

$\mathrm{\hspace{0.33em}}\Rightarrow (x,f(x))\mathrm{⊲}(y,f(y)).$

In the computation rule (11.6.3) for the point constructor, $x$ is a surreal number defined by a cut, and $f[x]$ denotes the dependent cut over $x$ defined by applying $f$ (and using the fact that $f$ takes to $\mathrm{⊲}$). As usual, we will generally use pattern-matching notation, where the definition of $f$ on a cut $\{x^L|x^R\}$ may use the symbols $f(x^L)$ and $f(x^R)$ and the assumption that they form a dependent cut.

As with the Cauchy reals, we have special cases resulting from trivializing some of $A$, $$, and $\mathrm{⊲}$. Taking $$ and $\mathrm{⊲}$ to be constant at $\mathrm{𝟏}$, we have $\mathrm{𝖭𝗈}$-induction, which for simplicity we state only for mere properties:

• Given $P:\mathrm{𝖭𝗈}\to \mathrm{𝖯𝗋𝗈𝗉}$, if $P(x)$ holds whenever $x$ is a surreal number defined by a cut such that $P(x^L)$ and $P(x^R)$ hold for all $L$ and $R$, then $P(x)$ holds for all $x:\mathrm{𝖭𝗈}$.

This should be compared with Conway’s remark:

In general when we wish to establish a proposition $P(x)$ for all numbers $x$, we will prove it inductively by deducing $P(x)$ from the truth of all the propositions $P(x^L)$ and $P(x^R)$. We regard the phrase “all numbers are constructed in this way” as justifying the legitimacy of this procedure.

With $\mathrm{𝖭𝗈}$-induction, we can prove

Theorem 11.6.3 (Conway’s Theorem 0).

1. For any $x:\mathrm{𝖭𝗈}$, we have $x\le x$.

2. For any $x:\mathrm{𝖭𝗈}$ defined by a cut, we have and for all $L$ and $R$.

Proof.

Note first that if $x\le x$, then whenever $x$ occurs as a left option of some cut $y$, we have by the first constructor of , and similarly whenever $x$ occurs as a right option of a cut $y$, we have by the second constructor of . In particular, 1$\Rightarrow$2.

We prove 1 by $\mathrm{𝖭𝗈}$-induction on $x$. Thus, assume $x$ is defined by a cut such that $x^L\le x^L$ and $x^R\le x^R$ for all $L$ and $R$. But by our observation above, these assumptions imply and for all $L$ and $R$, yielding $x\le x$ by the constructor of $\le$. ∎

Corollary 11.6.4.

$\mathrm{𝖭𝗈}$ is a 0-type.

Proof.

The mere relation $R(x,y):\equiv (x\le y)\wedge (y\le x)$ implies identity by the path constructor of $\mathrm{𝖭𝗈}$, and contains the diagonal by thm:NO-refl-opt1. Thus, thm:h-set-refrel-in-paths-sets applies. ∎

By contrast, Conway’s Theorem 1 (transitivity of $\le$) is somewhat harder to establish with our definition; see thm:NO-unstrict-transitive.

We will also need the joint recursion principle, -recursion, which it is convenient to state as follows. Suppose $A$ is a type equipped with relations $:A\to A\to \mathrm{𝖯𝗋𝗈𝗉}$ and $\mathrm{⊲}:A\to A\to \mathrm{𝖯𝗋𝗈𝗉}$. Then we can define $f:\mathrm{𝖭𝗈}\to A$ by doing the following.

1. For any $x$ defined by a cut, assuming $f(x^L)$ and $f(x^R)$ to be defined such that $f(x^L)\mathrm{⊲}f(x^R)$ for all $L$ and $R$, we must define $f(x)$. (We call this the primary clause of the recursion.)

2. Prove that $$ is antisymmetric: if $ab$ and $ba$, then $a=b$.

3. For $x,y$ defined by cuts such that for all $L$ and for all $R$, and assuming inductively that $f(x^L)\mathrm{⊲}f(y)$ for all $L$, $f(x)\mathrm{⊲}f(y^R)$ for all $R$, and also that $f(x^L)\mathrm{⊲}f(x^R)$ and $f(y^L)\mathrm{⊲}f(y^R)$ for all $L$ and $R$, we must prove $f(x)f(y)$.

4. For $x,y$ defined by cuts and an $L_0$ such that $x\le y^{L_0}$, and assuming inductively that $f(x)f(y^{L_0})$, and also that $f(x^L)\mathrm{⊲}f(x^R)$ and $f(y^L)\mathrm{⊲}f(y^R)$ for all $L$ and $R$, we must prove $f(x)\mathrm{⊲}f(y)$.

5. For $x,y$ defined by cuts and an $R_0$ such that $x^{R_0}\le y$, and assuming inductively that $f(x^{R_0})f(y)$, and also that $f(x^L)\mathrm{⊲}f(x^R)$ and $f(y^L)\mathrm{⊲}f(y^R)$ for all $L$ and $R$, we must prove $f(x)\mathrm{⊲}f(y)$.

The last three clauses can be more concisely described by saying we must prove that $f$ (as defined in the first clause) takes $\le$ to $$ and to $\mathrm{⊲}$. We will refer to these properties by saying that $f$ preserves inequalities. Moreover, in proving that $f$ preserves inequalities, we may assume the particular instance of $\le$ or to be obtained from one of its constructors, and we may also use inductive hypotheses that $f$ preserves all inequalities appearing in the input to that constructor.

If we succeed at 1–5 above, then we obtain $f:\mathrm{𝖭𝗈}\to A$, which computes on cuts as specified by 1, and which preserves all inequalities:

Like $({ℝ}_{𝖼},\mathrm{\sim })$-recursion for the Cauchy reals, this recursion principle is essential for defining functions on $\mathrm{𝖭𝗈}$, since we cannot first define a function on “pre-surreals” and only later prove that it respects the notion of equality.

Example 11.6.5.

Let us define the negation function $\mathrm{No}\mathrm{\to }\mathrm{No}$. We apply the joint recursion principle with $A\mathrm{:}\mathrm{\equiv }\mathrm{No}$, with $\mathrm{(}xy\mathrm{)}\mathrm{:}\mathrm{\equiv }\mathrm{(}y\mathrm{\le }x\mathrm{)}$, and . Clearly this $$ is antisymmetric.

For the main clause in the definition, we assume $x$ defined by a cut, with $\mathrm{-}{x}^L$ and $\mathrm{-}{x}^R$ defined such that $\mathrm{-}{x}^L\mathit{}\mathrm{⊲}\mathrm{-}{x}^R$ for all $L$ and $R$. By definition, this means for all $L$ and $R$, so we can define $\mathrm{-}x$ by the cut $\mathrm{\{}\mathrm{-}{x}^R\mathrm{|}\mathrm{-}{x}^L\mathrm{\}}$. This notation, which follows Conway, refers to the cut whose left options are indexed by the type $\mathrm{R}$ indexing the right options of $x$, and whose right options are indexed by the type $\mathrm{L}$ indexing the left options of $x$, with the corresponding families $\mathrm{R}\mathrm{\to }\mathrm{No}$ and $\mathrm{L}\mathrm{\to }\mathrm{No}$ defined by composing those for $x$ with negation.

We now have to verify that $f$ preserves inequalities.

• For $x\le y$, we may assume for all $L$ and for all $R$, and show $-y\le -x$. But inductively, we may assume and , which gives the desired result, by definition of $-y$, $-x$, and the constructor of $\le$.

• For , in the first case when it arises from some $x\le y^{L_0}$, we may inductively assume $-y^{L_0}\le -x$, in which case follows by the constructor of .

• Similarly, if arises from $x^{R_0}\le y$, the inductive hypothesis is $-y\le -x^R$, yielding again.

To do much more than this, however, we will need to characterize the relations $\le$ and more explicitly, as we did for the Cauchy reals in thm:RC-sim-characterization. Also as there, we will have to simultaneously prove a couple of essential properties of these relations, in order for the induction to go through.

Theorem 11.6.6.

There are relations $\mathrm{⪯}\mathrm{:}\mathrm{No}\mathrm{\to }\mathrm{No}\mathrm{\to }\mathrm{Prop}$ and $\mathrm{\prec }\mathrm{:}\mathrm{No}\mathrm{\to }\mathrm{No}\mathrm{\to }\mathrm{Prop}$ such that if $x$ and $y$ are surreals defined by cuts, then

$(x⪯y)$ $:\equiv (\forall (L).x^L\prec y)\wedge (\forall (R).x\prec y^R)$

$(x\prec y)$ $:\equiv (\exists (L).x⪯y^L)\vee (\exists (R).x^R⪯y).$

Moreover, we have

$$(x\prec y)\to (x⪯y)$$ (11.6.6)

and all the reasonable transitivity properties making $\mathrm{\prec }$ and $\mathrm{⪯}$ into a “bimodule” over $\mathrm{\le }$ and :

(11.6.7)

Proof.

We define $⪯$ and $\prec$ by double -induction on $x,y$. The first induction is a simple recursion, whose codomain is the subset $A$ of $(\mathrm{𝖭𝗈}\to \mathrm{𝖯𝗋𝗈𝗉})\times (\mathrm{𝖭𝗈}\to \mathrm{𝖯𝗋𝗈𝗉})$ consisting of pairs of predicates of which one implies the other and which satisfy “transitivity on the right”, i.e. (11.6.6) and the right column of (11.6.7) with $(x⪯\text{–})$ and $(x\prec \text{–})$ replaced by the two given predicates. As in the proof of defn:RC-approx, we regard these predicates as half of binary relations, writing them as $y\mapsto (\mathrm{♢}⪯y)$ and $y\mapsto (\mathrm{♢}\prec y)$, with $\mathrm{♢}$ denoting the pair of relations. We equip $A$ with the following two relations:

$(\mathrm{♢}\mathrm{♡})$ $:\equiv \forall (y:\mathrm{𝖭𝗈}).((\mathrm{♡}⪯y)\to (\mathrm{♢}⪯y))\wedge ((\mathrm{♡}\prec y)\to (\mathrm{♢}\prec y)),$

$(\mathrm{♢}\mathrm{⊲}\mathrm{♡})$ $:\equiv \forall (y:\mathrm{𝖭𝗈}).((\mathrm{♡}⪯y)\to (\mathrm{♢}\prec y)).$

Note that $$ is antisymmetric, since if $\mathrm{♢}\mathrm{♡}$ and $\mathrm{♡}\mathrm{♢}$, then $(\mathrm{♡}⪯y)\iff (\mathrm{♢}⪯y)$ and $(\mathrm{♡}\prec y)\iff (\mathrm{♢}\prec y)$ for all $y$, hence $\mathrm{♢}=\mathrm{♡}$ by univalence for mere propositions and function extensionality. Moreover, to say that a function $\mathrm{𝖭𝗈}\to A$ preserves inequalities is exactly to say that, when regarded as a pair of binary relations on $\mathrm{𝖭𝗈}$, it satisfies “transitivity on the left” (the left column of (11.6.7)).

Now for the primary clause of the recursion, we assume given $x$ defined by a cut, and relations $(x^L\prec \text{–})$, $(x^R\prec \text{–})$, $(x^L⪯\text{–})$, and $(x^R⪯\text{–})$ for all $L$ and $R$, of which the strict ones imply the non-strict ones, which satisfy transitivity on the right, and such that

$$\forall (L,R).\forall (y:\mathrm{𝖭𝗈}).((x^R⪯y)\to (x^L\prec y)).$$ (11.6.9)

We now have to define $(x\prec y)$ and $(x⪯y)$ for all $y$. Here in contrast to defn:RC-approx, rather than a nested recursion, we use a nested induction, in order to be able to inductively use transitivity on the left with respect to the inequalities and . Define $A^{\prime }:\mathrm{𝖭𝗈}\to 𝒰$ by taking $A^{\prime }(y)$ to be the subset $A^{\prime }$ of $\mathrm{𝖯𝗋𝗈𝗉}\times \mathrm{𝖯𝗋𝗈𝗉}$ consisting of two mere propositions, denoted $\mathrm{△}⪯y$ and $\mathrm{△}\prec y$ (with $\mathrm{△}:A^{\prime }(y)$), such that

$$(\mathrm{△}\prec y)\to (\mathrm{△}⪯y)$$ (11.6.10)

$$\forall (L).(\mathrm{△}⪯y)\to (x^L\prec y)$$ (11.6.10)

$$\forall (R).(x^R⪯y)\to (\mathrm{△}\prec y).$$ (11.6.10)

Using notation analogous to $$ and $\mathrm{⊲}$, we equip $A^{\prime }$ with the two relations defined for $\mathrm{△}:A^{\prime }(y)$ and $\mathrm{\square }:A^{\prime }(z)$ by

$(\mathrm{△}⊑\mathrm{\square })$ $:\equiv ((\mathrm{△}⪯y)\to (\mathrm{\square }⪯z))\wedge ((\mathrm{△}\prec y)\to (\mathrm{\square }\prec z))$

$(\mathrm{△}⊏\mathrm{\square })$ $:\equiv ((\mathrm{△}⪯y)\to (\mathrm{\square }\prec z)).$

Again, $⊑$ is evidently antisymmetric in the appropriate sense. Moreover, a function ${\prod }_{(y:\mathrm{𝖭𝗈})}{A}^{\prime }(y)$ which preserves inequalities is precisely a pair of predicates of which one implies the other, which satisfy transitivity on the right, and transitivity on the left with respect to the inequalities and . Thus, this inner induction will provide what we need to complete the primary clause of the outer recursion.

For the primary clause of the inner induction, we assume also given $y$ defined by a cut, and properties $(x\prec y^L)$, $(x\prec y^R)$, $(x⪯y^L)$, and $(x⪯y^R)$ for all $L$ and $R$, with the strict ones implying the non-strict ones, transitivity on the left with respect to and , and on the right with respect to . We can now give the definitions specified in the theorem statement:

$(x⪯y)$ $:\equiv (\forall (L).x^L\prec y)\wedge (\forall (R).x\prec y^R),$ (11.6.10)

$(x\prec y)$ $:\equiv (\exists (L).x⪯y^L)\vee (\exists (R).x^R⪯y).$ (11.6.10)

For this to define an element of $A^{\prime }(y)$, we must show first that $(x\prec y)\to (x⪯y)$. The assumption $x\prec y$ has two cases. On one hand, if there is $L_0$ with $x⪯y^{L_0}$, then by transitivity on the right with respect to , we have $x\prec y^R$ for all $R$. Moreover, by transitivity on the left with respect to , we have $x^L\prec y^{L_0}$ for any $L$, hence $x^L\prec y$ by transitivity on the right. Thus, $x⪯y$.

On the other hand, if there is $R_0$ with $x^{R_0}⪯y$, then by transitivity on the left with respect to we have $x^L\prec y$ for all $L$. And by transitivity on the left and right with respect to and , we have $x\prec y^R$ for any $R$. Thus, $x⪯y$.

We also need to show that these definitions are transitive on the left with respect to and . But if $x⪯y$, then $x^L\prec y$ for all $L$ by definition; while if $x^R⪯y$, then $x\prec y$ also by definition.

Thus, (11.6.10) and (11.6.10) do define an element of $A^{\prime }(y)$. We now have to verify that this definition preserves inequalities, as a dependent function into $A^{\prime }$, i.e. that these relations are transitive on the right. Remember that in each case, we may assume inductively that they are transitive on the right with respect to all inequalities arising in the inequality constructor.

• Suppose $x⪯y$ and $y\le z$, the latter arising from and for all $L$ and $R$. Then the inductive hypothesis (of the inner recursion) applied to yields $x\prec z^R$ for any $R$. Moreover, by definition $x⪯y$ implies that $x^L\prec y$ for any $L$, so by the inductive hypothesis of the outer recursion we have $x^L\prec z$. Thus, $x⪯z$.

• Suppose $x⪯y$ and . First, suppose arises from $y\le z^{L_0}$. Then the inner inductive hypothesis applied to $y\le z^{L_0}$ yields $x⪯z^{L_0}$, hence $x\prec z$.

  Second, suppose arises from $y^{R_0}\le z$. Then by definition, $x⪯y$ implies $x\prec y^{R_0}$, and then the inner inductive hypothesis for $y^{R_0}\le z$ yields $x\prec z$.

• Suppose $x\prec y$ and $y\le z$, the latter arising from and for all $L$ and $R$. By definition, $x\prec y$ implies there merely exists $R_0$ with $x^{R_0}⪯y$ or $L_0$ with $x⪯y^{L_0}$. If $x^{R_0}⪯y$, then the outer inductive hypothesis yields $x^{R_0}⪯z$, hence $x\prec z$. If $x⪯y^{L_0}$, then the inner inductive hypothesis for (which holds by the constructor of $y\le z$) yields $x\prec z$.

This completes the inner induction. Thus, for any $x$ defined by a cut, we have $(x\prec \text{–})$ and $(x⪯\text{–})$ defined by (11.6.10) and (11.6.10), and transitive on the right.

To complete the outer recursion, we need to verify these definitions are transitive on the left. After a $\mathrm{𝖭𝗈}$-induction on $z$, we end up with three cases that are essentially identical to those just described above for transitivity on the right. Hence, we omit them. ∎

Theorem 11.6.10.

For any $x\mathrm{,}y\mathrm{:}\mathrm{No}$ we have and $\mathrm{(}x\mathrm{\le }y\mathrm{)}\mathrm{=}\mathrm{(}x\mathrm{⪯}y\mathrm{)}$.

Proof.

From left to right, we use -induction where $A(x):\equiv \mathrm{𝟏}$, with $⪯$ and $\prec$ supplying the relations $$ and $\mathrm{⊲}$. In all the constructor cases, $x$ and $y$ are defined by cuts, so the definitions of $⪯$ and $\prec$ evaluate, and the inductive hypotheses apply.

From right to left, we use $\mathrm{𝖭𝗈}$-induction to assume that $x$ and $y$ are defined by cuts. But now the definitions of $⪯$ and $\prec$, and the inductive hypotheses, supply exactly the data required for the relevant constructors of $\le$ and . ∎

Corollary 11.6.11.

The relations $\mathrm{\le }$ and on $\mathrm{No}$ satisfy

and are transitive:

$$(x\le y)\to (y\le z)\to (x\le z)$$

As with the Cauchy reals, the joint -recursion principle remains essential when defining all operations on $\mathrm{𝖭𝗈}$.

Example 11.6.12.

We define $\mathrm{+}\mathrm{:}\mathrm{No}\mathrm{\to }\mathrm{No}\mathrm{\to }\mathrm{No}$ by a double recursion. For the outer recursion, we take the codomain to be the subset of $\mathrm{No}\mathrm{\to }\mathrm{No}$ consisting of functions $g$ such that and $\mathrm{(}x\mathrm{\le }y\mathrm{)}\mathrm{\to }\mathrm{(}g\mathrm{(}x\mathrm{)}\mathrm{\le }g\mathrm{(}y\mathrm{)}\mathrm{)}$ for all $x\mathrm{,}y$. For such $g\mathrm{,}h$ we define $\mathrm{(}gh\mathrm{)}\mathrm{:}\mathrm{\equiv }\mathrm{\forall }\mathrm{(}x\mathrm{:}\mathrm{No}\mathrm{)}\mathrm{.}g\mathrm{(}x\mathrm{)}\mathrm{\le }h\mathrm{(}x\mathrm{)}$ and . Clearly $$ is antisymmetric.

For the primary clause of the recursion, we suppose $x$ defined by a cut, and we define $\mathrm{(}x\mathrm{+}\mathit{\text{–}}\mathrm{)}$ by an inner recursion on $\mathrm{No}$ with codomain $\mathrm{No}$, with relations $\mathrm{⊑}$ and $\mathrm{⊏}$ coinciding with $\mathrm{\le }$ and . For the primary clause of the inner recursion, we suppose also $y$ defined by a cut, and give Conway’s definition:

$$x+y:\equiv \{x^L+y,x+y^L|x^R+y,x+y^R\}.$$

In other words, the left options of $x\mathrm{+}y$ are all numbers of the form $x^L\mathrm{+}y$ for some left option $x^L$, or $x\mathrm{+}{y}^L$ for some left option $y^L$. Now we verify that this definition preserves inequality:

• If $y\le z$ arises from knowing that and for all $L$ and $R$, then the inner inductive hypothesis gives and , while the outer inductive hypotheses give and . And since each $x^L+z$ is by definition a left option of $x+z$, we have , and similarly . Thus, using transitivity, and , and so we may conclude $x+y\le x+z$ by the constructor of $\le$.

• If arises from an $L_0$ with $y\le z^{L_0}$, then inductively $x+y\le x+z^{L_0}$, hence since $x+z^{L_0}$ is a right option of $x+z$.

• Similarly, if arises from $y^{R_0}\le z$, then since $x+y^{R_0}\le x+z$.

This completes the inner recursion. For the outer recursion, we have to verify that $\mathrm{+}$ preserves inequality on the left as well. After an $\mathrm{No}$-induction, this proceeds in exactly the same way.

In the Appendix to Part Zero of [conway:onag], Conway discusses how the surreal numbers may be formalized in ZFC set theory: by iterating along the ordinals and passing to sets of representatives of lowest rank for each equivalence class, or by representing numbers with “sign-expansions”. He then remarks that

The curiously complicated nature of these constructions tells us more about the nature of formalizations within ZF than about our system of numbers…

and goes on to advocate for a general theory of “permissible kinds of construction” which should include

1. Objects may be created from earlier objects in any reasonably constructive fashion.

2. Equality among the created objects can be any desired equivalence relation.

Condition 1 can be naturally read as justifying general principles of inductive definition, such as those presented in sec:strictly-positive,sec:generalizations. In particular, the condition of strict positivity for constructors can be regarded as a formalization of what it means to be “reasonably constructive”. Condition 2 then suggests we should extend this to higher inductive definitions of all sorts, in which we can impose path constructors making objects equal in any reasonable way. For instance, in the next paragraph Conway says:

…we could also, for instance, freely create a new object $(x,y)$ and call it the ordered pair of $x$ and $y$. We could also create an ordered pair $[x,y]$ different from $(x,y)$ but co-existing with it…If instead we wanted to make $(x,y)$ into an unordered pair, we could define equality by means of the equivalence relation $(x,y)=(z,t)$ if and only if $x=z,y=t$ or $x=t,y=z$.

The freedom to introduce new objects with new names, generated by certain forms of constructors, is precisely what we have in the theory of inductive definitions. Just as with our two copies of the natural numbers $\mathbb{N}$ and ${\mathbb{N}}^{\prime }$ in sec:appetizer-univalence, if we wrote down an identical definition to the cartesian product type $A\times B$, we would obtain a distinct product type $A{\times }^{\prime }B$ whose canonical elements we could freely write as $[x,y]$. And we could make one of these a type of unordered pairs by adding a suitable path constructor.

To be sure, Conway’s point was not to complain about ZF in particular, but to argue against all foundational theories at once:

…this proposal is not of any particular theory as an alternative to ZF… What is proposed is instead that we give ourselves the freedom to create arbitrary mathematical theories of these kinds, but prove a metatheorem which ensures once and for all that any such theory could be formalized in terms of any of the standard foundational theories.

One might respond that, in fact, univalent foundations is not one of the “standard foundational theories” which Conway had in mind, but rather the metatheory in which we may express our ability to create new theories, and about which we may prove Conway’s metatheorem. For instance, the surreal numbers are one of the “mathematical theories” Conway has in mind, and we have seen that they can be constructed and justified inside univalent foundations. Similarly, Conway remarked earlier that

…set theory would be such a theory, sets being constructed from earlier ones by processes corresponding to the usual axioms, and the equality relation being that of having the same members.

This description closely matches the higher-inductive construction of the cumulative hierarchy of set theory in sec:cumulative-hierarchy. Conway’s metatheorem would then correspond to the fact we have referred to several times that we can construct a model of univalent foundations inside ZFC (which is outside the scope of this book).

However, univalent foundations is so rich and powerful in its own right that it would be foolish to relegate it to only a metatheory in which to construct set-like theories. We have seen that even at the level of sets (0-types), the higher inductive types in univalent foundations yield direct constructions of objects by their universal properties (sec:free-algebras), such as a constructive theory of Cauchy completion (sec:cauchy-reals). But most importantly, the potential to model homotopy theory and category theory directly in the foundational system (cha:homotopy,cha:category-theory) gives univalent foundations an advantage which no set-theoretic foundation can match.

Title	11.6 The surreal numbers