What does it take to identify the field and the continuum of reals?
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
Vaughan Pratt wrote in part: [about Conway's surreal numbers]
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).
It's my understanding that you don't get a field until (just before) day K for K an inaccessible cardinal number. I'm not 100% certain about this, however! -- Toby Bartels
Vaughan Pratt writes:
I would bounce this question back to Martin: what did he mean by "th= e Dedekind reals" in his attribution to Freyd?
I meant (and still mean): the underlying object of the final coalgebra is what topos theorists know as "the object of Dedekind reals" (in an elementary topos with nno). In more detail [Freyd & Johnstone, in Johnstone's Elephant, pages 1028-1032]: given a topos with nno, consider the category of (internal) posets in the topos. In this category, define a functor. Consider its final coalgebra. Theorem: (1) It exists. (2) Moreover, the underlying object of the algebra is the Dedekind unit interval under its natural order. (3) The structure map performs average (x,y) |-> (x+y)/2 (for full details, see the reference). Answering the question quoted below, you get all the ingredients you are looking for: a *set* of numbers (as the underlying set of the underlying poset of the final coalgebra), its *order* (as the underlying object of the final coalgebra), and (part of) its *algebraic* structure (as the structure map of the final coalgebra). Of course, here "set" means an object of a topos, e.g. that of classical sets. You get only part of the *algebraic* structure, but topos logic is strong enough to allow you to fully recov= er=20 it after you have the final coalgebra in your hands.=20 The Escardo-Simpson approach is similar, but takes a different route and makes weaker assumptions - I won't repeat the story, which can be found in the paper whose reference was already given by Alex Simpson. Martin Escardo
participants (3)
-
Martin Escardo -
Toby Bartels -
Vaughan Pratt