Chapter 11 Notes

Defining algebraic operations on Dedekind reals, especially multiplicationPlanetmathPlanetmath, is both somewhat tricky and tedious. There are several ways to get arithmeticPlanetmathPlanetmath 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 cutsMathworldPlanetmath, while Conway [conway:onag] has observed that the definition of multiplication for surreal numbersMathworldPlanetmath 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 λ-calculus with a distinguished object Σ 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 operationsMathworldPlanetmath.

The fact that 𝖼 is the least Cauchy completePlanetmathPlanetmathPlanetmathPlanetmathPlanetmath archimedeanPlanetmathPlanetmath ordered field, as was proved in \autorefRC-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 intervalMathworldPlanetmathPlanetmath, is interesting because it can be stated in any category with finite productsPlanetmathPlanetmath.

In constructive set theory augmented by the “regular extension axiom”, one may also try to define Cauchy completion by closing under limits of Cauchy sequencesMathworldPlanetmathPlanetmath 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 choice states that for a total relation R on A, by which we mean (x:A).(y:A).R(x,y), and for any a:A there merely exists f:A such that f(0)=a and R(f(n),f(n+1)) for all n:. Our \autorefwhen-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 constructive setting is discussed in [bridges2002compactness]. Palmgren [Palmgren:FT] has a good comparison between pointwise analysisMathworldPlanetmath and pointfree 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 theoryMathworldPlanetmath. The idea of representing them in type theoryPlanetmathPlanetmath was first considered by Hancock, while Setzer and Forsberg [forsbergfinite] noted that the surreals and their inequality relations < and 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.

Title Chapter 11 Notes