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

[Andrej Bauer]

Dear Arnon,

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?

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

The kind of reductionism that is present in today's foundations of
mathematics is dangerous. All mathematical objects and ideas tend to
be expressed in classical set theory. I believe this kills many useful
mathematical intuitions, in particular those related to geometry and
computation. We're like logicians after Aristotle who were unable to
imagine anything beyond his logic. We're unable to imagine anything
beyond classical set theory. (Well, there are people who can, but they
a tiny minority.)

In view of this I would definitely say that in most contexts it is a
mistake to identify Euclid's plane with R^2 because doing so ignores
the purpose and the sense of Euclid's geometry. It is most definitely
a methodological mistake to teach planar geometry _only_ in terms of
analytic coordinates, I hope everyone agrees with that. It is a
mistake to emphasize a single point of view (e.g. "plane = R^2")
because eventually people will not be able to imagine an alternative,
and their intuitions will be deprived of a wealth of examples and
possibilities. But Decartes' and Hilbert's identification of the
Euclidean plane with R^2 was _not_ a mistake. It was a big discovery.

> And do constructivists have any theory/grasp of
> the *geometrical* plane which is independent of their
> theory (theories?) of the real numbers?

Yes. I believe Michael Beeson did some work on this topic:

Constructive geometry, to appear in Arai, T. (ed.) Proceedings of the
Tenth Asian Logic Colloquium, Kobe, Japan, 2008, World Scientific,
Singapore, 2009. Available at:
http://www.michaelbeeson.com/research/papers/ConstructiveGeometry.pdf

I don't want to talk about constructive mathematics today so I won't
comment on the intermediate value theorem. Let's stick to real numbers
with(out) powersets.

With kind regards,

Andrej