Re: Cauchy completeness of Cauchy reals

["Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>]

On Fri, 24 Jan 2003, Dusko Pavlovic wrote:

> >
> >
> >Set. Do you think your construction works in any topos?
> >
> the coalgebraic structures are defined using just arithmetic. in the
> first one, there is the "no infinite sequences of 1s" condition, which i
> am reminded depends on markov's principle; but that is just used in the
> explanation. i don't think there are other constraints.
>
> >If so, what
> >would "Cauchy reals" mean precisely in this general context?
> >
> it means fundamental sequence, with the equivalence relation in the
> "lazy" mode, a la bishop, as described in andrej bauer's message.
>
I'm sorry, but this won't do. In a topos, equality is equality; you can't
treat it "lazily". So a Cauchy real has to be an equivalence class of
Cauchy sequences, and there is in general no way of choosing a
canonical representative for it. Markov's principle would, I think
(I haven't checked the details), suffice to give a canonical
representation as a binary expansion with no infinite sequence of
1's, and then Dusko's argument would suffice to show that the Cauchy
reals are Cauchy complete. But there are many toposes where Markov's
principle fails.

I doubt very much whether the Cauchy reals occur
as a final coalgebra for anything, in any topos where they fail to
coincide with the Dedekind reals, simply because the Dedekind reals
are likely to be a coalgebra for the same endofunctor (and they're
more "final" than the Cauchy reals). Incidentally, Peter Freyd and
I worked out how to do his coalgebra construction constructively,
and I showed that its final coalgebra is the Dedekind interval in any
topos -- the proof is in the Elephant, at the end of section D4.7.

Peter Johnstone