Dusko Pavlovic writes:
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.
Yes there is an error; but, more importantly, you are not answering the original question. Regarding the error, your argument is as follows. You start off with a Cauchy sequence a = (a_i) of rationals between 0 and 1. Using this you claim to find a binary expansion X such that X = lim a. Your construction of X is by:
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 not a valid intuitionistic definition, because the property of ending in an infinite sequence of 1s is not (logically) decidable. In fact,the internal statement that every Cauchy real in [0,1] has a binary expansion fails in many toposes (e.g. it fails in the effective topos). As is well known, this can be easily patched by, e.g., allowing 1/2 as an extra digit in binary expansions. Then one does obtain that every Cauchy real (in [0,1]) has such an "extended" binary expansion. However, none of this addresses the original question:
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 this question, one must first construct the Cauchy reals R_C, e.g. as Cauchy sequences quotiented by equivalence, or, equivalently, as extended binary representations quotiented by equivalence. 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. Instead (x_i) is a Cauchy sequence of equivalence classes of Cauchy sequences. To construct a limit, one apparently needs some choice to select representatives from each x_i. Thus it appears that the Cauchy completeness of R_C should fail in general. We would like to have an example of a topos in which it does fail. (Of course if there exists one such example then it also fails in the free topos with nno, but this is no help.) Alex Simpson Alex Simpson, RIMS, Kyoto University, Kyoto, Japan Permanent address: LFCS, Division of Informatics, Univ. of Edinburgh Email: Alex.Simpson@ed.ac.uk Web: http://www.dcs.ed.ac.uk/home/als