Re: "Kantor dust"

[Toby Bartels <toby+categories@ugcs.caltech.edu>]

Dusko Pavlovic wrote in part:

[Prof. Johnstone responded to most of this, but I want to address one point.]

>there are
>many things that need to be computed with the reals, and no one
>representation fits for all purposes. so the statement

>>nobody uses the binary reals

>probably has more counterexamples than, say, the statement "nobody
>uses toposes". even if "the" binary reals were completely wrong.

What I meant is that no practising constructivist accepts
that the binary reals are the (or a) good notion of real number,
especially since no practising constructivist believes they form a ring.
I don't intend this as a dogamatic statement, and I'd be very interested
to here of any exceptions, but nevertheless I believe that it is true.

I certainly don't mean that nobody, not even a constructivist,
uses the binary reals as an approximation to real numbers
for the purposes of convenient calculations.
And of course, classical mathematicians do believe
that the binary reals are (all of) the reals.

As I suggested in a reply to Steve Stevenson,
constructive mathematics is about what can in principle be computed exactly.
What can in practice be computed closely enough is another question,
quite a useful one to ask but not at all the same thing.
(And what can in practice be computed exactly is another good question,
 one that I'm interested in but don't know enough about.)


--Toby