From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/51 Path: news.gmane.org!not-for-mail From: Paul Taylor Newsgroups: gmane.science.mathematics.categories Subject: Re: "Kantor dust" Date: Sun, 8 Feb 2009 15:03:04 +0000 Message-ID: Reply-To: Paul Taylor NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 (Apple Message framework v624) Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1234127749 785 80.91.229.12 (8 Feb 2009 21:15:49 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sun, 8 Feb 2009 21:15:49 +0000 (UTC) To: Categories list Original-X-From: categories@mta.ca Sun Feb 08 22:17:02 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 1LWH1L-0001cn-Vz for gsmc-categories@m.gmane.org; Sun, 08 Feb 2009 22:16:56 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LWGQu-0002qe-G5 for categories-list@mta.ca; Sun, 08 Feb 2009 16:39:16 -0400 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:51 Archived-At: There have been several very interesting comments on this thread, but I would like to repeat my request that people should be clear about WHICH OF MANY "CONSTRUCTIVE" THEORIES OF MATHEMATICS they mean as the context of their comments. There are, as I said, interesting mathematical points to be made, both within each of these theories, and by comparing them. However, without a clear statement of the foundational context, the discussion degenerates. The original question was about Cantor space, rather than either the Cauchy or Dedekind reals. If you want to construct Cantor space from the reals by the "missing third" construction, I would think that it makes little difference whether you start from Cauchy or Dedekind. Or, indeed, from binary sequences, which of course form a Cantor space in the first place, so that is really a question of how to construct the reals from Cantor space rather than vice versa. Vaughan Pratt said > between Dedekind cuts and Cauchy sequences, the more appropriate notion > of reals for constructive analysis would surely be the Cauchy reals and I am certainly aware that, as a sociological fact, many type theorists and exact real arithmetic programmers believe this. Can anybody point me to a reasoned critique, or justification of the view that Cauchy sequences are "more appropriate" for purposes such as these? All that I have ever heard is essentially a condemnation of Dedekind for the "heresy" of impredicativity, uncountability, non-computability, being a proper class, etc. I gave a lecture (see PaulTaylor.EU/slides) entitled "In defence of Dedekind and Heine--Borel", which I presented as if I were an advocate in a court of law. Several type theorists and constructive analysts were present. Beforehand, I had asked around for a statement of "the case against Dedekind", but nobody seemed to be able to state it for me. Five years ago I had no opinion whatever on these matters, but, as you gather, I now consider that both Dedekind completeness and the Heine-- Borel theorem are essential parts of "constructive" analysis. Of course, I think that because the reals in Abstract Stone Duality satisfy them (and because it puts me in agreement with mainstream analysts). However, ASD is a recursively axiomatised and enumerable theory. I don't like the notions of (un)countability or (im)predicativity, but, if you must apply them, ASD is countable and predicative. Regarding computation, last year Andrej Bauer gave a "proof of concept" demonstration that one can compute efficiently with Dedekind reals in the ASD language for R. This of course uses interval arithmetic, but in fact it also makes extremely novel use of back-to-front ("Kaucher") intervals, which appear but are very badly presented in the interval analysis literature. I have been trying to persuade him to make this work publicly available. Since I'm talking about the reals in ASD, I should say what the difference is between the Cauchy and Dedekind reals is there. I haven't actually written out a construction of the Cauchy reals, but the evidence that I do have is that THEY ARE THE SAME. More precisely, Dedekind completeness is inter-derivable with sobriety for R, just as definition by description is equivalent to sobriety of N. This means that if you construct the "Cauchy reals" as a quotient of Cantor space by an equivalence relation (this is known as the "signed binary" representation of reals) within ASD then the result will be Dedekind complete. The details of this are set out in Section 14 of "The Dedekind reals in ASD" by Andrej and me, www.PaulTaylor.EU/ASD/dedras I think it is worth making a note of Vaughan's earlier comment that > In concrete Stone duality, increasing structure on one side is offset > by > decreasing structure on the other. One would hope for a similar > phenomenon in abstract Stone duality. > > If we can consider constructivity as part of the structure of an > object, > then we should expect that the more constructive some type of object, > the less constructive the "object of all objects of that type." So > for > example if (total) recursive functions are demonstrably more > constructive than partial recursive functions by some criterion, we > should expect the set of all recursive functions to be *less* > constructive than that of partial recursive functions by the same > criterion, rather than more. > > The phenomena you're observing here seem entirely consistent with this > principle, and point up the need to be clear, when judging > constructivity in some context, whether it is the collection or the > individuals therein being so judged, with the added complication that > Stone duality makes the roles of collection and individual therein > interchangeable, such as when elements of sets are understood as > ultrafilters of Boolean algebras. However, I think that the Galois--Stone contravariance applies WITHIN a particular foundational system, and not to VARIATIONS of the degree of constructivity. Indeed, the usual experience in setting up a Galois connection or Stone adjunction is that, in order to make the comparison work at all, you need to make additional assumptions. Paul Taylor