Re: Generalization of Browder's F.P. Theorem?

[Andrej Bauer <Andrej.Bauer@andrej.com>]

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