Chapter 11 Notes

Defining algebraic operations on Dedekind reals, especially multiplication, is both somewhat tricky and tedious.There are several ways to get arithmetic going: each has its own advantages, but they all seem to require some technical work.For instance, Richman [Richman:reals] defines multiplication on the Dedekind reals first on the positive cuts and then extends it algebraically to all Dedekind cuts, while Conway [conway:onag] has observed that the definition of multiplication for surreal numbers works well for Dedekind reals.

Our treatment of the Dedekind reals borrows many ideas from [BauerTaylor09] where the Dedekind reals are constructed in the context of Abstract Stone Duality.This is a (restricted) form of simply typed $\lambda$-calculus with a distinguished object $\mathrm{\Sigma }$ which classifies open sets, and by duality also the closed ones. In [BauerTaylor09] you can also find detailed proofs of the basic properties of arithmetical operations.

The fact that ${ℝ}_{𝖼}$ is the least Cauchy complete archimedean ordered field, as was proved in RC-initial-Cauchy-complete, indicates that our Cauchy reals probably coincide with the Escardó-Simpson reals [EscardoSimpson:01].It would be interesting to check whether this is really the case. The notion of Escardó-Simpson reals, or more precisely the corresponding closed interval, is interesting because it can be stated in any category with finite products.

In constructive set theory augmented by the “regular extension axiom”, one may also try to define Cauchy completion by closing under limits of Cauchy sequences with a transfinite iteration.It would also be interesting to check whether this construction agrees with ours.

It is constructive folklore that coincidence of Cauchy and Dedekind reals requires dependent choice but it is less well known that countable choice suffices. Recall that dependent choicestates that for a total relation $R$ on $A$, by which we mean $\forall (x:A).\exists (y:A).R(x,y)$, and for any $a:A$ there merely exists $f:\mathbb{N}\to A$ such that $f(0)=a$ and $R(f(n),f(n+1))$ for all $n:\mathbb{N}$. Our when-reals-coincide uses the typical trick for converting an application of dependent choice to one using countable choice. Namely, we use countable choice once to make in advance all the choices that could come up, and then use the choice function to avoid the dependent choices.

The intricate relationship between various notions of compactness in a constructivesetting is discussed in [bridges2002compactness]. Palmgren [Palmgren:FT] has agood comparison between pointwise analysis andpointfree topology.

The surreal numbers were defined by [conway:onag], using a sort of inductive definition but without justifying it explicitly in terms of any foundational system.For this reason, some later authors have tended to use sign-expansions or other more explicit presentations which can be coded more obviously into set theory.The idea of representing them in type theory was first considered by Hancock, whileSetzer and Forsberg [forsbergfinite] noted that the surreals and their inequality relations and $\le$ naturally form an inductive-inductive definition.The higher inductive-inductive version presented here, which builds in the correct notion of equality for surreals, is new.