From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/2160 Path: news.gmane.org!not-for-mail From: Dusko Pavlovic Newsgroups: gmane.science.mathematics.categories Subject: Re: Cauchy completeness of Cauchy reals Date: Tue, 04 Feb 2003 01:15:11 -0800 Message-ID: <3E3F849F.5080704@kestrel.edu> References: <3E36ED4F.4070807@kestrel> <1043829334.3e37925619e77@mail.inf.ed.ac.uk> NNTP-Posting-Host: main.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241018456 2781 80.91.229.2 (29 Apr 2009 15:20:56 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:20:56 +0000 (UTC) To: CATEGORIES mailing list Original-X-From: rrosebru@mta.ca Wed Feb 5 11:37:52 2003 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Wed, 05 Feb 2003 11:37:52 -0400 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.10) id 18gRc5-0003EK-00 for categories-list@mta.ca; Wed, 05 Feb 2003 11:37:25 -0400 X-Accept-Language: en-us, en Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 15 Original-Lines: 91 Xref: news.gmane.org gmane.science.mathematics.categories:2160 Archived-At: (not sure whether i shouldn't let this thread die, since i didn't read mail for a week, and we all have things to do. but it's not like this list is filling anyone's mailbox with megabytes of usolicited research problems, and it seems a couple more dekabytes on cauchy reals might be useful.) Alex Simpson wrote: >> |cb(x)i - cb(y)i| <= [... calculation omitted ...] >> <= 1/2^i >> >>means that cb(x)i and cb(y)i have the first i digits equal. >> >I don't see that cb(x)i and cb(y)i have the first i digits equal. > i stand corrected (as they say). >>now, as everyone has been pointing out, the dyadic representation >>depends on markov's principle. >> > >This is *not* what has been pointed out (whatever you mean >by dyadic representation). > >What I previously pointed out was that the existence of >ordinary binary representations may fail even in the presence >of Markov's principle. > dyadic numbers are rationals in the form p/2^n. (google helps with such things.) the intuition that dyadic approximation has to do with markov's principle is supported by the fact that markov's principle is equivalent with the statement >>that 1/2 + 1/4 +...+ 1/2^k > 1-e. in other words, that there is k >>s.t. 1/2^k < e. this is *equivalent* to markov's principle. >> > >The property quoted is in fact a trivial consequence of intuitionistic >arithmetic alone. It has nothing to do with Markov's principle. > for a real number e, i am pretty sure that the above is equivalent with markov's principle. it must be in books, but i think you can't miss the proof if you try. *however* you are right that in my "construction", it is used in a wrong place, for a rational number, and k exists trivially. >Such an f is tantamount to giving a splitting to the epi > > r: {x: Q^N | x a Cauchy sequence} --> I_C > >where I_C is the Cauchy interval. There are many toposes >in which Q^N is basically Baire space and I_C is basically >the closed unit interval in Euclidean space >Furthermore, >in many such toposes (e.g. Johnstone's), countable >choice and Markov's principle both hold. > splitting r is only the strongest sense of finding the canonical representatives, not the only one. r may not split by a topos morphism, but the canonical representatives can be found externally, and suffice for a completeness proof. after all, if i remember correctly, such is the situation with markov's principle itself: for a decidable P, * heyting arithmetic does not validate |- ~forall x. P(x) -> exists x.~ P(x) * but if |-~foral x. P(x) can be derived, then |- exists x.~P(x) can be derived. in particular, if i can prove that not all numbers in a binary stream are 0, then i can extract the first 1 from that proof, although that proof transformation cannot be internalized as a recursive function, to realize the implication. all this is, of course, just more intuitive support for the idea that i have been trying out, that *dyadic approximations might yield representatives of cauchy sequences, and since they are a coalgebra, help with their completeness*. i know that it is probably a wrong idea, but it also feels wrong to me to settle with incomplete cauchy reals. i'd like to understand why in the world would toposes deviate from cantor's idea of continuum, so pervasive in everyday math? -- dusko