[FOM] What do you lose if you ditch Powerset?
aa at tau.ac.il
Sun Nov 16 11:15:10 EST 2003
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).
School of Computer Science, Tel-Aviv University
email: aa at math.tau.ac.il
More information about the FOM