Least inner model of ZF without power set axiom I'm interested in the existence and properties of an analogue version of $L$ for models of ZF$^-$ (ZF without the power set axiom), which for simplicity I'll call $L^-$. By "analogue" I mean the least inner model of a set theory universe $V$ (same ordinals and transitive).


*

*Assuming $V$ is a model of ZF$^-$, does a least inner model exist, and is it unique? Intuitively I'd answer that as "yes", though I don't know how to prove it.

*Assuming "yes" for question 1, and assuming $V$ is a model of ZF (note here that $V$ does satisfy the power set axiom), is $L^- = L$ (obviously $L$ itself is a model of ZF$^-$, so $L^- \subseteq L$)?


Assuming existence and uniqueness, I strongly suspect equality, though it isn't obvious to me. If we look at the power set axiom as a large cardinal axiom (postulating the existence of some large cardinal with a certain property), then this just means that $L$ "inherits" these "large cardinals" from the universe. On the other hand, if $L^-$ is actually a proper subclass of $L$, then a host of new questions about this $L^-$ spring to mind.


*In a universe where $V$ is a model of ZF$^-$ only, does $L^-$ satisfy AC? This question seems to be a little bit trickier than for $L$, because of our non-constructive definition of $L^-$.

 A: Your intuition is correct, for we have $L^-=L$.
Inside any model $V$ of $\text{ZF}^-$, we can still build $L$. You don't need the power set axiom to construct $L$. And furthermore, the resulting inner model $L$ will satisfy $\text{ZF}^-$. 
From this, it follows that $L^-=L$, since if $W$ is a transitive model of
$\text{ZF}^-$ containing all the ordinals, then $W$ will construct the same $L$ as we did in $V$, and so $L\subset W$, verifying leastness as desired.
A: I believe the answer to all your questions are in:
Gostanian, "Constructible Models of Subsystems of $\mathsf{ZF}$", J. Symbolic Logic 45 (1980), 237–250 (MR0569395)
which is precisely about this sort of models.
If $T$ is a "reasonable" theory extending $\mathsf{KP}$ then you can construct $L$ inside a transitive model $M$ of $T$ and you get (the usual) $L_\alpha$, where $\alpha$ is the least ordinal not in $M$, which is also a model of $T$ (this is what Gostanian proves for various $T$, including $\mathsf{ZF}^-$), which is consequently the least inner model of $T$ in $M$.  Since $\alpha$ is admissible, $L_\alpha$ satisfies $\mathsf{AC}$.
