[FOM] Constructivism, Geometry, and Powerset

[Arnon Avron]

I got a lot of reactions from constructivists
following a posting of mine in which
I question the identity between R^2 (which I am not
sure what it is) and the points on the Euclidean plane
(of which in my opinion any humane being has a clear 
grasp since her/his childhood). So I want to clarify: 
that posting was not meant at all as
an attack on constructivism.  In fact, my problem here 
concerns orthodox classical mathematics at least as it 
concerns constructive mathematics.

Concerning constructive mathematics I said  only two things,
and I stand behind them:

A)  The constructivists' R^2 (or rather R^2s in plural, as 
Paul Taylor was happy to confirm) cannot be identified
with the *geometrical* Euclidean plane. Here is
my argument for Andrej Bauer's construction of $R$ 
(what I say is based only on what Andrej himself said
about it. I do not claim to know his construction):

1) The set of points of the Euclidean plane is (classically
   and constructively) uncountable - and one does not
   need the powerset axiom to see that. It suffices to
   accept that this set exists (as a set of atoms), and 
   that it has certain geometric properties I am not 
   going to specify here (Andrej seems to agree with this).

2) In classical ZFC-P (where P is the powerset axiom) one 
   cannot prove the uncountability of any set 
   (this is a theorem).

3) Andrej Bauer claims that he can  *construct* 
   a certain set  "R", without using the powerset axiom 
   (or something similar), and without
   using principles that are in conflict with classical logic.

4) From 2 and 3 it follows that Andrej cannot prove that 
   his R^2 is uncountable.

5) From 1 and 4 it follows that his R^2 and the Euclidean plane
   cannot be identified, because there is some property one can
   prove for one, but cannot prove for the other.

Let me repeat at this point that in my opinion also 
the classical "R^2" cannot be identified with the Euclidean
plane because its construction depends on the problematic
powerset axiom. Still it does seem to me
a better candidate for *this* task than the 
constructivist ones (because it is provably uncountable). 
This does *not* mean that constructive concepts of R are 
not useful for computational mathematics or for 
applied mathematics! 

B) The failure in constructive mathematics of the intermediate
value theorem *In its classical, intuitive form* makes
the classical notion of a continuous function
a better *approximation* of the original intuitive
(or "naive", if one prefers. I do not mind) geometric
concept. Note that this does not imply that the 
constructive versions of the IVT 
are not interesting or useful, or even intuitive from some 
other perspective (I believe that they are).
Note also that in my opinion the classical concept
too fails to capture the original geometric notion!

Arnon Avron