If we add to the language of set theory a total one place function symbol $\mathcal P$ standing for powerset operator, and then add to ZF-Power the following axioms:


**Power:** if $\phi$ is a formula in which only the symbol $y$ occurs free, then: $$ X \subseteq A \land X=\{ y \mid \phi\} \to X\in \mathcal P(A) $$


**Countability:** $\forall X: X \text { is countable }$



> 
> Is this theory interpretable in Kripke-Platek set theory (with Infinity)?
> 
> 
> 



> 
> If not, would it constitute a subsystem of second order arithmetic? If yes, what would be its proof theoretic ordinal?
> 
> 
> 



Does this restriction on powersets in ZF have a proof theoretic ordinal?
Your theory interprets $\mathsf{ZF}^-$. In fact, $\mathsf{ZF}-$ (namely, $\mathsf{ZF}$ without Powerset) interprets $\mathsf{ZF}^-+(V=L)$.
It answers your questions negatively since the proof-theoretic strength of $\mathsf{ZF}^-+(V=L)$ is that of Full Second-order Arithmetic.


The reason is that we can construct $L$ from $\mathsf{ZF}-$.
We need to check whether $\mathsf{ZF-}$ proves transfinite recursion, but you can check proofs in standard textbooks (like Jech or Kunen) work. Also, we can define $\operatorname{Def}(X)$ by using Replacement.


Work in $L$, we can see that $L$ has a natural rank function given by the $L$-hierarchy. Hence $L$ satisfies its own version of the reflection principle. We can see that $L$ satisfies $\mathsf{ZF}^-$ by using the reflection principle in $L$.


