[FOM] Intermediate value theorem (and ASD)]]

[Andrej Bauer]

Dear Arnon,

as much as I would like to finish the current discussions about
constructive mathematics, I feel obliged to answer to you.

> Now the set of points of the
> Euclidean Plane is absolutely (and constructively!)
> uncountable. No ifs, no buts
> (and I would be very surprised indeed if some
> constructivist succeeds to refute this absolute fact using
> a constructive argument...).

Constructive mathematicians would be as surprised as you.

I think I pointed this out earlier, but I have to repeat: constructive
mathematics is _more general_ than classical mathematics in the sense
that ZFC is a model of constructive mathematics. Therefore, if you
prove the Euclidean Plane to be uncountable in ZFC, constructive
mathematics cannot prove the opposite.

You seem to think that constructive mathematics is somehow at odds
with classical mathematics. Where does that opinion come from? One
possible confusion might be that you refer to the Russian
Constructivism as "constructive mathematics", whereas most
practitioners of constructive mathematics today use the term to refer
to Bishop's constructive mathematics.

Russian constructivism is at odds with classical mathematics, but
Bishop's constructive mathematics is not.

> Hence no construction of "R" or
> "2^X" that does not have this property can possibly count
> as a candidate for a collection  of objects which is
> isomorphic to the set of points in an Euclidean Plane.

Every construction of the reals known to me, wheather it be classical
or constructive, has this property, namely that the reals are
uncountable. You speak as if somewhere you saw a constructive
statement that 2^N or R is countable. If you did, I would like to see
a reference. If you did not, what is the source of your (implicit)
expectation that constructive mathematicians might think something as
unreasonable as "R is countable"?

I do not particularly care if your personal view of constructive
mathematics is different from mine. But I do feel obliged to point out
the mistaken opinions that seem to serve as a basis for your views (as
politely as I can) when you make public statements that spread false
expectations and unfounded critique of constructive mathematics.

With kind regards,

Andrej