# Does this restriction on powersets in ZF have a proof theoretic ordinal?

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?

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$$.