Which set theories without the power set axiom are used occasionally?

To get a set theory without the power set axiom, I could just take an existing set theory like ZF or ZFC, and remove the power set axiom. However, perhaps I would have to be careful how to formulate the other axioms then, or have to add some sentences that were provable before in the presence of the power set axiom as additional axioms.

So if I need a set theory without the power set axiom, it seems wiser to use a theory already investigated in sufficient detail by somebody else. Of course, the theory should be sufficiently "well behaved" so that it is still used at least occasionally. (If ZF or ZFC without the power set axiom should turn out to be such theories, then of course they also qualify as an answer.)

Take a look at "What is the theory ZFC without power set?" by Victoria Gitman, Joel David Hamkins, Thomas A. Johnstone, freely available at arxiv: http://arxiv.org/abs/1110.2430

This would seem to give you an excellent (and recent!) starting point for thinking about your question. One thing the paper makes clear is that the issue of what you can prove in a theory without the power set axiom depends on your choice of the remaining axioms (equivalent systems of axioms for set theory, both including the powerset axiom, can become inequivalent when you remove the power set axiom).

• In particular, from the abstract: "these deficits of [ZFC without powerset] are completely repaired by strengthening it to the theory $ZFC^-$, obtained by using collection rather than replacement" Jun 2 '13 at 11:44

Peter's answer probably addresses your question more directly, but I thought I might mention that Kripke–Platek set theory is a widely studied set theory that omits the power set axiom. It is weaker than the theory $\mathsf{ZFC}^-$ of the Gitman–Hamkins–Johnstone paper, but has what you might consider the advantage that it has been around for a longer time.

The SEP article on Alternative Axiomatic Set Theories mentions at least two (classical first-order logic based) set theories without the power set axiom: Kripke–Platek set theory with urelements and Pocket set theory.

As a common theme from what I learned so far, it seems wise to avoid the axiom schema of replacement and instead use the axiom schema of collection or the Axiom of limitation of size. Limitation of size seems to be quite a bit stronger than replacement, even so it often serves as motivation for the axiom of replacement. I also noticed that the axiom of choice seems best formulated as the well-ordering principle. Another theme seems to be the reformulation of the axiom of regularity (foundation) as an $\in$-induction scheme.

One theory which hasn't been touched is $\mathsf{ZF^-}$, but probably just removing the well-ordering principle from $\mathsf{ZFC^-}$ will do the trick without further nasty surprises.