Re: Dedekind versus Cauchy reals

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

Dear Andrej,

wasn't aware of the fact that insisting on fixed rate of convergence can make
things slower. My argument BTW was not about speed but rather about the ability
to read off the desired result. In case of Cauchy sequences I need the modulus
of convergence to know when I am close enough. In case of Dedekind reals that's
not needed PROVIDED the left and the right set are given by enumerations of
rationals. I "just" have to wait till close enough approximations from left
and right have been enumerated.
But is it right that in your implementation the left and right cuts are given
by ENUMERATIONS of its elements and now via semidecision procedures?
I guess so.
Well, but when considering Dedekind cuts this way it essentially boils down
to introducing reals as interval nestings (as done in High School sometimes).
So really the question is whether Cauchy sequences or interval nestings are
better. The way I interpret your remarks is that interval nesting is better
since it allows one to avoid moduli of continuity which is good since fixed
rate of convergence is a source of inefficiency.

I think even constructivists refuting impredicativity have no problem to
embrace representations by interval nestings. If I am not mistaken one finds
this also in Martin-Loef's 1970 book.

Thomas