The power set axiom and the specification schema

Some people at the lab know that I occasionally (half-jokingly) question the existence of the real numbers and the (informal) validity of a set of axioms that imply that the reals exist.

Most recently I had pinned this down to the powerset axiom in Zermelo set theory. The powerset axiom is: "For any set z, there is a set whose members are just the subsets of z." [ forall z exists y forall x (x in y iff forall w ( w in x implies w in z )) ].

Let me be clear here: I have no problem with the powerset operator being applied to finite sets. I definitely see that for any finite set z, the powerset of z is easily constructed. The questionable part is: why should I believe that the powerset operator is applicable to infinite sets? Given the set of natural numbers N, if we allow the existance of its powerset, 2^N, then there are elements of 2^N that cannot be described by a finite piece of text. Why should we assume that such sets exist?

I recently picked up Boolos' book, "Logic, Logic, and Logic", again, and started looking there for answers to questions I've been having recently about Linear Logic. The first chapter presents "The Iterative Conception of Set", where Boolos describes a staged model for constructing the sets described by Zermelo's axioms (which include the powerset axiom above).

There are a lot of rules for building up these stages, but most of them are straightforward and believable. I skimmed them over, said "okay", and moved on to the next section, which argues that the axioms of Zermelo Set theory follow from the rules given for building the stages. This includes the Powerset axiom; so I was naturally interested in reading this more carefully.

The derivation of the Powerset axiom hinges on the truth of the "specification axioms" of the staged model. When I saw that, I said, "okay, I missed the details of the specification axioms, lets revisit it. . ." It is actually a schema describing an infinite set of formulas that we take as axioms. It is phrased as follows:

"forall s exists y forall x (x in y iff [X] and exists t (t earlierThan s and x formedAt t)))"
where [X] is a formula of in which no occurrence of "y" is free.

As Boolos puts it, "any such axiom will say that for any stage there is a set of just those sets to which [X] applies that are formed before that stage. Let us call these axioms specification axioms."

To derive the powerset axiom, one starts with the specification axiom:
"forall s exists y forall x (x in y iff (forall w (w in x implies w in z) and exists t (t earlierThan s and x formedAt t)))"
which is the same as the above with [X] := "forall w (w in x implies w in z)". This specification axiom says "for any stage, there is a set of all subsets of z formed at earlier stages." (the argument continues from there, but I don't want to relay the remainder of it at this point.)

z is free in the above specification axioms. So it seems that we're actually going to be employing an infinite number of the specification axioms to argue that the powerset axiom is true, since the powerset axiom is quantified over all z; is this okay? Plus, I'm no longer so sure that it is sensible to put no constraints on [X] other than that no occurrence of "y" be free in [X].

But these are pretty flimsy questions; and that's a good thing for me, because it means that I'm narrowing down my uneasiness about the powerset axiom into more bite-size chunks that I can process.