From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/47 Path: news.gmane.org!not-for-mail From: "Prof. Peter Johnstone" Newsgroups: gmane.science.mathematics.categories Subject: Re: "Kantor dust" Date: Sat, 7 Feb 2009 17:18:29 +0000 (GMT) Message-ID: Reply-To: "Prof. Peter Johnstone" NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Trace: ger.gmane.org 1234039421 24723 80.91.229.12 (7 Feb 2009 20:43:41 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sat, 7 Feb 2009 20:43:41 +0000 (UTC) To: Vaughan Pratt , categories list Original-X-From: categories@mta.ca Sat Feb 07 21:44:56 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 1LVu2p-0007Hl-RJ for gsmc-categories@m.gmane.org; Sat, 07 Feb 2009 21:44:55 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LVtPW-00034X-7B for categories-list@mta.ca; Sat, 07 Feb 2009 16:04:18 -0400 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:47 Archived-At: On Fri, 6 Feb 2009, Vaughan Pratt wrote: > > Toby Bartels wrote: >> But it's not a constructive theorem that every such x has a binary >> expansion. >> That's still a neat result, that the binary reals are given by N^N, >> but the binary reals aren't constructively the same as the reals. > > Whose reals, Cauchy's or Dedekind's? Toby was of course referring to the Dedekind reals, but your binary reals are not constructively either the Cantor or the Dedekind reals. 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. > If the latter then that's no > surprise---carrying out constructions with open order filters is less > constructive than with the Cauchy sequence concept. Lubarsky and > Rathien in Logic and Analysis 1:2 131-152 have recently made the point > that whereas Cauchy reals can be understood constructively as a set, any > attempt to make Dedekind's reals constructive turns them into a proper > class. > > Between Dedekind cuts and Cauchy sequences, the more appropriate notion > of reals for constructive analysis would surely be the Cauchy reals. I could take issue with you on this. If you insist that "constructive" entails "predicative", then you are of course right; but in a topos- theoretic context, where you don't have countable choice automatically available, it's very much the other way round. >> >> In the topos of sheaves on the real line, >> every function from [0,1) to N is constant, >> yet there are obviously many other functions from N^N to N. >> Thus N^N and [0,1) are not constructively isomorphic as sets, >> so there is no way to give N^N the order type of [0,1) constructively. > > Let's compare apples with apples here. There are presumably going to be > nonconstant *functions* from the Freyd coalgebra object to 2 in this > topos, although they won't be continuous with respect to the topology > induced on that object by its coalgebra structure. No -- that's the whole point. In the topos of sheaves on R (better, in the gros topos of sheaves on topological spaces) every function R --> R is continuous, hence every function [0,1] --> 2 is constant. Peter Johnstone