Alex Simpson <als@inf.ed.ac.uk> writes:
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.
This is clearly wrong. Every epi is regular, in a topos.
My original statement was correct. In the effective topos, the map from binary representations to Cauchy (= Dedekind) reals is not epi.
I stand corrected. I am confusing the effective topos with assemblies (or modest sets) over the first Kleene algebra. Andrej
[this is a copy of my post of monday morning, which bounced between bob and me a couple of times, courtesy of our mailers. -- dusko] thanks for the replies. sorry to clog people's mailboxes, but i'll permit myself one more post on cauchy. (i think this does deserve some general interest because we often say that categories capture real mathematical practices --- but as it happens, cauchy reals are not complete, and the mean value theorem fails, and so on. i was hoping to understand where does the usual intuition of continuum fail, and what categorical property do we need to do basic calculus. i came to think that coalgebras help with this, since they capture the various notions of completeness, and wondered why they don't capture the standard cauchy completeness argument in this context. hence my post that invoked the reactions.) On Sat, 25 Jan 2003 Prof. Peter Johnstone wrote:
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.
one would hope that equality in a topos is widely understood, even by me. treating fundamental sequences up to an equivalence relation in a lazy mode just means not taking their quotient, but carrying the explicit equivalence relation. such structures are commonly considered in toposes. on the other hand, many constructivists (martin-lof, bishop) say that this is the way to do constructivist mathematics. (although i am not sure whether i came to think of cauchy reals in this way because constructivist education left some trace, or because undergraduate analysis didn't.) sorry i didn't make all this clear. martin escardo's remark to which i responded was rather cursory, he just attributed two things, so i kept mine short. moreover, toposes were not mentioned, and as far as i remember, the validity in toposes was not discussed either by freyd, or by vaughan and me. we all talked about streams of digits and it seemed to me that we were talking about cauchy reals (the constructivist ones), until peter johnstone observed that freyd = dedekind++. On Sat, 25 Jan 2003 Alex Simpson wrote:
The question is: does every Cauchy sequence (x_i) in R_C have a limit in R_C
Here we are not starting off with a Cauchy sequence of rationals; not even a Cauchy sequence of Cauchy sequences.
i realized that i typed "let a = (a_i) be a sequence of rationals" instead of "a sequence of cauchy reals" as soon as i woke up, the morning after i typed it, and sent a correction a couple of hours after the post --- but our watchful moderator for some reason didn't forward it to the list. in any case, i said i thought that the construction went through for cauchy sequences of constructivist cauchy reals, as described in andrej bauer's message:
(2) we say that a real _is_ a fundamental sequence, where two reals are claimed "equal" if they coincide (the approach taken by Bishop).
now it turns out that such cauchy reals don't count, that cauchy reals must be
(1) we say that a real is an equivalence class of fundamental sequences under the relation ~,
well, call me irresponsible, but i think that the same idea still applies: the irredundant coalgebraic reals give canonical representatives for equivalence classes too. with them, one can prove completeness as usually. here is a slight modification of sequences from my previous post. let Q be the set of rationals between 0 and 1, D <= Q dyadic rationals and N natural numbers. a cauchy real A is now a subobject of Q^N such that exists x in A forall x in A holds: |xm - xn| < 1/m+1/n forall x in A and all y in Q^N holds: |xm - yn| < 2/m+2/n iff y in A. consider maps b: Q^N --> Q^N, c: Q^N --> D^N and d : D^N --> Q^N, defined b(x)i = x(2^(i+3)) c(x)i = p/2^n, such that |xi - p/2^n| < 1/2^(i+2) and |xi - q/2^m| < 1/2^(i+2) implies m>=n of q>=p d(x)i = x truncated after i'th digit ** i claim that the image dcb(A) of A along is a representative of A, ie ** ** 1. it is a singleton, and ** 2. an element of A. this means that the function dcb : Q^N-->Q^N induces a choice function from Q^N/~ to Q^N, assigning to each cauchy real a cauchy sequence of ratioanls representing it. the proofs proceed like for the corresponding sequences in my previous post. in particular, for every x,y : A holds |cb(x)i - cb(y)i| <= |cb(x)i - b(x)i| + |b(x)i-b(y)i| + |b(y)i-cb(y)i| < < 1/2^(i+2) + 2/2^(i+3)+2/2^(i+3) + 1/2^(i+2) = = 1/2^i means that cb(x)i and cb(y)i have the first i digits equal. hence dcb(x)i =dcb(y)i. since this holds for all i, dcb(x) = dcb(y). now, as everyone has been pointing out, the dyadic representation depends on markov's principle. in order to prove that the map c is total, we need the fact that for every e>0 in Q there is some k such 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. how bad is markov's principle? well, i think that markov proposed it as a valid *intuitionistic* principle: ** given an algorithm, if i can prove that it terminates, then i ** should be able to construct its output. it would be nice to know that this is all we need in order to have cauchy complete cauchy reals. also, if this is the case, the challenge topos, where cauchy reals are not complete, would be the realizability topos invalidating markov: the cauchy sequence without a cauchy limit would have to be the one that can be proven different from 0, but cannot be proven apart from 0. is there still an error? please ignore the trivial ones this time, and i'll try to learn from errors. all the best, -- dusko
Dusko Pavlovic wrote in part:
(i think this does deserve some general interest because we often say that categories capture real mathematical practices --- but as it happens, cauchy reals are not complete, and the mean value theorem fails, and so on. i was hoping to understand where does the usual intuition of continuum fail, and what categorical property do we need to do basic calculus.
It depends on what you mean by "basic calculus". Bishop would argue that he can do basic calculus just fine using a constructive version of the mean value theorem. This is not to say that you don't have an interesting question; from the POV of the mathematician on the street (not very theoretical), classical theorems often follow from constructivist (a la Bishop) one if you assume that sequentially compact metric spaces are compact (which means complete and totally bounded to Brouwer and Bishop), so that might be one place to look. -- Toby
Dear Dusko,
is there still an error? please ignore the trivial ones this time, and i'll try to learn from errors.
Yes, I think there's an error.
here is a slight modification of sequences from my previous post. let Q be the set of rationals between 0 and 1, D <= Q dyadic rationals and N natural numbers. a cauchy real A is now a subobject of Q^N such that
[... construction omitted ...]
the proofs proceed like for the corresponding sequences in my previous post. in particular, for every x,y : A holds
|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. hence dcb(x)i =dcb(y)i. since this holds for all i, dcb(x) = dcb(y).
I don't see that cb(x)i and cb(y)i have the first i digits equal. It seems possible to have e.g. cb(x)i = .0111 and cb(y)i = .1000. Indeed, .0111, although it is sufficiently close to b(x)i to be the value of cb(x)i, may nonetheless be too far from b(y)i to qualify as a "simpler" candidate for cb(y)i than .1000. This problem is not easily repaired. In fact, there is a fundamental obstacle to this approach. Your argument attempts to construct a function f: Q^N --> Q^N (in your proof given by f=dcb) satisfying: 1. f maps any Cauchy sequence to a Cauchy sequence representing the same real number. 2. All sequences that represent the same real number get mapped to a single unique Cauchy sequence representative. 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 (e.g. Johnstone's "topological topos", many "Gros toposes"). In such toposes, a splitting of r would correspond to a non-constant continuous function from the Euclidean interval to Baire space. This is clearly impossible, as Baire space is totally disconnected. Furthermore, in many such toposes (e.g. Johnstone's), countable choice and Markov's principle both hold. In conclusion, it is impossible to prove the existence of an f satisfying 1 and 2 above using intuitionistic logic, even if one further assumes countable choice and Markov's principle. Regarding Markov's principle:
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). It is well-known that, in general, very many different versions of Cauchy sequence coincide, including: Cauchy sequences of rationals, indeed many variants depending on properties of the modulus; ditto for sequences of dyadic rationals; nested sequences of closeed proper intervals; "signed" binary representation, etc, etc. What I previously pointed out was that the existence of ordinary binary representations may fail even in the presence of Markov's principle.
in order to prove that the map c is total, we need the fact that for every e>0 in Q there is some k such 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. Indeed your function c is total in any elementary topos.
how bad is markov's principle? well, i think that markov proposed it as a valid *intuitionistic* principle:
** given an algorithm, if i can prove that it terminates, then i ** should be able to construct its output.
This is a curious paraphrasing. It should rather be: "if the algorithm cannot fail to terminate then ..."
it would be nice to know that this is all we need in order to have cauchy complete cauchy reals.
It would be nice and may be true. At present we don't have a single example topos in which the Cauchy reals are not complete (w.r.t. sequences). However, there is, as yet, no convincing reason to link Markov's principle to this question. Best wishes, Alex 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
participants (4)
-
Alex Simpson -
Andrej Bauer -
Dusko Pavlovic -
Toby Bartels