Re: "Kantor dust"

["Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>]

On Tue, 10 Feb 2009, Vaughan Pratt wrote:

> 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."
>
Whoa! This simply can't work. Whatever the final coalgebra for N x (-)
looks like, it must (thanks to Lambek) be isomorphic to N x itself,
and therefore (since equality for N is decidable) must have lots of
complemented subobjects {0} x itself, {1} x itself, ... The point of
the continuity theorem for functions R --> R is that there are toposes
in which R has *no* nontrivial complemented subobjects -- indeed, in
which the sentence

(\forall S : PR)((\forall x : R)((x \in S) \vee \neg(x\in S))
     \implies ((S = R)\vee (S = \emptyset)))

is valid. This is purely a matter of logic: it has nothing to do with
the order, topological or any other sort of structure carried by
the final coalgebra. So invoking Alexandroff and Scott isn't going to
help at all. The only way to get round it (apart from using glue)
is to replace N by some "nonstandard natural number object" having no
nontrivial complemented subobjects -- but where you get that from, I
don't know.

Peter