From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/49 Path: news.gmane.org!not-for-mail From: gcuri@math.unipd.it Newsgroups: gmane.science.mathematics.categories Subject: Re: "Kantor dust" Date: Sun, 8 Feb 2009 12:56:53 +0100 Message-ID: Reply-To: gcuri@math.unipd.it NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1234103306 28366 80.91.229.12 (8 Feb 2009 14:28:26 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sun, 8 Feb 2009 14:28:26 +0000 (UTC) To: categories@mta.ca Original-X-From: categories@mta.ca Sun Feb 08 15:29: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 1LWAf5-00017J-WD for gsmc-categories@m.gmane.org; Sun, 08 Feb 2009 15:29:32 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LWA3I-0001os-Pn for categories-list@mta.ca; Sun, 08 Feb 2009 09:50:28 -0400 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:49 Archived-At: Quoting "Prof. Peter Johnstone" : > > 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 poin= t > > that whereas Cauchy reals can be understood constructively as a set, = any > > attempt to make Dedekind's reals constructive turns them into a prope= r > > class. > > > > Between Dedekind cuts and Cauchy sequences, the more appropriate noti= on > > 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. Even if one insists that constructive entails predicative the appropriate= ness of Cauchy reals is questionable: Lubarsky and Rathjen prove in fact that in = a=20 subsystem of CZF (Aczel' constructive set theory), i.e., in CZF with Subset Collection replaced by exponentiation, the Dedekind reals form a = proper class. In ordinary CZF (that has no choice principle and no powersets), the Dedekind reals *do* form a set (Aczel & Rathjen), as do more generall= y the points of any weakly set-presented T^*_1 locale (Aczel & Curi), in particular of any locally compact regular one. It is also useful to recall that (in "On the Cauchy Completeness of the Constructive Cauchy Reals", MLQ, 53, No. 4-5 (2007), pp. 396-414) Lubarsky has proved that the Cauchy Reals are not complete in intuitioni= stic set theory without choice. There's then the point of view that, constructively, the reals should be considered as a `space', rather than a set, and that in this perspective = they are more properly regarded e.g. as a locale/formal space (rather than as = a set/class of points with a topology)... Regards, Giovanni Curi ----------------------------------------------------------------- This message was sent using IMP, the Internet Messaging Program. Dipartimento di Matematica Pura ed Applicata Universita' degli Studi di Padova www.math.unipd.it