This is a reply to Chris Mulvey's and Mamuka Jibladze's messages. Chris Mulvey's message nicely illustrates Martin Escardo's point that there are different senses in which one might understand Cauchy completion. As Chris confirms, it has long been known that, in toposes not satisfying number-number choice, the Cauchy reals, i.e. the set of Cauchy sequences (with modulus) quotiented by the obvious equivalence, are problematic. Chris takes Cauchy complete to mean complete w.r.t. "Cauchy approximations" which he defines as:
Without countable choice, you still have an inhabited subset of the rationals consisting of all rationals at a distance of < 1/n from the Dedekind cut. This gives you a sequence of such subsets - a Cauchy approximation to the real.
As he remarks, it is well known that the Cauchy reals need not be Cauchy complete w.r.t. Cauchy approximations. Moreover, their "Cauchy completion" is the object of Dedekind reals. Thus, any of the familiar toposes in which Cauchy and Dedekind reals differ (e.g. sheaves on R) provides an example in which the Cauchy reals are not Cauchy complete w.r.t. Cauchy approximations. The above story repeats itself exactly if one changes the meaning of Cauchy completeness to mean completeness w.r.t. a suitable notion of "Cauchy" filter. However, Andrej Bauer was referring to Cauchy completeness in a different sense. A very natural definition of Cauchy completeness is to merely require completeness w.r.t. Cauchy sequences (with modulus) of elements. This is weaker than the definitions above. The open(?) question Andrej referred to is to find an example of a topos (if one exists) in which the Cauchy reals are not themselves Cauchy complete w.r.t. convergent sequences. For this, one of course requires a topos in which the Cauchy and Dedekind reals differ (as the latter are complete). However, the standard examples of such toposes (e.g. sheaves on R) do not answer the question, for, in them, the Cauchy reals do turn out to be complete w.r.t. sequences. One might object to the above question on the grounds that completeness w.r.t. sequences is not the "correct" notion in a topos. There is some validity to this. However, the question originally arose because Martin Escardo and I came up with a definition of an "interval object" (an object of a category corresponding to the closed interval [0,1] in much the same way that a "natural numbers object" corresponds to the natural numbers) that makes sense in the very general setting of an arbitrary category with finite products. When interpreted in Set, the interval object is the interval [0,1]. When interpreted in Top it is the interval with Euclidean topology. When interpreted in an elementary topos, the interval object turns out to be the interval [0,1] constructed within the "Cauchy completion w.r.t convergent sequences of the Cauchy reals within the Dedekind reals", where the quotes are, once again, because the phrase needs careful interpretation. For mathematical details, see our paper in LICS 2001 "A Universal Characterization of the Closed Euclidean Interval". Our approach apparently has something to say related to Mamuka Jiblaze's question. For us the interval is defined as an algebra (implementing an algebraic notion of convexity) freely generated by the object 1+1. In Top, one can replace 1+1 by Sierpinski space as the generating object, in which case the interval with the topology of lower semicontinuity (equivalently the Scott topology) is obtained. Similarly, in a topos, one might take non-decidable objects (e.g. interesting "dominances" in the sense of Rosolini) as generating objects. We have not pursued this latter direction at all, but it might be interesting to do so. Alex Simpson Alex Simpson, LFCS, Division of Informatics, Univ. of Edinburgh Email: Alex.Simpson@ed.ac.uk Tel: +44 (0)131 650 5113 Web: http://www.dcs.ed.ac.uk/home/als Fax: +44 (0)131 667 7209