From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/57 Path: news.gmane.org!not-for-mail From: Dusko Pavlovic Newsgroups: gmane.science.mathematics.categories Subject: Re: "Kantor dust" Date: Mon, 9 Feb 2009 22:18:44 +0000 (GMT) Message-ID: Reply-To: Dusko Pavlovic NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Trace: ger.gmane.org 1234271545 25028 80.91.229.12 (10 Feb 2009 13:12:25 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Tue, 10 Feb 2009 13:12:25 +0000 (UTC) To: "Prof. Peter Johnstone" , Original-X-From: categories@mta.ca Tue Feb 10 14:13:40 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 1LWsQk-0007Sr-79 for gsmc-categories@m.gmane.org; Tue, 10 Feb 2009 14:13:38 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LWriU-000088-W1 for categories-list@mta.ca; Tue, 10 Feb 2009 08:27:55 -0400 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:57 Archived-At: hi. i missed most of this thread, but even this one message that i did catch raises several questions that i would like to share. 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.) 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? COMMENT: IF the answer to either of the above questions is NO, then maybe the tacit SLOGAN that "constructively valid" = "true in every topos" needs to be taken *very carefully*. when we build toposes over classical universes, then we may be able to force away more than any constructivist would ever reject. the strict constructivist logics have already been marginalized as too restrictive; lets not completely bury them just for the joy of constructing counterexamples. moreover, EVEN IF the answer to both of the above questions is YES, the above SLOGAN still does not tell the whole story, IMHO. the constructivists wanted to make our computations effective. that goal led to some great philosophical debates in the first half of XX century. later people built computers and paid lots of programmers to make computations effective. besides brouwer, and heyting and kolmogorov, maybe we should admit that people like gosper, and knuth, and dijkstra, and our own vaughan pratt, also have an idea about what is effectively computable. peter johnstone points out that the comparison test for the binary reals (i presume the reals in base 2; there are many other representations, of course) is undecidable. this actually applies to every base, and even to the continued fraction representation (because it is irredundant). but in the practice of effective computations, this is no showstopper. there are many things that need to be computed with the reals, and no one representation fits for all purposes. so the statement > nobody uses the binary reals probably has more counterexamples than, say, the statement "nobody uses toposes". even if "the" binary reals were completely wrong. the study of the various effective algebraic operations on the reals, always reduced to one binary form or another, goes back at least to gosper and schroepel, the original "hackers" from the 70s. they were, of course, aware that the comparison test was undecidable. buyt people prefer to run a program that may not terminate, or will terminate fast, over a program guaranteed to terminate between tomorrow and 2 years from now. gosper's continued fraction representation was improved by jean vuillemin, who proposed in 1990s a redundant representation, where the comparison test is decidable. this is what at least some people have really been using in their real projects, sensitive enough to bring the chaotic effects of the floating point arithmetic to the surface. it would be interesting to understand whether the notion of computability as embodied in toposes is related in some rational way with the notion of computability as embodied in computers. -- dusko