Re: Generalization of Browder's F.P. Theorem?
Michael Barr <barr@barrs.org> 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
Andrej Bauer writes:
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.
One small clarification: Regarding the extra credit, there doesn't seem to be a reasonable "absolute" way of defining the completion in question. E.g. the various, constructively different, notions of metric completion already assume the existence of some given complete reals. However, one can always embed the Cauchy reals into the Dedekind reals, which are always Cauchy complete, and then look at the smallest "subset" containing this which is closed under limits of Cauchy sequences (where Cauchy sequences are defined as in Andrej's message). We sometimes call this, somewhat verbosely, "the Cauchy completion of the Cauchy reals within the Dedekind reals". But notice that this is the same as what one gets starting from the rationals within the Dedekind reals and then closing under limits and hence could be called the "Cauchy completion of the rationals within the Dedekind reals". NB. Freyd characterized the Dedekind reals as a final coalgebra. Alex Simpson and I characterized "the Cauchy completion of the rationals within the Dedekind reals" as a free algebra (to be precise, we started from the algebras as a primitive notion and later found this construction of the free one). But this has already been discussed in postings in the past few years. Martin Escardo
Martin Escardo wrote:
NB. Freyd characterized the Dedekind reals as a final coalgebra. Alex Simpson and I characterized "the Cauchy completion of the rationals within the Dedekind reals" as a free algebra
and vaughan pratt and i characterized the cauchy reals as a final coalgebra. the papers are i proceedings of CMCS 99 and in TCS 280. in fact, freyd came up with his characterization of the closed interval while commenting on our first paper, where vaughan and i worked with the semiopen interval. but it is fair to say that the algebraic approach allows easier algebraic operations on reals. (i only managed to multiply them in one of our coalgebras, and in a very inefficient way.) -- dusko BTW have you seen the book: Life Itself. A Comprehensive Inquiry Into the Nature, Origin, and Fabrication of Life by Robert Rosen (Columbia University Press 1991) it was referenced in a biology paper, i found it in the biology library, and it's full of categories. (yes, i kno, people often do that to sound complicated, but this seems like honest work, perhaps even inspiring, although it does not go very deep.)
Dusko --
BTW have you seen the book:
Life Itself. A Comprehensive Inquiry Into the Nature, Origin, and Fabrication of Life by Robert Rosen (Columbia University Press 1991)
it was referenced in a biology paper, i found it in the biology library, and it's full of categories. (yes, i kno, people often do that to sound complicated, but this seems like honest work, perhaps even inspiring, although it does not go very deep.)
An earlier book of Rosen's applying category theory to biology (or rather, speaking more carefully, exploring how one might conceive of applying category theory to biological domains) was: "Anticipatory Systems: Philosophical, Mathematical and Methodological Foundations" (Pergamon Press, Oxford, UK 1985) You may also be interested in this work by Andree Ehresmann and Jean-Paul Venbremeersch on a category-theoretic account of evolving systems, such as those found in biological domains: http://perso.wanadoo.fr/vbm-ehr/ Peter McBurney Department of Computer Science University of Liverpool
Dusko Pavlovic writes:
NB. Freyd characterized the Dedekind reals as a final coalgebra. Alex Simpson and I characterized "the Cauchy completion of the rationals within the Dedekind reals" as a free algebra
and vaughan pratt and i characterized the cauchy reals as a final coalgebra. the papers are i proceedings of CMCS 99 and in TCS 280.
I forgot to mention this --- I apologize. In your paper, you work in Set. Do you think your construction works in any topos? If so, what would "Cauchy reals" mean precisely in this general context? Thanks. ME
Andrej Bauer wrote:
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.
this will give me negative credits one way or another, but here it goes: let a = (a_i) be a cauchy sequence of rationals between 0 and 1. (cauchy means |a_m - a_n| < 1/m + 1/n, as in andrej's message.) let b = (b_i) be the subsequence b_i = a_{2^i+3}. b and a are equivalent in the sense from the message, because |a_m - b_n| < 1/m + 1/(2^n+3) < 2/m + 2/n note that |b_i - b_{i+k}| < 1/(2^i+3) + 1/(2^(i+k)+3) < 1/(2^i+2) now define x_i to be the simplest dyadic that falls in the interval between b_i - 1/2^(i+2) and b_i + 1/2^(i+2). in other words, to get x_i, begin adding 1/2 + 1/4 + 1/8... until you overshoot b_i - 1/2^(1+2). if you also overshoot b_i + 1/2^(1+2), and the last summand was 1/2^k, skip it, and try adding 1/2^(k+1), etc. one of them must fall in between. a less childish way to say this is that x_i is the shortest irredundant binary (no infinite sequences of 1) such that |b_i - x_i| < 1/2^(i+2) so x = (x_i) is a cauchy sequence equivalent to b, with |x_i - x_{i+k}| <= |x_i-b_i| + | b_i - b_{i+k}| + |b_{i+k} - x_{i+k}| < < 1/2^(i+2) + 1/2^(i+2) + 1/2^(i+k+2) < < 1/2^i this means that the first i digits of x_i and x_{i+k} coincide. now let X be the binary number such that its first i digits are the same as in x_i, for every i. (if it ends on an infinte sequence of 1s, replace it by the corresponding irredundant representative.) this is clearly a constant cauchy sequence equivalent to x, so it is its limit. since x is equivalent to b |b_m - x_n| <= |b_m - b_n| + |b_n - x_n| < 1/2^(m+3) + 1/2^(n+3) + 1/2^(n+2) < 2/m + 2/n and b is equivalent to a, X is also the limit of a. is there an error in the above reasoning? i can't find it. on the other hand, i printed out the paper by alex and martin, and the conjecture is stated rather strongly, so i guess i must be missing something. -- dusko
heh, i typed this late, and managed to confuse the basic assumption. instead of
let a = (a_i) be a cauchy sequence of rationals between 0 and 1.
let a = (a_i) be a cauchy sequence of *cauchy reals*, i.e. each a_i is a cauchy sequence of rationals between 0 and 1. i think the rest goes unchanged: you take a fast converging subsequence b of a, and then approximate b by irredundant rational prefixes. the irredundant representation is thus used instead of choice. the completeness of such representation is the finality of its coalgebraic structure. -- dusko
Set. Do you think your construction works in any topos?
the coalgebraic structures are defined using just arithmetic. in the first one, there is the "no infinite sequences of 1s" condition, which i am reminded depends on markov's principle; but that is just used in the explanation. i don't think there are other constraints.
If so, what would "Cauchy reals" mean precisely in this general context?
it means fundamental sequence, with the equivalence relation in the "lazy" mode, a la bishop, as described in andrej bauer's message. if my last night's posting makes sense, then these constructivist cauchy reals make a whole lot of difference, because they really let you avoid the choice and get limits. -- dusko
On Fri, 24 Jan 2003, Dusko Pavlovic wrote:
Set. Do you think your construction works in any topos?
the coalgebraic structures are defined using just arithmetic. in the first one, there is the "no infinite sequences of 1s" condition, which i am reminded depends on markov's principle; but that is just used in the explanation. i don't think there are other constraints.
If so, what would "Cauchy reals" mean precisely in this general context?
it means fundamental sequence, with the equivalence relation in the "lazy" mode, a la bishop, as described in andrej bauer's message.
I'm sorry, but this won't do. In a topos, equality is equality; you can't treat it "lazily". So a Cauchy real has to be an equivalence class of Cauchy sequences, and there is in general no way of choosing a canonical representative for it. Markov's principle would, I think (I haven't checked the details), suffice to give a canonical representation as a binary expansion with no infinite sequence of 1's, and then Dusko's argument would suffice to show that the Cauchy reals are Cauchy complete. But there are many toposes where Markov's principle fails. I doubt very much whether the Cauchy reals occur as a final coalgebra for anything, in any topos where they fail to coincide with the Dedekind reals, simply because the Dedekind reals are likely to be a coalgebra for the same endofunctor (and they're more "final" than the Cauchy reals). Incidentally, Peter Freyd and I worked out how to do his coalgebra construction constructively, and I showed that its final coalgebra is the Dedekind interval in any topos -- the proof is in the Elephant, at the end of section D4.7. Peter Johnstone
Peter Johnstone writes:
I'm sorry, but this won't do. In a topos, equality is equality; you can't treat it "lazily". So a Cauchy real has to be an equivalence class of Cauchy sequences, and there is in general no way of choosing a canonical representative for it. Markov's principle would, I think (I haven't checked the details), suffice to give a canonical representation as a binary expansion with no infinite sequence of 1's,
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. Alex Simpson Alex Simpson, LFCS, Division of Informatics, Univ. of Edinburgh Email: Alex.Simpson@ed.ac.uk Tel: +44 (0)131 650 5113 Web: http://www.dcs.ed.ac.uk/home/als Fax: +44 (0)131 667 7209
With all this talk about real numbers, perhaps readers would be interested in my little paper (reporting an idea of Steve Schanuel): An efficient construction of the real numbers, Gazette Australian Math. Soc. 12 (1985) 57-58. which may be hard to find. However, a recent report of an undergraduate vacation project can be obtained at http://www.maths.mq.edu.au/~street/efficient.pdf This project convinced me that this construction is a good one for teaching undergraduates. Others have had this idea too. In particular, the following was recently posted on the math arXiv: Norbert A'Campo, A natural construction of the real numbers, arXiv:math.GN/0301015 v1 3 Jan 2003. With regards, Ross
participants (7)
-
Alex Simpson -
Andrej Bauer -
Dusko Pavlovic -
Martin Escardo -
Peter McBurney -
Prof. Peter Johnstone -
Ross Street