FOM: Intuitionistic reals

[Fred Richman]

Alex Simpson wrote:
 
> does anybody know a model for some reasonable intuitionistic
> set theory (e.g. a topos) in which the Cauchy reals are *not* Cauchy
> complete in this sense?

I don't know the answer to this. I just wanted to say that I have also
wondered about this question. It seems to me that "this sense" is the
correct sense, namely that any Cauchy sequence of real numbers
converges (as opposed to some statement about doubly indexed sequences
of rational numbers).
 
> Thus one can also define the "Cauchy-completed
> reals" R_cc as the intersection of all Cauchy-complete subsets of
> R_d containing the rationals Q.

> Question 2 is: has anyone seen the Cauchy-completed reals
> (or something equivalent to them) defined before? Any references would
> be very welcome.

I haven't, but that doesn't mean much. It seems like an interesting
idea. You could do the same thing for any metric space: There are a
couple of equivalent ways to define the completion of a metric space,
without assuming number-number choice, so that, in particular, the
completion is Cauchy complete.

While we are on the subject of models, I have a question also. A
function f : R -> R is said to be "strongly extensional" if a is apart
from b whenever f(a) is apart from f(b). Every pointwise continuous
function is strongly extensional, and Markov's principle implies that
every function is strongly extensional (for Cauchy reals). Are there
models (preferably with number-number choice, so all reals are Cauchy
reals) where there are functions that are not strongly extensional?

--Fred