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