[FOM] When is it appropriate to treat isomorphism as identity?

[Andrej Bauer]

Dear Arnon,

> The concept of a "real number" was historically
> problematic, and in my opinion it still is, since it
> depends on the very questionable powerset axiom.

But aren't there constructions of real numbers that do not require the
powerset axiom? For example:
- reals in constructive set theory, see section 3.6 of
http://www.ml.kva.se/preprints/meta/AczelMon_Sep_24_09_16_56.rdf.html
,
- reals in type theory with inductive definitions,
http://www.cs.chalmers.se/~coquand/silvio.ps
- reals in Abstract Stone Duality, http://www.paultaylor.eu/ASD/dedras/
- reals by a universal property,
http://www.dcs.ed.ac.uk/home/als/Research/interval.ps
- reals may be constructed in any "Pi-pretopos with natural numbers",
http://ncatlab.org/nlab/show/pretopos , as completion of rationals by
Cauchy sequences

In a particular setting such as ZF it might be the case that one needs
the powerset axiom to show that the reals exist, but this may a
deficiency of the particular setting, not the real numbers. Do you
feel that the reals themselves (not necessarily within ZF) are
problematic?

With kind regards,

Andrej