By way of motivating the question posed in the subject line I'll pick up in the middle of this thread on Dedekind vs. Cauchy reals, which I can't help much with I'm afraid but which provides a nice jumping off point for my real topic nonetheless.
From: Martin Escardo
From: Dusko Pavlovic
From: Martin Escardo NB. Freyd characterized the Dedekind reals as a final coalgebra. Alex Simpson and I characterized "the Cauchy completion of the rationals within the Dedekind reals" as a free algebra
and vaughan pratt and i characterized the cauchy reals as a final coalgebra. the papers are i proceedings of CMCS 99 and in TCS 280.
I forgot to mention this --- I apologize. In your paper, you work in Set. Do you think your construction works in any topos? If so, what would "Cauchy reals" mean precisely in this general context? Thanks.
I would bounce this question back to Martin: what did he mean by "the Dedekind reals" in his attribution to Freyd? Both the Pavlovic-Pratt and Freyd constructions of the continuum as a final coalgebra characterize the continuum only up to its order type (and hence up to homeomorphism if we take the usual order topology generated by the open intervals). Cuts in the *field* Q of rationals inherit Q's metric, but cuts in the *poset* Q acquire only topology. Only with Q qua poset would it be fair to say that either Peter's or our coalgebraic construction of the continuum "characterized the Dedekind reals." The Cauchy completion of the rationals on the other hand requires Q to be at minimum a metric space and surely a field if you want to bring in 1/n. This distinction constitutes a disconnect between Martin's first two sentences that subsequent emails are at risk of propagating. I have not to date seen any really convincing marriage of the algebraic and coalgebraic approaches to defining real numbers. The very fact that algebra produces the field of reals while coalgebra produces the continuum as understood by descriptive set theorists draws a sharp line right there between the two approaches. The only marriage I'm aware of that even works at all is Conway's elegant construction of his surreal numbers. It is a marriage because (loosely speaking) the numbers entering on the ends create algebra while those interpolating their predecessors in the Conway ordering create coalgebra. A great virtue of this construction is its complete lack of any distinction between, or even reference to, algebra and coalgebra, the implicit presence of both notwithstanding. Unfortunately it produces neither the field of reals nor a continuum. Conway doesn't get the former because just before day omega he has only produced the ring of binary fractions, those rationals of the form m/2^n. Day omega itself however witnesses the birth not only of all the remaining reals but the first few infinities and infinitesimals, in particular ±w and their reciprocals. This doesn't even form an additive monoid let alone a ring since w+w for example is not due to arrive for another w days! Negation is the only arithmetic operation surviving the day-to-day evolution of Conway's surreal universe, from its little bang to its apocalyptic Field. Seeking closure, Conway slogs gamely on through *all* the ordinals to produce a Field of reals. (Or rather The Field, the maximal such having been shown elsewhere to be unique, if I've understood that correctly.) This being a proper class, not only does it not have the cardinality of the continuum, it doesn't have a cardinality at all! Now I conjecture that stopping just before day \epsilon_0, for the sake of getting a set, produces a field closed under all functions whose n-th bit is computable in time f(n) where f is definable in Peano arithmetic. And it may well be that Conway already has a field just before day \omega^\omega, I haven't checked but surely someone has by now (I'm very bad at keeping up with these things, sorry). But all this is for naught here, since even the smallest Conway field whatever it might turn out to be is cannot be Archimedean, for the reason above. And although it has the power of the continuum it lacks its order type: with the usual order topology, the Conway continuum becomes totally disconnected as soon as ±1 appear, and remains that way thenceforth. Total disconnectedness is not anything a continuum can be proud of. It seems to me that topos theory, or logic, or something in between if that makes sense, should have something to say about a gap between the algebra and coalgebra of the reals. Algebraically the reals form a field, coalgebraically they form a continuum. What is the logical strength of the weakest framework identifying these dual views of the reals? Vaughan Pratt