Consider a [set theory](https://en.wikipedia.org/wiki/Alternative_set_theory) with the following axioms:


1. [separation](https://en.wikipedia.org/wiki/Axiom_schema_of_specification): $\exists y \forall x (x \in y \leftrightarrow \phi \land x \in a)$ where $y$ is not free in $\phi$
2. [reflection](https://en.wikipedia.org/wiki/Reflection_principle): $\phi \to \exists u \phi^u$


where $\phi^u$ bounds all *unbounded* quantifiers in $\phi$ to $u$ (see [this question](https://math.stackexchange.com/questions/4528459/does-relativization-of-formulas-replace-bounded-quantifiers-or-not)). This theory proves:





| Result | Parameters | Formula $\phi$ |
| --- | --- | --- |
| existence |  | $\top$ |
| [pairing](https://en.wikipedia.org/wiki/Axiom_of_pairing) | $a,b$ | $\exists x (x = a) \land \exists x (x = b)$ |
| [union](https://en.wikipedia.org/wiki/Axiom_of_union) | $a$ | $\forall x\_{\in a} \forall y\_{\in x} \exists z (z = y)$ |
| [infinity](https://en.wikipedia.org/wiki/Axiom_of_infinity) | $a$ | $\exists x (x = a) \land \forall x \exists y (x \in y \land \forall z\_{\in y} (z = x))$ |
| [collection](https://en.wikipedia.org/wiki/Axiom_schema_of_replacement#Collection) for a [$\Delta\_0$](https://en.wikipedia.org/wiki/L%C3%A9vy_hierarchy#Definitions) formula $\psi$ | $a$ | $\forall x\_{\in a} \exists y \psi$ |
| [transitive model](https://en.wikipedia.org/wiki/Transitive_model) for a $\Delta\_0$ formula $\psi$ |  | $\psi \land \forall x \forall y\_{\in x} \exists z (z = y)$ |



What is the consistency strength and interpretability strength of this theory? Can it prove full collection? Has it been studied in the literature?



How strong is separation + reflection of unbounded quantifiers?
This theory is mutually interpretable with second-order arithmetic $\mathsf{Z}\_2$ and $\mathsf{ZFC}-\mathsf{PowerSet}$ (and hence equiconsistent with them). Note that the mentioned theories are well-known to be mutually interpretable: the interpretation of $\mathsf{ZFC}-\mathsf{PowerSet}$ in $\mathsf{Z}\_2$ is achieved by carriying out the construction of $L$.


Trivially your theory is a subtheory of $\mathsf{ZFC}-\mathsf{PowerSet}$ and hence is interpretable there. The non-trivial part of interpreting $\mathsf{Z}\_2$ in your theory is to show there that there is a model of second-order Peano arithmetic (in the signature with just the successor).


For that you simply take any set $A$ such that it contains an empty set and for any $x\in A$ there is a set of the form $\{x\}\cup x\in A$, i.e. it satisfies $$(\exists x\in A)(\forall y\in x) y\ne y \land (\forall x\in A)(\exists y\in A)((\forall z\in x)z\in y \land (\forall z\in y)(z=x\lor z\in x)).$$ Then you consider (set-encoded) binary relations $E$ on $A$ s.t. $x\_1 \mathrel{E} x\_2$, for all empty $x\_1,x\_2\in A$ and for every $x\_1 \mathrel{E} x\_2$ and $y\_1,y\_2$ of the shapes $\{x\_1\}\cup x\_1$, $\{x\_2\}\cup x\_2$ we have $y\_1\mathrel{E} y\_2$. Then you construct a least binary relation $E\_0$ like this. For this you, starting from a Cartesian square $U$ of $A$ (a set containing at least one presentation of pair $(x,y)$, for all $x,y\in A$), construct the set $E\_0\subseteq U$ that consists of all $z\in U$ of the form $(x,y)$ such that some presentation of $(x,y)$ is in every binary relation of the considered form. You put $N$ to be the subset of $A$ consisting only of $E\_0$-reflexive points. Finally you define the successor relation $x \mathsf{R} y$ to be $(\exists x',y'\in N)(x\mathrel{E} x'\land y\mathrel{E} y'\land \text{$y'$ is of the shape $\{x'\}\cup x'$})$. The structure $(N,E,S)$, where $E$ serves as equality clearly will be a model of second-order Peano arithmetic.


Your theory doesn't prove collection. In fact even the extension of Zermelo set theory with choice $\mathsf{ZC}$ by your reflection principle doesn't prove collection. For this let me show that $\mathsf{ZFC}$ proves consistency of this theory. We cosider an $\omega$-sequence of ordinals $\omega=\alpha\_0<\alpha\_1<\ldots$ such that each $\alpha\_{n+1}$ is least such that for every transitive model $M$, there is a transitive model $M'\in V\_{\alpha\_{n+1}}$ for which $M\cap V\_{\alpha\_n}=M'\cap V\_{\alpha\_n}$ and $M$ and $M'$ satisfy the same first-order formulas with parameters from $M\cap V\_{\alpha\_n}$. It is easy to see that for $\alpha\_\omega=\lim\_{n<\omega} \alpha\_n$ the model $V\_{\alpha\_\omega}$ is a model of $\mathsf{ZC}$ togethe r with reflection.


Don't know if this theory was studied.


