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

[Arnon Avron]

On Sat, May 16, 2009 at 03:07:33PM -0000, Paul Taylor wrote:

> ASD, a calculus that DOES NOT USE THE POWERSET, or any sets

So it uses something else, which is no less problematic
(like A->B or A^B or whatever). Nobody can do 
what cannot be done.

>  I suggest that the debate
> over the intermediate value theorem is rather 
> sterile unless it is
> conducted in the setting of actually wanting to 
> CALCULATE a number  (or Euclidean point)  

Talking about CALCULATING a Euclidean point makes sense
only if you identify R^2 with the Euclidean plane. But
this was exactly what I was questioning! 

  We all have clear intuitions and understanding of the
objects (points, curves, etc) of the Euclidean plane.
We do NOT have such understanding of R or R^2. 
In fact mathematicians 
have always struggled with the notion of a real number, and 
they still do. Your work is an excellent example of this:
how else can you explain the fact that at the 21th century
you (or Andrej) still publish papers in which  (at last) 
what you believe to be adequate constructions of the reals
are provided?

 By the way, Euclid was constructive *without 
doing calculations*. He proved existence of points
by CONSTRUCTING them (using abstract instruments),
not by calculating approximations of them. However,
this is a side (though interesting) point. When I 
talk about the Euclidean plane I do not have in mind
only the theory developed by Euclid (which concentrates
on objects that can be constructed using a ruler and a compass),
but the whole framework of intuitions
and understanding that stands behind it.

 
> Eve did in the Garden of Eden where geometric intuition prevailed.
> Maybe all of their functions were differentiable, and/or they used
> Newton's algorithm to solve equations.

There is no sufficient evidence about Adam and Eve,
but Euclid definitely did not identify curves
with functions. You seem to forget the correct
order of things. Curves are intuitive
and come first. Differentiable
functions are only (rather problematic) approximations. 

 
Arnon Avron