From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/85 Path: news.gmane.org!not-for-mail From: Thomas Streicher Newsgroups: gmane.science.mathematics.categories Subject: Re: Dedekind versus Cauchy reals Date: Fri, 13 Feb 2009 13:28:54 +0100 Message-ID: Reply-To: Thomas Streicher NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: ger.gmane.org 1234549280 19974 80.91.229.12 (13 Feb 2009 18:21:20 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Fri, 13 Feb 2009 18:21:20 +0000 (UTC) To: Andrej Bauer , categories@mta.ca Original-X-From: categories@mta.ca Fri Feb 13 19:22: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 1LY2g1-00087G-BU for gsmc-categories@m.gmane.org; Fri, 13 Feb 2009 19:22:13 +0100 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1LY282-0000su-Lr for categories-list@mta.ca; Fri, 13 Feb 2009 13:47:06 -0400 Content-Disposition: inline Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:85 Archived-At: Dear Andrej, wasn't aware of the fact that insisting on fixed rate of convergence can make things slower. My argument BTW was not about speed but rather about the ability to read off the desired result. In case of Cauchy sequences I need the modulus of convergence to know when I am close enough. In case of Dedekind reals that's not needed PROVIDED the left and the right set are given by enumerations of rationals. I "just" have to wait till close enough approximations from left and right have been enumerated. But is it right that in your implementation the left and right cuts are given by ENUMERATIONS of its elements and now via semidecision procedures? I guess so. Well, but when considering Dedekind cuts this way it essentially boils down to introducing reals as interval nestings (as done in High School sometimes). So really the question is whether Cauchy sequences or interval nestings are better. The way I interpret your remarks is that interval nesting is better since it allows one to avoid moduli of continuity which is good since fixed rate of convergence is a source of inefficiency. I think even constructivists refuting impredicativity have no problem to embrace representations by interval nestings. If I am not mistaken one finds this also in Martin-Loef's 1970 book. Thomas