What does it take to identify the field and the continuum of reals?

[Vaughan Pratt <pratt@CS.Stanford.EDU>]

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