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

Question

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?

Answer 1

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