Re: "Kantor dust"

[Vaughan Pratt <pratt@cs.stanford.edu>]

Vaughan Pratt wrote:
> Similar reasoning should also rehabilitate the constructivity of binary
> fractions, where the final coalgebra surely deletes the open set
> separating 0111... from 1000...  Perhaps ASD has something to say about
> this---Paul?

Unfortunately the reasoning is not similar enough to make this work.
The crucial difference is that in the representation of [0,oo) ~
[0,1)[1,2)[2,3)... as N^N, there is no largest element of [0,1) whence
the Scott topology omits the open set separating [0,1) from [1,0).  With
binary fractions however we have two points 0111... and 1000... with
nothing between them and the inequality 0111... < 1000..., which the
Scott topology must respect by preserving the open set separating them.

There is (as far as I'm aware) no such localic alternative of the kind I
was envisaging to either omitting 0111... or identifying it with
1000..., both of which are intrinsically spatial solutions to the
problem of converting Cantor space 2^N to the continuum.  In contrast
the Alexandroff-to-Scott conversion of N^N to the continuum is localic
in character, in that it operates on open sets instead of points.

The crucial difference between classical and sheaf-theoretic toposes is
that localic procedures are meaningless in the former.  The latter
permit the finer distinctions to be drawn that are needed to explicate
constructivity, starting with the distinction between not-not and identity.

(Unlike some other buggy posts of mine that I've been able to retract
before Bob forwarded them to the list, this one went through too
promptly for me to catch it in time.  I made this mistake by incorrectly
visualizing the gap between 0111... and 1000... as though it were the
gap between

     .0 < .01 < .011 < .0111 < ... and ... < .1000 < .100 < .10 < .1

This makes no sense (a) because the finite sequences on the right should
all be identified and (b) there are no finite sequences to begin with,
the binary fractions are properly understood as infinite sequences,
namely maps N --> 2.  The paragraph was an afterthought I tacked on with
insufficient consideration before posting.)

Vaughan Pratt