From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/62 Path: news.gmane.org!not-for-mail From: Greg Meredith Newsgroups: gmane.science.mathematics.categories Subject: Re: "Kantor dust" Date: Tue, 10 Feb 2009 13:05:26 -0800 Message-ID: Reply-To: Greg Meredith NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1234361789 23959 80.91.229.12 (11 Feb 2009 14:16:29 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 11 Feb 2009 14:16:29 +0000 (UTC) To: "Prof. Peter Johnstone" , categories@mta.ca Original-X-From: categories@mta.ca Wed Feb 11 15:17:43 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 1LXFtm-0000mG-Se for gsmc-categories@m.gmane.org; Wed, 11 Feb 2009 15:17:11 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LXFKX-00033v-FC for categories-list@mta.ca; Wed, 11 Feb 2009 09:40:45 -0400 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:62 Archived-At: Categorically minded, Many thanks for an interesting thread! Just out of curiousity, is the Conway construction clearly identified with the Dedekind reals? How does the construction fit into the constructivist debate? Best wishes, --greg On Mon, Feb 9, 2009 at 2:47 PM, Prof. Peter Johnstone < P.T.Johnstone@dpmms.cam.ac.uk> wrote: > On Mon, 9 Feb 2009, Dusko Pavlovic wrote: > > QUESTION 1: re peter johnstone's >> >> > > 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. >>> >> >> are you claiming that this statement is true with respect to every base >> topos >> and every real line in it? (the discussion seems to have touched upon the >> various constructions of the various real lines. it would be nice to know >> where is the one, over which you build the topos, is coming from.) >> >> That's actually a quote from Toby Bartels, not from me. > It's a statement about a topos built over the classical topos of sets; > the argument is a rather ad hoc one, and I'm not sure to what extent > it's possible to make it constructive. However, as I said elsewhere, I > prefer to work with the gros topos of spaces (i.e. sheaves on a suitable > full subcategory of spaces for the coverage consisting of jointly- > surjective families of open inclusions) and there it's quite clear > what you need: namely, Heine--Borel (equivalently, exponentiability > of R in your category of spaces). That's not true in all toposes; > you could try to get round it by basing your gros topos on locales > rather than spaces (the locale of formal reals being constructively > locally compact), but it's not clear (to me, at least) what the > result would actually mean if you based yourself on a topos where > the formal reals aren't spatial. > > QUESTION 2: is there a branch of constructivism that would reject as >> non-constructive the map N^N-->[0,1) obtained by interpreting the N^N as >> the >> coefficients of continued fractions? >> >> I don't think there is any doubt that the map exists. The problem is > that, > for most if not all schools of constructivism, it's wildly non-surjective. > > Peter Johnstone > > > > -- L.G. Meredith Managing Partner Biosimilarity LLC 806 55th St NE Seattle, WA 98105 +1 206.650.3740 http://biosimilarity.blogspot.com