11.6 The surreal numbers


In this sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath we consider another example of a higher inductive-inductive type, which draws together many of our threads: Conway’s field 𝖭𝗈 of surreal numbersMathworldPlanetmath [conway:onag]. The surreal numbers are the natural common generalizationPlanetmathPlanetmath of the (Dedekind) real numbers (\autorefsec:dedekind-reals) and the ordinal numbersMathworldPlanetmath (\autorefsec: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 relationMathworldPlanetmathPlanetmathPlanetmath of (strict) inequality between surreals, so that relation must be defined simultaneously with the type 𝖭𝗈 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 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 .

Moreover, we will define strict inequality < and non-strict inequality for surreals separately (and mutually inductively). Conway defines < in terms of , in a way which is sensible classically but not constructively. Furthermore, a negative definition of < would make it unacceptable as a hypothesisMathworldPlanetmathPlanetmath of the constructor of a higher inductive type (see \autorefsec: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 predicateMathworldPlanetmathPlanetmath 𝖭𝗈𝖯𝗋𝗈𝗉 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 theoryMathworldPlanetmath the surreal numbers form a proper classMathworldPlanetmath, whereas the sets L and R are true (small) sets, not arbitrary subclasses of 𝖭𝗈. In type theoryPlanetmathPlanetmath, this means that 𝖭𝗈 will be defined relative to a universePlanetmathPlanetmath 𝒰, but will itself belong to the next higher universe 𝒰, like the sets 𝖮𝗋𝖽 and 𝖢𝖺𝗋𝖽 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 \autorefsec:cumulative-hierarchy.) That is, the constructor of surreals will have type

,:𝒰(𝖭𝗈)(𝖭𝗈)(some condition)𝖭𝗈

which is indeed strictly positive.

Finally, after giving the mutual definitions of 𝖭𝗈 and its ordering, Conway declares two surreal numbers x and y to be equal if xy and yx. This is naturally read as passing to a quotientPlanetmathPlanetmath of the set of “pre-surreals” by an equivalence relationMathworldPlanetmath. However, in the absence of the axiom of choiceMathworldPlanetmath, 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 No of surreal numbers, along with the relations <:NoNoU and :NoNoU, are defined higher inductive-inductively as follows. The type No has the following constructors.

  • For any ,:𝒰 and functions 𝖭𝗈 and 𝖭𝗈, whose values we write as xL and xR for L: and R: respectively, if (L:).(R:).xL<xR, then there is a surreal number x.

  • For any x,y:𝖭𝗈 such that xy and yx, we have 𝖾𝗊𝖭𝗈(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 xL will implicitly assume L:L, and similarly xR will assume R:R. In this way we can usually avoid naming the indexing types L and R, which is convenient when there are many different cuts under discussion. Following Conway, we call xL a left option of x and xR 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 has the following constructors.

  • Given cuts defining two surreal numbers x and y, if xL<y for all L, and x<yR for all R, then xy.

  • Propositional truncation: for any x,y:𝖭𝗈, if p,q:xy, 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 xyL, then x<y.

  • Given cuts defining two surreal numbers x and y, if there is an R such that xRy, then x<y.

  • Propositional truncation: for any x,y:𝖭𝗈, if p,q:x<y, 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 any member of R, then there is a number {L|R}. All numbers are constructed in this way.

  • -

    xy iff (no xRy and x no yL).

  • -

    x=y iff (xy and yx).

  • -

    x>y iff (xy and yx).

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

We can immediately populate 𝖭𝗈 with many surreal numbers. Like Conway, we write

{x,y,z,|u,v,w,}

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

  • We define ι:𝖭𝗈 recursively by

    ι(0) :{|},
    ι(𝗌𝗎𝖼𝖼(n)) :{ι(n)|}.

    That is, ι(0) is defined by the cut consisting of 𝟎𝖭𝗈 and 𝟎𝖭𝗈. Similarly, ι(𝗌𝗎𝖼𝖼(n)) is defined by 𝟏𝖭𝗈 (picking out ι(n)) and 𝟎𝖭𝗈.

  • Similarly, we define ι:𝖭𝗈 using the sign-case recursion principle (\autorefthm:sign-induction):

    ι(0) :{|},
    ι(n+1) :{ι(n)|} n0,
    ι(n-1) :{|ι(n)} n0.
  • By a dyadic rational we mean a pair (a,n) where a: and n:, and such that if n>0 then a is odd. We will write it as a/2n, and identify it with the corresponding rational number. If D denotes the set of dyadic rationals, we define ιD:D𝖭𝗈 by inductionMathworldPlanetmath on n:

    ιD(a/20) :ι(a),
    ιD(a/2n) :{a/2n-1/2n|a/2n+1/2n},for n>0.

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

  • We define ι𝖽:𝖽𝖭𝗈, where 𝖽 is (any version of) the Dedekind reals from \autorefsec:dedekind-reals, by

    ι𝖽(x) :{qD such that q<x|qD such that x<q}.

    Unlike in the previous cases, it is not obvious that this extends ιD when we regard dyadic rationals as Dedekind reals. This follows from the simplicity theoremMathworldPlanetmath (\autorefthm:NO-simplicity).

  • Recall the type 𝖮𝗋𝖽 of ordinals from \autorefsec:ordinals, which is well-ordered by the relation <, where A<B means that A=B/b for some b:B. We define ι𝖮𝗋𝖽:𝖮𝗋𝖽𝖭𝗈 by well-founded recursion (\autorefthm:wfrec) on 𝖮𝗋𝖽:

    ι𝖮𝗋𝖽(A):{ι𝖮𝗋𝖽(A/a) for all a:A|}.

    It will also follow from the simplicity theorem that ι𝖮𝗋𝖽 restricted to finite ordinals agrees with ι.

  • A few more interesting examples taken from Conway:

    ω :{ 0,1,2,3,|}  (also an ordinal)
    -ω :{|,-3,-2,-1,0}
    1/ω :{ 0| 1,12,14,18,}
    ω-1 :{ 0,1,2,3,|ω}
    ω/2 :{ 0,1,2,3,|,ω-2,ω-1,ω}.

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.

  • xL<z<xR for all L and R.

  • For every left option zL of z, there exists a left option xL with zLxL.

  • For every right option zR of z, there exists a right option xR with xRzR.

Then x=z.

Proof.

Applying the path constructor of 𝖭𝗈, we must show xz and zx. The first entails showing xL<z for all L, which we assumed, and x<zR for all R. But by assumptionPlanetmathPlanetmath, for any zR there is an xR with xRzR hence x<zR as desired. Thus xz; the proof of zx is symmetricPlanetmathPlanetmath. ∎

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 :𝖭𝗈𝒰
B :(x,y:𝖭𝗈)(a:A(x))(b:A(y))(xy)𝒰
C :(x,y:𝖭𝗈)(a:A(x))(b:A(y))(x<y)𝒰.

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,ξ) as (x,a)\trianglelefteqslantξ(y,b) and C(x,y,a,b,ξ) as (x,a)ξ(y,b). Similarly, we usually omit the ξ since it inhabits a mere proposition and so is uninteresting, and we may often omit x and y as well, writing simply a\trianglelefteqslantb or ab. With these notations, the hypotheses of the induction principle are the following.

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

    1. (a)

      for each L, an element aL:A(xL), and

    2. (b)

      for each R, an element aR:A(xR), such that

    3. (c)

      for all L and R we have (xL,aL)(xR,aR)

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

  • For any x,y:𝖭𝗈 with a:A(x) and b:A(y), if xy and yx and also (x,a)\trianglelefteqslant(y,b) and (y,b)\trianglelefteqslant(x,a), then a=𝖾𝗊𝖭𝗈Ab.

  • 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 xL<y and (xL,aL)(y,fb), and for all R we have x<yR and (x,fa)(yR,bR), then (x,fa)\trianglelefteqslant(y,fb).

  • \trianglelefteqslant 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 L0 such that xyL0 and (x,fa)\trianglelefteqslant(yL0,bL0), we have (x,fa)(y,fb).

  • Given cuts defining two surreal numbers x and y, dependent cuts a over x and b over y, and an R0 such that xR0y together with (xR0,aR0),\trianglelefteqslant(y,fb), we have (x,fa)(y,fb).

  • takes values in mere propositions.

Under these hypotheses we deduce a function f:(x:𝖭𝗈)A(x) such that

f(x) ff[x] (11.6.3)
(xy) (x,f(x))\trianglelefteqslant(y,f(y))
(x<y) (x,f(x))(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 ). As usual, we will generally use pattern-matching notation, where the definition of f on a cut {xL|xR} may use the symbols f(xL) and f(xR) and the assumption that they form a dependent cut.

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

  • Given P:𝖭𝗈𝖯𝗋𝗈𝗉, if P(x) holds whenever x is a surreal number defined by a cut such that P(xL) and P(xR) hold for all L and R, then P(x) holds for all x:𝖭𝗈.

This should be compared with Conway’s remark:

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

With 𝖭𝗈-induction, we can prove

Theorem 11.6.3 (Conway’s Theorem 0).
  1. 1.

    For any x:𝖭𝗈, we have xx.

  2. 2.

    For any x:𝖭𝗈 defined by a cut, we have xL<x and x<xR for all L and R.

Proof.

Note first that if xx, then whenever x occurs as a left option of some cut y, we have x<y by the first constructor of <, and similarly whenever x occurs as a right option of a cut y, we have y<x by the second constructor of <. In particular, 12.

We prove 1 by 𝖭𝗈-induction on x. Thus, assume x is defined by a cut such that xLxL and xRxR for all L and R. But by our observation above, these assumptions imply xL<x and x<xR for all L and R, yielding xx by the constructor of . ∎

Corollary 11.6.4.

𝖭𝗈 is a 0-type.

Proof.

The mere relation R(x,y):(xy)(yx) implies identityPlanetmathPlanetmathPlanetmathPlanetmath by the path constructor of 𝖭𝗈, and contains the diagonal by \autorefthm:NO-refl-opt1. Thus, \autorefthm:h-set-refrel-in-paths-sets applies. ∎

By contrast, Conway’s Theorem 1 (transitivity of ) is somewhat harder to establish with our definition; see \autorefthm: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 \trianglelefteqslant:AA𝖯𝗋𝗈𝗉 and :AA𝖯𝗋𝗈𝗉. Then we can define f:𝖭𝗈A by doing the following.

  1. 1.

    For any x defined by a cut, assuming f(xL) and f(xR) to be defined such that f(xL)f(xR) for all L and R, we must define f(x). (We call this the primary clause of the recursion.)

  2. 2.

    Prove that \trianglelefteqslant is antisymmetric: if a\trianglelefteqslantb and b\trianglelefteqslanta, then a=b.

  3. 3.

    For x,y defined by cuts such that xL<y for all L and x<yR for all R, and assuming inductively that f(xL)f(y) for all L, f(x)f(yR) for all R, and also that f(xL)f(xR) and f(yL)f(yR) for all L and R, we must prove f(x)\trianglelefteqslantf(y).

  4. 4.

    For x,y defined by cuts and an L0 such that xyL0, and assuming inductively that f(x)\trianglelefteqslantf(yL0), and also that f(xL)f(xR) and f(yL)f(yR) for all L and R, we must prove f(x)f(y).

  5. 5.

    For x,y defined by cuts and an R0 such that xR0y, and assuming inductively that f(xR0)\trianglelefteqslantf(y), and also that f(xL)f(xR) and f(yL)f(yR) for all L and R, we must prove f(x)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 to \trianglelefteqslant and < to . 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 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 15 above, then we obtain f:𝖭𝗈A, which computes on cuts as specified by 1, and which preserves all inequalities:

(x,y:𝖭𝗈).((xy)(f(x)\trianglelefteqslantf(y)))((x<y)(f(x)f(y))).

Like (𝖼,)-recursion for the Cauchy reals, this recursion principle is essential for defining functions on 𝖭𝗈, 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 NoNo. We apply the joint recursion principle with A:No, with (x\trianglelefteqslanty):(yx), and (xy):(y<x). Clearly this \trianglelefteqslant is antisymmetric.

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

We now have to verify that f preserves inequalities.

  • For xy, we may assume xL<y for all L and x<yR for all R, and show -y-x. But inductively, we may assume -y<-xL and -yR<-x, which gives the desired result, by definition of -y, -x, and the constructor of .

  • For x<y, in the first case when it arises from some xyL0, we may inductively assume -yL0-x, in which case -y<-x follows by the constructor of <.

  • Similarly, if x<y arises from xR0y, the inductive hypothesis is -y-xR, yielding -y<-x again.

To do much more than this, however, we will need to characterize the relations and < more explicitly, as we did for the Cauchy reals in \autorefthm: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 :NoNoProp and :NoNoProp such that if x and y are surreals defined by cuts, then

(xy) :((L).xLy)((R).xyR)
(xy) :((L).xyL)((R).xRy).

Moreover, we have

(xy)(xy) (11.6.6)

and all the reasonable transitivity properties making and into a “bimodule” over and <:

(xy)(yz)(xz)    (xy)(yz)(xz)(xy)(yz)(xz)    (xy)(y<z)(xz)(x<y)(yz)(xz)    (xy)(yz)(xz). (11.6.7)
Proof.

We define and by double (𝖭𝗈,,<)-induction on x,y. The first induction is a simple recursion, whose codomain is the subset A of (𝖭𝗈𝖯𝗋𝗈𝗉)×(𝖭𝗈𝖯𝗋𝗈𝗉) 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) and (x) replaced by the two given predicates. As in the proof of \autorefdefn:RC-approx, we regard these predicates as half of binary relations, writing them as y(y) and y(y), with denoting the pair of relations. We equip A with the following two relations:

(\trianglelefteqslant) :(y:𝖭𝗈).((y)(y))((y)(y)),
() :(y:𝖭𝗈).((y)(y)).

Note that \trianglelefteqslant is antisymmetric, since if \trianglelefteqslant and \trianglelefteqslant, then (y)(y) and (y)(y) for all y, hence = by univalence for mere propositions and function extensionality. Moreover, to say that a function 𝖭𝗈A preserves inequalities is exactly to say that, when regarded as a pair of binary relations on 𝖭𝗈, 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 (xL), (xR), (xL), and (xR) for all L and R, of which the strict ones imply the non-strict ones, which satisfy transitivity on the right, and such that

(L,R).(y:𝖭𝗈).((xRy)(xLy)). (11.6.9)

We now have to define (xy) and (xy) for all y. Here in contrast to \autorefdefn: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 xL<x and x<xR. Define A:𝖭𝗈𝒰 by taking A(y) to be the subset A of 𝖯𝗋𝗈𝗉×𝖯𝗋𝗈𝗉 consisting of two mere propositions, denoted y and y (with :A(y)), such that

(y)(y) (11.6.10)
(L).(y)(xLy) (11.6.10)
(R).(xRy)(y). (11.6.10)

Using notation analogous to \trianglelefteqslant and , we equip A with the two relations defined for :A(y) and :A(z) by

() :((y)(z))((y)(z))
() :((y)(z)).

Again, is evidently antisymmetric in the appropriate sense. Moreover, a function (y:𝖭𝗈)A(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 xL<x and x<xR. Thus, this inner induction will provide what we need to completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmath 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 (xyL), (xyR), (xyL), and (xyR) for all L and R, with the strict ones implying the non-strict ones, transitivity on the left with respect to xL<x and x<xR, and on the right with respect to yL<yR. We can now give the definitions specified in the theorem statement:

(xy) :((L).xLy)((R).xyR), (11.6.10)
(xy) :((L).xyL)((R).xRy). (11.6.10)

For this to define an element of A(y), we must show first that (xy)(xy). The assumption xy has two cases. On one hand, if there is L0 with xyL0, then by transitivity on the right with respect to yL0<yR, we have xyR for all R. Moreover, by transitivity on the left with respect to xL<x, we have xLyL0 for any L, hence xLy by transitivity on the right. Thus, xy.

On the other hand, if there is R0 with xR0y, then by transitivity on the left with respect to xL<xR0 we have xLy for all L. And by transitivity on the left and right with respect to x<xR0 and y<yR, we have xyR for any R. Thus, xy.

We also need to show that these definitions are transitiveMathworldPlanetmathPlanetmathPlanetmathPlanetmath on the left with respect to xL<x and x<xR. But if xy, then xLy for all L by definition; while if xRy, then xy also by definition.

Thus, (11.6.10) and (11.6.10) do define an element of A(y). We now have to verify that this definition preserves inequalities, as a dependent function into A, 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 xy and yz, the latter arising from yL<z and y<zR for all L and R. Then the inductive hypothesis (of the inner recursion) applied to y<zR yields xzR for any R. Moreover, by definition xy implies that xLy for any L, so by the inductive hypothesis of the outer recursion we have xLz. Thus, xz.

  • Suppose xy and y<z. First, suppose y<z arises from yzL0. Then the inner inductive hypothesis applied to yzL0 yields xzL0, hence xz.

    Second, suppose y<z arises from yR0z. Then by definition, xy implies xyR0, and then the inner inductive hypothesis for yR0z yields xz.

  • Suppose xy and yz, the latter arising from yL<z and y<zR for all L and R. By definition, xy implies there merely exists R0 with xR0y or L0 with xyL0. If xR0y, then the outer inductive hypothesis yields xR0z, hence xz. If xyL0, then the inner inductive hypothesis for yL0<z (which holds by the constructor of yz) yields xz.

This completes the inner induction. Thus, for any x defined by a cut, we have (x) and (x) 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 𝖭𝗈-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,y:No we have (x<y)=(xy) and (xy)=(xy).

Proof.

From left to right, we use (𝖭𝗈,,<)-induction where A(x):𝟏, with and supplying the relations \trianglelefteqslant and . In all the constructor cases, x and y are defined by cuts, so the definitions of and evaluate, and the inductive hypotheses apply.

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

Corollary 11.6.11.

The relations and < on No satisfy

(x,y:𝖭𝗈).(x<y)(xy)

and are transitive:

(xy)(yz)(xz)
(xy)(y<z)(x<z)
(x<y)(yz)(x<z).

As with the Cauchy reals, the joint (𝖭𝗈,,<)-recursion principle remains essential when defining all operationsMathworldPlanetmath on 𝖭𝗈.

Example 11.6.12.

We define +:NoNoNo by a double recursion. For the outer recursion, we take the codomain to be the subset of NoNo consisting of functions g such that (x<y)(g(x)<g(x)) and (xy)(g(x)g(y)) for all x,y. For such g,h we define (g\trianglelefteqslanth):(x:No).g(x)h(x) and (gh):(x:No).g(x)<h(x). Clearly \trianglelefteqslant is antisymmetric.

For the primary clause of the recursion, we suppose x defined by a cut, and we define (x+) by an inner recursion on No with codomain No, with relations and coinciding with and <. For the primary clause of the inner recursion, we suppose also y defined by a cut, and give Conway’s definition:

x+y:{xL+y,x+yL|xR+y,x+yR}.

In other words, the left options of x+y are all numbers of the form xL+y for some left option xL, or x+yL for some left option yL. Now we verify that this definition preserves inequality:

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

  • If y<z arises from an L0 with yzL0, then inductively x+yx+zL0, hence x+y<x+z since x+zL0 is a right option of x+z.

  • Similarly, if y<z arises from yR0z, then x+y<x+z since x+yR0x+z.

This completes the inner recursion. For the outer recursion, we have to verify that + preserves inequality on the left as well. After an 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 classMathworldPlanetmath, 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. 1.

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

  2. 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 \autorefsec:strictly-positive,\autorefsec: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 numbersMathworldPlanetmath and in \autorefsec:appetizer-univalence, if we wrote down an identical definition to the cartesian product type A×B, we would obtain a distinct product type A×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 metatheoremMathworldPlanetmath 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 \autorefsec: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 propertiesMathworldPlanetmath (\autorefsec:free-algebras), such as a constructive theory of Cauchy completion (\autorefsec:cauchy-reals). But most importantly, the potential to model homotopy theory and category theoryMathworldPlanetmathPlanetmathPlanetmathPlanetmath directly in the foundational system (\autorefcha:homotopyMathworldPlanetmathPlanetmath,\autorefcha:category-theory) gives univalent foundations an advantage which no set-theoretic foundation can match.

Title 11.6 The surreal numbers
\metatable