From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/63 Path: news.gmane.org!not-for-mail From: Vaughan Pratt Newsgroups: gmane.science.mathematics.categories Subject: Re: "Kantor dust" Date: Tue, 10 Feb 2009 21:49:35 -0800 Message-ID: Reply-To: Vaughan Pratt NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1234361809 24055 80.91.229.12 (11 Feb 2009 14:16:49 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 11 Feb 2009 14:16:49 +0000 (UTC) To: categories list Original-X-From: categories@mta.ca Wed Feb 11 15:18:04 2009 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.50) id 1LXFtr-0000p8-8C for gsmc-categories@m.gmane.org; Wed, 11 Feb 2009 15:17:15 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXFMg-0003Je-65 for categories-list@mta.ca; Wed, 11 Feb 2009 09:42:58 -0400 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:63 Archived-At: 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