## The surreals contain the plump ordinals

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 $x$ and $y$ to be equal if $x\le y$ and $y\le x$; 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 $\ge$, constructively we treat them as distinct, each defined inductively in terms of the other (see below).
• Therefore, both $<$ and $\le$ 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 $L$ and $R$ of surreals such that each element of $L$ is $<$ each element of $R$, there is a surreal $\{L|R\}$, called the cut defined by $L$ and $R$. If $x$ is a cut $\{L|R\}$, we write $x^L$ and $x^R$ for generic elements of $L$ and $R$ respectively; they are called the left and right options of $x$.

Now the inductive definitions of $<$ and $\le$ are:

• If each $x^L < y$ and each $y^R > x$, then $x\le y$.
• If some $x^R\le y$ or some $y^L\ge x$, then $x < y$.

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 $\in$ and subset $\subseteq$ 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 $i:\mathrm{Ord}\to \mathrm{No}$ 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, $\mathrm{Prop}$ itself is an ordinal under the relation $P< Q$ iff $Q \wedge \neg P$. It’s fairly straightforward to show that $i(\mathrm{Prop})=i(2)$ (in fact, both are the surreal usually called “2”), but of course $\mathrm{Prop}=2$ 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, $\mathrm{Prop}$ is the “plumpification” of $2$.

### 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 $\mathrm{POrd}$ to have two constructors:

• For any $A:U$ and $x:A\to \mathrm{POrd}$, we have $\mathrm{sup}(x):\mathrm{POrd}$.
• For $x,y:\mathrm{POrd}$, if $x\le y$ and $y\le x$, then $x=y$.

The mutually defined relation $\le:\mathrm{POrd} \to \mathrm{POrd} \to U$ has two constructors:

• If $x_a < y$ for every $a:A$, then $\mathrm{sup}(x)\le y$.
• Mere propositional truncation.

And the mutually defined relation $<:\mathrm{POrd}\to \mathrm{POrd}\to U$ also has two constructors:

• If $x \le y_a$ for some $a:A$, then $x<\mathrm{sup}(y)$.
• Mere propositional truncation.

By recursion over this inductive-inductive definition, we can define a map $j:\mathrm{POrd} \to \mathrm{No}$ which preserves inequalities, setting $j(\mathrm{sup}(x)) = \{ j(x_a) \,|\, \}$. And by induction over $\mathrm{POrd}$, we can show that $j$ also reflects inequalities, since the definitions of $<$ and $\le$ for surreals reduce to those for $\mathrm{POrd}$ if there are no right options. Therefore, $j$ also reflects equality, hence is injective.

I also claim that $\mathrm{POrd}$ is an ordinal (in the next higher universe, like $\mathrm{Ord}$) 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 $x:\mathrm{POrd}$ that every $y\le x$ is accessible. The inductive hypothesis is that we have a family of (left) options $x:A\to \mathrm{POrd}$ such that every $y\le x_a$ is accessible; we are now given $z\le \mathrm{sup}(x)$ and must show that it is accessible. By definition of accessibility, this means we must show that every $y is accessible. But then $y< \mathrm{sup}(x)$, hence $y\le x_a$ for some $a$. The inductive hypothesis then tells us that $y$ is accessible, as desired.

In particular, it follows that every $x:\mathrm{POrd}$ can be considered itself as an ordinal, namely the strict slice $\mathrm{POrd}_{/x} = \sum_{(y:\mathrm{POrd})} (y< x)$. However, in the absence of propositional resizing, $\mathrm{POrd}_{/x}$ may only live in the next higher universe like $\mathrm{POrd}$ itself; indeed $\mathrm{POrd}_{/2} = \mathrm{Prop}$.

### Comparing notions of plump ordinal

However, if we do assume propositional resizing, then $\mathrm{POrd}$ 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 $\mathrm{POrd}_{/x}$ lives in the smaller universe. But we can use a different construction of a map $f:\mathrm{POrd} \to \sum_{A:\mathrm{Ord}} \mathrm{isPlump}(A)$: we use recursion on $\mathrm{POrd}$, with the formula

$f(\mathrm{sup}(x)) = \bigcup_a f(x_a)^+.$

Here $A^+$ denotes the plump successor: the set of all plump ordinals $C$ such that $C\le B < A$ for some $B$, with order inherited from $\mathrm{Ord}$. The recursion principle for $\mathrm{POrd}$ says that we need to simultaneously prove that this definition of $f$ preserves inequalities.

For $\le$, if we have $x_a < y$ for every $a:A$, so that $\mathrm{sup}(x)\le y$, then by the inductive hypothesis each $f(x_a) < f(y)$. It will suffice to show that this implies $f(x_a)^+ \le f(y)$, i.e. that if $C$ is a plump ordinal with $C\le B < f(x_a)$, then $C< f(y)$. But since < is transitive, we have $C \le B < f(y)$, so since $f(y)$ is plump, $C< f(y)$.

For <, if we have $x \le y_a$ for some $a$, so that $x < \mathrm{sup}(y)$, then by the inductive hypothesis $f(x) \le f(y_a)$. And certainly $f(y_a) < f(\mathrm{sup}(y))$, so by plumpness of $f(\mathrm{sup}(y))$, we have $f(x) < f(\mathrm{sup}(y))$.

Note that Taylor's definition of plumpness is exactly what we need to make the definition of $f$ go through. It's now fairly straightforward to verify that $f$ is an equivalence; its inverse is $i:\mathrm{Ord}\to \mathrm{No}$ (which obviously factors through $\mathrm{POrd}$). Thus, $\mathrm{POrd}$ is equivalent to the subset of plump ordinals in $\mathrm{Ord}$.

Exercise: Define a pseudo-ordinal to be a surreal defined by a cut $\{ x^L \,|\, \}$ 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 $\mathrm{POrd}$)” is equivalent to LEM.

This entry was posted in Higher Inductive Types. Bookmark the permalink.

### 3 Responses to The surreals contain the plump ordinals

1. Toby Bartels says:

Since mathforge.org is down, I note here that I fixed an error at [[nlab:plump ordinal]] (unless you meant something different by the minus sign than most people do.

• Mike Shulman says:

Thanks, but I think your fix didn’t quite do the job either — both of our definitions were actually defining equality and apartness rather than non-strict and strict inequality! I’ve backpedaled the mention of real numbers a bit; someone more expert can add more details if they like.

• Toby Bartels says:

You’re right! But that’s easy to fix by removing the absolute value bars. I’ll do that.