The very last section of the book presents a constructive definition of Conway’s surreal numbers as a higher inductive-inductive type. Conway’s classical surreals include the ordinal numbers; so it’s natural to wonder whether, or in what sense, this may be true constructively. Paul Taylor recently made an observation which leads to an answer.

The constructive surreals

The constructive higher inductive-inductive definition of the surreals has the following distinguishing features:

• Conway defines two surreal numbers and to be equal if and ; we ensure that this “equality” coincides with ordinary equality by using a path-constructor.
• While Conway defines strict inequality to be the negation of non-strict inequality , constructively we treat them as distinct, each defined inductively in terms of the other (see below).
• Therefore, both and must be defined mutually inductively (and thus inductive-inductively) with the set of surreals itself.

The point-constructor of the surreals says that for two families and of surreals such that each element of is each element of , there is a surreal , called the cut defined by and . If is a cut , we write and for generic elements of and respectively; they are called the left and right options of .

Now the inductive definitions of and are:

• If each and each , then .
• If some or some , then .

I obtained these definitions just by inspecting Conway’s theory and trying to remove all the double-negations. But Paul Taylor recently observed on the constructivenews list that these are two-sided versions of the characterizing relations between membership and subset for his plump ordinals!

Plump ordinals

What is a plump ordinal, you ask? Well, I just wrote an nLab page describing the basic idea; go have a look.

Ordinals and surreals

Now recall that for Conway’s surreals using classical logic, the ordinal numbers can be identified with certain surreals. A cursory reading of the book section on HIIT surreals might leave you with the impression that the same is true here. In particular, a map is constructed that mirrors Conway’s.

However, constructively, this map is quite far from being injective! Indeed, it is injective if and only if excluded middle holds. For example, itself is an ordinal under the relation iff . It’s fairly straightforward to show that (in fact, both are the surreal usually called “2”), but of course implies LEM. (Exercise: give a similar counterexample that works without propositional resizing.)

Thus, constructively, not all the ordinals embed into the surreals. But might there be some “ordinal-like” notion that does so embed? Paul’s observation suggests that plump ordinals should be the answer — and indeed, is the “plumpification” of .

The higher inductive-inductive plump ordinals

Taylor’s original definition of plump ordinal requires propositional resizing (impredicative power sets). However, we can obtain a predicative notion that deserves the same name by mimicking the HIIT definition of surreals, but using only left options.

That is, we define the type to have two constructors:

• For any and , we have .
• For , if and , then .

The mutually defined relation has two constructors:

• If for every , then .
• Mere propositional truncation.

And the mutually defined relation also has two constructors:

• If for some , then .
• Mere propositional truncation.

By recursion over this inductive-inductive definition, we can define a map which preserves inequalities, setting . And by induction over , we can show that also reflects inequalities, since the definitions of and for surreals reduce to those for if there are no right options. Therefore, also reflects equality, hence is injective.

I also claim that is an ordinal (in the next higher universe, like ) under the relation . Transitivity follows just as for the surreals, so it remains to consider well-foundedness, i.e. that every element is accessible.

Let’s prove by induction on that every is accessible. The inductive hypothesis is that we have a family of (left) options such that every is accessible; we are now given and must show that it is accessible. By definition of accessibility, this means we must show that every is accessible. But then , hence for some . The inductive hypothesis then tells us that is accessible, as desired.

In particular, it follows that every can be considered itself as an ordinal, namely the strict slice . However, in the absence of propositional resizing, may only live in the next higher universe like itself; indeed .

Comparing notions of plump ordinal

However, if we do assume propositional resizing, then is equivalent to the set of ordinals (in the same universe) which are plump in Taylor’s sense. I don’t see right now how to show directly from propositional resizing that each lives in the smaller universe. But we can use a different construction of a map : we use recursion on , with the formula

Here denotes the plump successor: the set of all plump ordinals such that for some , with order inherited from . The recursion principle for says that we need to simultaneously prove that this definition of preserves inequalities.

For , if we have for every , so that , then by the inductive hypothesis each . It will suffice to show that this implies , i.e. that if is a plump ordinal with , then . But since < is transitive, we have , so since is plump, .

For <, if we have for some , so that , then by the inductive hypothesis . And certainly , so by plumpness of , we have .

Note that Taylor's definition of plumpness is exactly what we need to make the definition of go through. It's now fairly straightforward to verify that is an equivalence; its inverse is (which obviously factors through ). Thus, is equivalent to the subset of plump ordinals in .

Exercise: Define a pseudo-ordinal to be a surreal defined by a cut with no right options (but whose left options may themselves have right options). Show that the statement “every pseudo-ordinal is a plump ordinal (i.e. in the image of )” is equivalent to LEM.