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

[Arnon Avron]

Dear  Andrej,

> > 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? 

...

> 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?

Without entering now to a new debate on constructivism, let us
concentrate this time on the context of my previous message,
which was whether it is justified to *identify* the points 
of the Euclidean Plane with ordered pairs of real numbers.
So for the time being I would like to ask informative questions:
Does any of the constructions you mention of R provide an isomorphism
of R^2 with the Euclidean Plane *as was grasped by Euclid*
(and I believe by all other people, living and dead)? 
And do constructivists have any theory/grasp of
the *geometrical* plane which is independent of their
theory (theories?) of the real numbers?

   In his Book "Mathematics: Form and function" Mac-Lane 
says somewhere that one of the main shortcomings of intuitionistic
mathematics is that it ignores geometric intuitions (I am 
relying on my memory here, I do not have a copy of the book).
I fully agree. Thus geometric intuitions dictate that the mean-value
theorem (if f(0)<0 and f(1)>0 then f(a)=0 for some a in [0,1])
should be valid for any adequate notion of a "continuous function"
(i.e. a notion which has pretensions to correspond to
the idea of a function whose graph can be drawn with a pencil
without leaving the paper). As far as I know, this theorem fails
for the constructive theory of the reals (and continuous
functions on them). If so, then the constructive R^2 (whatever
it is) is even less entitled to be identified with the
true Euclidean plane than the R^2 of classical set theory. 

Arnon Avron