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