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<z 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 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.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s