From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2134 Path: news.gmane.org!not-for-mail From: Andrej Bauer Newsgroups: gmane.science.mathematics.categories Subject: Re: Cauchy completeness of Cauchy reals Date: 27 Jan 2003 18:41:39 +0100 Message-ID: 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 1241018434 2647 80.91.229.2 (29 Apr 2009 15:20:34 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:20:34 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Mon Jan 27 19:41:59 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Mon, 27 Jan 2003 19:41:59 -0400 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18dIpk-0003BF-00 for categories-list@mta.ca; Mon, 27 Jan 2003 19:38:32 -0400 In-Reply-To: Alex Simpson's message of "Mon, 27 Jan 2003 03:57:45 +0000 (GMT)" 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: 59 Original-Lines: 28 Xref: news.gmane.org gmane.science.mathematics.categories:2134 Archived-At: Alex Simpson writes: > In fact not. Markov's principle holds in the effective topos, and > there, unless I'm much mistaken, it is not even true that the map from > binary representations to Cauchy (= Dedekind) reals in [0,1] is epi, > let alone split epi. The map e : 2^N --> [0,1] defined by e x = x_0/2 + x_1/4 + x_2/8 + ... is epi in the effective topos, but it is not regular epi. In terms of logic, this means that forall a : [0,1]. (not not (exists x : 2^n. (e x = a))) is valid in the effective topos, but forall a : [0,1]. (exists x : 2^n. (e x = a)) is not valid. Andrej