Re: "Kantor dust"

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

Apropos of my

> PS. [...] That said, I would
> still like to know whether our final coalgebra, for FX = N x X where x
> is "lexicographic product" suitably defined for an NNO N in a topos, is
> or is not equally real in these toposes.  If it is then this would be a
> situation where apartness is not needed to produce the reals
> constructively, presumably contradicting Brouwer.

I returned to this question after a pleasant dinner this evening with
Sol Feferman, Paul Eklof, and Grisha Mints, and it occurred to me almost
immediately (my subconscious must have been working on it without my
permission) that in a topos over any sufficient category of topological
spaces (not that I have the faintest idea how to make that rigorous), it
must be the case that the final coalgebra for the functor F described
above is the "real reals."

The intuitition behind this is that N together with an upper bound
thereon (call it oo) has only two possible T0 topologies whose
specialization order is the standard linear one, namely the Alexandroff
and Scott topologies.  These differ by a single open set, which is
present in the former and absent from the latter.  In the former it
isolates oo from N, in the latter its absence allows oo to link up with
  N in the sense that every ultimately constant function on N must map
oo to the limiting value of that function.

There is a unique map from the Alexandroff to the Scott topology on this
set preserving the NNO structure, and no map back (where would you send
the Alexandroff open witnessing the solitude of oo?).  So in any
competition for a final coalgebra Scott is going to beat Alexandroff.

Now in N^N as a representation of the isomorphism [0,oo) ~
[0,1)[1,2)[2,3)..., the objection that will naturally be raised to any
claim that this could be the continuum is that, even though [0,1)[1,2)
*looks* like it should glue together seamlessly, its implementation in
terms of continued fractions will create a gap between [0,1) and [1,2)
that is not found in the "real reals".  While this gap cannot be used in
the topos Set to distinguish N^N from the Freyd coalgebra, where things
are so discrete that all realizations of the reals suffer from gaps, in
a more topologically sensitive topos it becomes possible to find open
sets willing to testify to these gaps in those cases where insufficient
care has been taken to bump off these witnesses, as surely happens when
one defines N^N naively as simply an exponential.  Implementing the glue
of the Freyd coalgebra via apartness bumps off all such witnesses to the
disconnectedness of the Freyd continuum, making it thus far the sole
survivor in this competition to define the reals constructively.  (If
there is another why isn't it in the Elephant?)

In any topos with sufficiently accommodating open sets as to permit this
Alexandroff-Scott distinction (surely not a tall order given that only
one open set need be removed to pass from Alexandroff to Scott), I claim
that the final coalgebra for the functor Dusko and I exhibited in our
CMCS'99 paper bumps off the Alexandroff open witnessing a gap between
[0,1) and [1,2), where the 1 in [1,2) plays the role of oo in my earlier
discussion of N and oo.

If the topos of sheaves on R, or on whichever essentially small version
of Top Peter Johnstone prefers over R itself, does not result in
removing this open set in a way that leaves no other witnesses to
disconnectedness then I will be bitterly disappointed.

If it does however then we have what as far as I'm aware must be the
first alternative since Brouwer to apartness in formulating the
continuum to the constructive standards set by toposophers.  And
moreover using much older technology than the Freyd coalgebra, namely
good old continuous fractions (done right of course, none of this
antimonotone 1/(1+x) stuff totally disconnecting them).

(How old?  Continued fractions are ancient, appearing in Euclid and no
doubt going back a lot further as with much of Euclidean mathematics.
They are a very natural and convenient way of representing reals, though
with subtleties to trip one up, just as with the Freyd coalgebra.)

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?

Vaughan Pratt