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

[Arnon Avron]

On Thu, May 21, 2009 at 10:55:29PM -0700, Vaughan Pratt wrote:
> 
> 
> On 5/20/2009 2:48 PM, Arnon Avron wrote:
> > 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.
> 
> Stone can.

No, he cannot.

Let us clarify the issue I was talking about. I was not talking
about various constructions (no matter how interesting and/or
useful - and they *are* interesting and useful)
which some people call for some reasons
(usually because of some analogy) "R" or "2^X".
I was talking about the specific R^2 that is supposed to be
isomorphic to the set of points in an Euclidean Plane (some
people might these days claim that this is not a well-defined,
or absolute mathematical concept. I'll argue with that
in some other posting). 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...). 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.

Now in ZFC without the powerset axiom one cannot prove
the existence of an uncountable set. Hence one cannot
possibly construct something isomorphic to 
the set of points in an Euclidean Plane without using
principles that are not available in classical ZFC-PS.
(the intuitive P(A), or A^B, or A->B, or whatever).
A mathematical fact is a mathematical fact, and what cannot
be done cannot be done.

> Assuming X is a set, what structure do you impute to 2^X?  

Again: this is not what I am talking about. I am not
imputing any structure to 2^X. I am just claiming that without
assuming something as strong as the "intuitive" 2^N
(or even a little bit weaker) one cannot construct
The "R^2" which is supposed to be isomorphic to 
the Euclidean Plane.

I have the feeling that I am repeating myself. So I'll stop here.

Arnon