From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/48 Path: news.gmane.org!not-for-mail From: Toby Bartels Newsgroups: gmane.science.mathematics.categories Subject: Re: "Kantor dust" Date: Sat, 7 Feb 2009 14:58:19 -0800 Message-ID: Reply-To: Toby Bartels NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: ger.gmane.org 1234103152 27955 80.91.229.12 (8 Feb 2009 14:25:52 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Sun, 8 Feb 2009 14:25:52 +0000 (UTC) To: categories list Original-X-From: categories@mta.ca Sun Feb 08 15:27:06 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 1LWAcc-00007P-CK for gsmc-categories@m.gmane.org; Sun, 08 Feb 2009 15:26:58 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LWA2p-0001nu-3U for categories-list@mta.ca; Sun, 08 Feb 2009 09:49:59 -0400 Content-Disposition: inline Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:48 Archived-At: Prof. Peter Johnstone wrote in part: >Vaughan Pratt wrote: >>Whose reals, Cauchy's or Dedekind's? >Toby was of course referring to the Dedekind reals Actually, I was trying to keep it open, since different schools of constructivism have different opinions about which are the correct reals (as well as which are equivalent). But nobody uses the binary reals, since they can't subtract them. (To get the first digit of 0.1000000000... - 0.01000000000..., you need to know which sequence, if either, stops repeating first.) I agree that one would default to Dedekind reals (or something equivalent), since that seems to be agreed on by the "practising" schools (that is, those constructivists trying to do ordinary mathematics, albeit constructively, rather than doing metamathematics). >>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. I'll have to read what they mean, but to say ~any~ attempt seems too strong. Even in a predicative theory, countable choice implies their equivalence, so are they claiming that countable choice is not constructive? (In my experience, Fred Richman is the only practising non-finitist analyst who doubts both excluded middle and countable choice.) The Dedekind reals can also be constructed in CZF (Peter Aczel's predicative constructive set theory) even if you remove countable choice, using subset collection aka fullness. Similarly, if you remove identity types from intensional type theory (so breaking the justification of countable choice), you can still justify the fullness axiom and so construct the Dedekind reals (albeit not literally as sets of rational numbers). >>Between Dedekind cuts and Cauchy sequences, the more appropriate notion >>of reals for constructive analysis would surely be the Cauchy reals. The experience in measure theory and Banach space theory since the 1980s suggests that a Dedekind-complete ordered field is needed. The only question is whether such a thing exists; most believe it does. (If countable choice or excluded middle holds, the Cauchy reals work, which takes care of nearly every practising analyst, constructive or not. Fred Richman, the only exception I know, still uses the Dedekind reals, although that's easy for him since he is not predicativist.) Note: everything above is about the ~located~ Dedekind reals; a located Dedekind cut is a pair (L,U) of order-open inhabited sets such that r in L and s in U => r < s => r in L or s in U. This is what Freyd's coalgebra construction produces, and it's what practising analysts want to use. --Toby