Re: "Kantor dust"

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

Prof. Peter Johnstone wrote on Feb. 7 at 17:18 GMT:
> The reason is that you have to know in advance that a binary
> sequence isn't going to end in an infinite string of 1's; by excluding
> those sequences, you make the question "Is x < 1/2?" decidable,
> which is not constructively true of either the Cantor reals or the
> Dedekind reals.

I had always been somewhat dissatisfied intuitively by the idea of
excluding sequences of the form 01111....  It seemed more natural to
identify them with those of the form 10000....  However I just assumed
that these were equivalent approaches.

Your point about making x < 1/2 decidable is a good one.  I'm now
convinced that it is better to identify than delete.  Identification can
be accomplished spatially, but perhaps it is more elegant to do so
localically, namely by removing the open set that separates the two
halves to be glued together.  In a T0 space, doing so will identify the
points anyway.  However in the situation [0,1)[1,2) of my previous
messages where there is no point on the left adjacent to the point 1 on
the right, identification of points is not an option.  The only
remaining concern then is whether there's an open set separating [0,1)
and [1,2).  Finality should eliminate spurious open sets that have no
reason to stick around.

Vaughan