Re: Cauchy completeness

Re: Cauchy completeness

[Alex Simpson]

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