Consider a theory $T$ with a binary relation $\in$ and the following axiom schemas:
- $\exists u \forall x (x \in u \leftrightarrow x \in a \land \phi)$ where $u$ is not free in $\phi$. This is the axiom schema of separation.
- $\phi \to \exists u \phi^u$. This is a form of reflection. We do not assert that $u$ is transitive.
Here, $\phi^u$ denotes $\phi$ with all quantifiers bounded to $u$: \begin{align} (\forall x \psi)^u &\leftrightarrow (\forall x \in u) \psi^u \\ (\exists x \psi)^u &\leftrightarrow (\exists x \in u) \psi^u \end{align}
Unlike this question, in this question, the notation $\phi^u$ bounds all quantifiers in $\phi$ to $u$, rather than just unbounded ones.
What is the interpretability strength of $T$? Is it as strong as or strictly weaker than second-order arithmetic?
