[FOM] R and the powerset axiom

[Arnon Avron]

Dear Andrej,

> the questions you asked is interesting, but let me just say that I was
> genuinely interested in understanding whether you claim that real
> numbers "depend" on the powersets, and that this has little to do with
> constructivism. The examples I cited were constructions of reals in
> systems without the powerset axiom that were supposed to show
> different ways of getting at the reals. Yes, most of them are
> constructively acceptable, but that is beside the point because
> classical set theory is also a model for most of the examples cited.
> So you could pick one of the constructions and interpret it as a
> classical mathematician. It would give you the classical real numbers,
> without the use of the powerset axiom. And that's what my question is
> about: why do you say that the reals are so tightly connected with the
> powersets, when there are (classical) constructions of reals that
> don't use powersets?

I admit that I am not acquainted with the constructions you have cited
(I thought they are all in the context of constructive mathematics).
However, I do not understand how a construction of the real "reals"
(*those that are supposed to correspond in exact way to the points
on an Euclidean straight line*) can be done without the powerset axiom
or something equivalent. As far as I know, without the
powerset axiom one cannot prove in ZFC the existence of any
uncountable set (including the real R).

Arnon Avron