Set Theory – How Strong is Separation and Reflection of Unbounded Quantifiers?

Question

Consider a set theory with the following axioms:

1. separation: $\exists y \forall x (x \in y \leftrightarrow \phi \land x \in a)$ where $y$ is not free in $\phi$
2. reflection: $\phi \to \exists u \phi^u$

where $\phi^u$ bounds all unbounded quantifiers in $\phi$ to $u$ (see this question). This theory proves:

Result	Parameters	Formula $\phi$
existence		$\top$
pairing	$a,b$	$\exists x (x = a) \land \exists x (x = b)$
union	$a$	$\forall x_{\in a} \forall y_{\in x} \exists z (z = y)$
infinity	$a$	$\exists x (x = a) \land \forall x \exists y (x \in y \land \forall z_{\in y} (z = x))$
collection for a $\Delta_0$ formula $\psi$	$a$	$\forall x_{\in a} \exists y \psi$
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?

Answer 1

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.