Re: Cauchy completeness of Cauchy reals
While I'm comfortable with coalgebraic presentations of the continuum, as well as such algebraic presentations as the field P/I (P being a ring of certain polynomials, I the ideal of P generated by 1-2x) that I mentioned a week or so ago, I'm afraid I'm no judge of constructive approaches to formulating Dedekind cuts. Would a toposopher (or a constructivist of any other stripe) view the following variants as all more or less equally constructive, for example? 1. Define a (closed) interval in the reals as a disjoint pair (L,R) consisting of an order ideal L and an order filter R, both in the rationals standardly ordered, both lacking endpoints. Order intervals by pairwise inclusion: (L,R) <= (L',R') when L is a subset of L' and R is a subset of R'. Define the reals to be the maximal elements in this order. Define an irrational to be a real for which (L,R) partitions Q. 2. Ditto but with the reals defined instead to be intervals for which Q - (L U R) is a finite set. ("Finite set" rather than just "finite" to avoid the other meaning of "finite interval." The order plays no role in this definition, maximality of reals in the order being instead a theorem.) 3. As for 2 but with "finite" replaced by "cardinality at most 1". The predicate "rational" is identified with the cardinality of Q - (L U R). Vaughan
(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
Dusko Pavlovic wrote:
Alex Simpson wrote:
Somebody wrote:
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.
I don't remember the original context, so I don't know who's right, but the answer depends on what sort of real number e could be. It can't be 0, for example, so what can it be? * If e > 0, then work with 1/e and use the Archimedean property; Bishop would recognise and accept this proof. * But if you only know that e <= 0 is false, then you need Markov's principle to deduce e > 0. -- Toby
On Mon, 3 Feb 2003, Vaughan Pratt wrote:
While I'm comfortable with coalgebraic presentations of the continuum, as well as such algebraic presentations as the field P/I (P being a ring of certain polynomials, I the ideal of P generated by 1-2x) that I mentioned a week or so ago, I'm afraid I'm no judge of constructive approaches to formulating Dedekind cuts. Would a toposopher (or a constructivist of any other stripe) view the following variants as all more or less equally constructive, for example?
1. Define a (closed) interval in the reals as a disjoint pair (L,R) consisting of an order ideal L and an order filter R, both in the rationals standardly ordered, both lacking endpoints. Order intervals by pairwise inclusion: (L,R) <= (L',R') when L is a subset of L' and R is a subset of R'. Define the reals to be the maximal elements in this order. Define an irrational to be a real for which (L,R) partitions Q.
2. Ditto but with the reals defined instead to be intervals for which Q - (L U R) is a finite set. ("Finite set" rather than just "finite" to avoid the other meaning of "finite interval." The order plays no role in this definition, maximality of reals in the order being instead a theorem.)
3. As for 2 but with "finite" replaced by "cardinality at most 1". The predicate "rational" is identified with the cardinality of Q - (L U R).
No constructivist (of whatever stripe) would be happy talking about Q - (L U R), as in your second and third definitions, since he wouldn't want to assume that L and R were complemented as subsets of Q. Your first definition, if I understand it correctly, is equivalent to what most toposophers would call the MacNeille reals -- that is, the (Dedekind-MacNeille) order-completion of Q. If you "positivize" the second and third (which would appear to be equivalent, for any sensible notion of finiteness) by saying "Whenever p and q are rationals with p < q, then either p \in L or q \in R", you get the Dedekind reals, which are a proper subset of the MacNeille reals (though they coincide iff De Morgan's law holds) but have rather better algebraic properties. Peter Johnstone
participants (4)
-
Dusko Pavlovic -
Prof. Peter Johnstone -
Toby Bartels -
Vaughan Pratt