[FOM] What do you lose if you ditch Powerset?

[Arnon Avron]

Harvey Friedman wrote:

> Let ZFC\P be the result of dropping the power set axiom from ZFC.
> 
> All presently known "natural" mathematical examples of sentences provable in
> ZFC but not in ZFC\P fall into two groups.
> 
> 1. Examples over several decades involving Borel measurable functions on
> Polish spaces (complete separable metric spaces).
> 
> 2. Examples from Boolean relation theory that don't quite exist yet, because
> my priority has always been on independence from ZFC.
> 
> 3. Under a moderately strict notion of "classical" mathematics, there are no
> known examples. 
> 
> Since 2 does not yet exist, we concentrate on 1.
> 
> Borel measurable functions, even on R, *superficially* use the power set for
> their formulation, since R cannot be proved to exist *as a set* in ZFC\P.
> However, there is absolutely no need to have R as a set in order to discuss
> Borel measurable functions on R. In fact, the whole theory of Borel
> measurable functions on Polish spaces has a completely natural development
> without using R as a set. One uses, instead, "being a real number", and uses
> countable well founded trees in order to present Borel measurable functions
> in a totally natural way.
> 

I guess that these (VERY interesting!) results require a LOT of 
encoding techniques, and perhaps some efforts to see the equivalence 
(where?) of this development of the theory with the standard one. 
I admit that like Chow, I dont know well the literature on the subject.
So I like first of all to ask some concrete questions:

1) Is the existence of the Cartesian product AxB provable in the *usual* 
   formulation of ZFC\P? (I ask about the usual one, since in the
   standard textbooks the existence of AxB is derived from its
   being a subset of P(P(A\cup B)). On the other hand  in my contribution
   to the forthcoming book "Thirty Five Years of Automating Mathematics"
   (ed. by Fairouz Kamareddine, Kluwer Academic Publishers) I present
   an alternative formulation, based on purely syntactical considerations,
   in which the existence of AxB does not depend on the Powerset axiom,
   although the definition of an order pair (and all other concepts) are
   the usual ones).
   
2) Can the notions of a function in general, and of piecewise 
   continuous function on $R$ in particular,
   be defined in the *usual* way (or something *clearly* equivalent)
   in ZFC\P? If so, can you give me a hint how? If not - what is the 
   substitute? And how, for example, are the standard theorems about 
   the properties of continuous functions on a closed interval formulated
   without the Powerset axiom at the background?


In order to clarify things: I suspect that the answers to these
questions can be found in Simpson's book. If this is what you have
in mind then I even know a part of them. What *I* am asking is to what
extent do we need the Powerset axiom for Classical mathematics
*as it is usually presented in textbooks*. It seems to me that you
provided an answer to something somewhat different: to what extent
can we produce appropriate substitutes in ZFC\P to the concepts
and theorems of classical Mathematics (this might indeed be
what Chow was asking - this I leave to him to decide).
  
Arnon Avron


School of Computer Science, Tel-Aviv University
email: aa at math.tau.ac.il
http://www.math.tau.ac.il/~aa/