From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2110 Path: news.gmane.org!not-for-mail From: Andrej Bauer Newsgroups: gmane.science.mathematics.categories Subject: Re: Generalization of Browder's F.P. Theorem? Date: 21 Jan 2003 19:11:24 +0100 Message-ID: References: Reply-To: Andrej Bauer NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: ger.gmane.org 1241018418 2533 80.91.229.2 (29 Apr 2009 15:20:18 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:20:18 +0000 (UTC) To: CATEGORIES LIST Original-X-From: rrosebru@mta.ca Tue Jan 21 19:21:02 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Tue, 21 Jan 2003 19:21:02 -0400 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18b7bZ-0003QS-00 for categories-list@mta.ca; Tue, 21 Jan 2003 19:14:53 -0400 In-Reply-To: Michael Barr's message of "Thu, 16 Jan 2003 18:05:39 -0500 (EST)" User-Agent: Gnus/5.0807 (Gnus v5.8.7) XEmacs/21.4 (Common Lisp) Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 35 Original-Lines: 48 Xref: news.gmane.org gmane.science.mathematics.categories:2110 Archived-At: Michael Barr writes: > For Bishop, a real number is an equivalence class of pairs of > RE sequences of integers a_n and b_n such that for all m,n |a_n/b_n - > a_m/b_m| < 1/m + 1/n ... Actually, Bishop purposely avoids taking a real to be an equivalence class of sequences, presumably because he does not want to assume the axiom of countable choice. A sequence as described above is sometimes called a "fundamental sequence". Two such sequences x = (a_n/b_n) and y = (c_n/b_n) are said to "coincide", written x ~ y iff |a_n/b_n - c_m/d_m| < 2/n + 2/m, where I might have gotten the right-hand side slightly wrong. Now there are two possibilities: (1) we say that a real is an equivalence class of fundamental sequences under the relation ~, or (2) we say that a real _is_ a fundamental sequence, where two reals are claimed "equal" if they coincide (the approach taken by Bishop). The first alternative gives us what is usually called "Cauchy reals". The difference between the two is apparent when we attempt to show that every Cauchy sequence of reals has a limit. In the first case we are given a sequence of equivalence classes of fundamental sequences. In order to construct a fundamental sequence representing the limit we need to _choose_ a representative from each equivalence class. In the second case a Cauchy sequence of reals is a sequence of fundamental sequences, so no choice is required. There seems to be an open question in regard to this, advertised by Alex Simpson and Martin Escardo: find a topos in which Cauchy reals are not Cauchy complete (i.e., not every Cauchy sequence of reals has a limit). For extra credit, make it so that the Cauchy completion of Cauchy reals is strictly smaller than the Dedekind reals. Has this been advertised on this list already? Or was it the FOM list? [If anyone replies to this, I suggest you start a new discussion thread.] Andrej Bauer