From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/87 Path: news.gmane.org!not-for-mail From: gcuri@math.unipd.it Newsgroups: gmane.science.mathematics.categories Subject: Re: Dedekind versus Cauchy reals Date: Fri, 13 Feb 2009 16:05:14 +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 1234549401 20390 80.91.229.12 (13 Feb 2009 18:23:21 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 13 Feb 2009 18:23:21 +0000 (UTC) To: categories@mta.ca Original-X-From: categories@mta.ca Fri Feb 13 19:24:35 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 1LY2iG-0000bU-TA for gsmc-categories@m.gmane.org; Fri, 13 Feb 2009 19:24:33 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LY29C-00012A-2C for categories-list@mta.ca; Fri, 13 Feb 2009 13:48:18 -0400 Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:87 Archived-At: Quoting Paul Taylor : > > > Toby has also said a lot of interesting things about many different > systems. These illustrate my point that it is essential to state > which system, or which notion of "constructivity" you intend. > > He has said, for example > * 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). > * The Cauchy reals exist an a Pi-W-pretopos (equivalently, in a > constructive set or type theory with exponentiation but no power > sets or even fullness and with infinity but no countable choice). > * But the Dedekind reals, as far as [he] can tell, do not; excluded > middle, power sets, fullness, or countable choice would each do the > job, but you need ~something~. > > I would challenge someone to consider the last of these questions > seriously, maybe taking a hint from the second. ASD provides another, > as it uses lambda term over a special object instead of talking about > "sets" of rational numbers. A note concerning the possibility of constructing the Dedekind reals with= out fullness, etc: the Dedekind reals can be defined in constructive set theory even withou= t excluded middle, power sets, fullness, or countable choice. The point is = that they then form a class and not a set. Class-sized objects are however the norm in a constructive predicative se= tting. For instance, a (non-trivial) locale is carried by a class that is never = a set; in general a formal space or formal topology is a large object too, so th= at one often deals with superlarge "categories" with large homsets. Giovanni Curi Dipartimento di Matematica Pura ed Applicata Universita' degli Studi di Padova www.math.unipd.it