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

[Harvey Friedman]

Reply to Avron.

On 11/16/03 11:15 AM, "Arnon Avron" <aa at tau.ac.il> wrote:

> 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) Is the existence of the Cartesian product AxB provable in the *usual*
>  formulation of ZFC\P?

Proofs on the FOM are not allowed, but in this case the proofs are what is
at issue, and they are very simple and easy to understand and NONTECHNICAL,
and one or two lines.

LEMMA. {x} cross B exists.

Proof: For each y in B, {x} cross {y} exists. Then use Replacement to get
the set of all <x,y> such that y in B (x fixed).

THEOREM. A cross B exists.

Proof: For each x in A, {<x,y>: y in B} exists. Use Replacement to get E =
{{<x,y>: y in B}: x in A}. A cross B = UE.

> 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.

Simpson's book keeps being usefully mentioned here on the FOM.
Unfortunately, it is currently out of print.

Simpson's book has affirmative answers to this over the (what amounts to)
fragment of ZF\P called second order arithmetic (Z2) - which is a system in
the two sorted first order predicate calculus. In fact, affirmative answers
in very weak fragments of even this fragment.

However, this development in Z2 comes at a cost. There is some coding
involved, and the weaker the fragment of Z2, the more careful one has to be
about the coding.

Since you ask about ZFC\P, the standards for doing this should be high -
i.e., the reliance on coding minimized.

1. Pointwise continuous function from R into R. The simplest way is to
identify this with a pointwise continous f:A into R, such that for all x in
R, there is a unique pointwise continuous g:A union {x} into R extending f.
The idea here is that this gives us the effect of the pointwise continuous
total extension. I.e., the "application "function"" from R into R is now
clearly and naturally defined. Also, we need only use countable f.

2. One can appropriately identify Polish spaces (complete separable metric
spaces) as countable metric spaces. Then we can extend 1 to pointwise
continuous functions from Polish spaces to Polish spaces.

3. I assume that by piecewise continuous functions from R into R, you mean
that R is partitioned into a countable set of nonempty intervals, and the
function is pointwise continous on each interval. A trivial modification of
1 gives us the notion of a pointwise continuous function from an interval
into R. So we just say that we have a set of items, comprising pointwise
continuous functions from nonempty intervals into R, where the intervals
form a partition of R.

4. We can extend 3 to Polish spaces via 2 if, e.g., the pieces are Boolean
combinations of open sets. There is no problem proving all of the usual
theorems of real and complex analysis.

5. Moreover, one can also nicely treat Borel subsets of Polish spaces, and
Borel functions between Polish spaces. And then one can prove all of the
usual theorems of DST = descriptive set theory.

>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).
> 

I had addressed the question of

*what "mathematically natural" theorems of ZFC that can be appropriately
stated without power set, can not be proved in ZFC\P?*

Incidentally, the following question has a trivial answer:

*what "mathematically natural" theorems of ZFC, can not be proved in ZFC\P?*

The answer is: the existence of the set of all real numbers, and related
statements.

Harvey Friedman