From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/46 Path: news.gmane.org!not-for-mail From: Vaughan Pratt Newsgroups: gmane.science.mathematics.categories Subject: Re: "Kantor dust" Date: Fri, 06 Feb 2009 16:37:11 -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 1234013612 14028 80.91.229.12 (7 Feb 2009 13:33:32 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sat, 7 Feb 2009 13:33:32 +0000 (UTC) To: categories list Original-X-From: categories@mta.ca Sat Feb 07 14:34:47 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 1LVnKY-00066W-W4 for gsmc-categories@m.gmane.org; Sat, 07 Feb 2009 14:34:47 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LVmdG-0006rr-Iz for categories-list@mta.ca; Sat, 07 Feb 2009 08:50:02 -0400 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:46 Archived-At: 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? 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. Are these constructively different from the binary reals? And if so, is there any intuition underlying that difference that is as clear-cut as the difference between either and the Dedekind reals? > >> is there a topos in >> which the order type of the Freyd coalgebra is not that of the (forward) >> lexicographic ordering of N^N (modulo endpoints)? > > 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. But neither will the nonconstant functions from N^N to N be continuous with respect to the order interval topology on N^N lexicographically ordered. So I don't see any progress here towards distinguishing the order type of the Freyd coalgebra from the lexicographic order on N^N, in this topos or any other. Vaughan Pratt