If you replace the axiom of the powerset, with one guaranteeing the existence of double powersets only … roughly speaking, what changes?
Here's the axiom of power set in ZF**, written out in first order logic with a binary predicate $\in$.
$$ \forall x \exists y \forall z (z \in y \iff \forall w (w \in z \implies w \in x) $$
equivalently, using $\mathcal{P}$ and $=$
$$ \forall x \exists y \left[ x = \mathcal{P}(x) \right]$$
If, instead of this axiom, you took the putative double powerset axiom
$$ \forall x \exists y (y = \mathcal{P}(\mathcal{P}(x)) $$
written out fully it's
$$ \forall x \forall y \forall z . x \in y \iff (\exists v . (\forall u . u \in z \implies u \in v) \land (\forall w . w \in v \implies w \in x) ) $$
from
$$ \forall x \forall y \forall z . (x \in y \iff z \subseteq \circ \subseteq x ) $$
would you still be able to construct all the cardinals in the $\beth$ hierarchy?*
I think it's the case that, if any of the $\beth$ cardinals are inaccessible after swapping out the powerset axiom, it's $\beth_1, \beth_3, \beth_5, \cdots$.
So, concretely, is a set with cardinality $|ℝ|$ ($\beth_1$) guaranteed to be there after the swapping out the powerset axiom?
* I'm just thinking about a set theory as collections of theorems/tautologies in first order logic with $\in$ as the sole non-logical connective/predicate thing. $=$ and $\mathcal{P}$, where they appear, are intended as syntactic sugar only. I think you can write down probes in first-order logic to test for the presence of sets of a particular cardinality. If you can't, I'm not sure what the appropriate way to extend the system is. Targeting such a cardinality is what I mean by "constructing". I'm also not commenting on whether there are non-finite cardinalities outside the $\beth$ hierarchy… I don't know enough to make a comment about them, so I'm explicitly only talking about the $\beth$ hierarchy.
** I don't know what would happen here if we take the axiom of choice. A solution that needs choice would also be interesting.
Best Answer
The answer is that double-powerset gives you back powerset, without using choice: Separation lets you get something "morally equivalent" to the powerset, and Replacement goes the rest of the way.
In more detail, suppose $y$ is the double powerset of $x$ - that is, suppose that the elements of $y$ are precisely the sets of subsets of $x$. Then by Separation, the subclass $$z=\{a\in y: \vert a\vert=1\}$$ is a set. Replacement tells us that the class $$z'=\{a: \{a\}\in z\}$$ is a set (the map $\{a\}\mapsto a$ being definable), but $z'$ is just the powerset of $x$.
EDIT: As Henning Makholm points out below, we can avoid replacement and separation both by simply noting that $$\bigcup P(P(x))=P(x).$$