What is the proof of consistency of anterior reflection?

Question

Let Anterior Reflection be the following principle: $$\forall \vec{v}~ \exists X: \operatorname {transitive} (X) \land \, (\varphi \to \varphi^{X"}) $$

where $\varphi$ is a formula in $\sf FOL(=,\in)$ that doesn't use the symbol $X$, and $\varphi^{X"}$ refers to $\varphi$ being anteriorly bounded by $X$, that is a formula obtained from $\varphi$ by merely bounding some of its quantifiers by $X$ in such a manner that all preceding quantifiers (i.e. appearing on the left of it) must be bounded by $X$ also, i.e. the bounding by $X$ is closed anteriorly.

Note: bounding is of the form $\exists y \in X, \forall z \in X$.

Clearly, Anterior Reflection together with Specification principle would axiomatize $\sf ZF–Reg.–Powerset$, where Specification is: $$\forall \vec{v} ~ \forall A ~ \exists! x ~ \forall y ~ (y \in x \leftrightarrow y \in A \land \varphi) \text{ ;}$$ for every formula $\varphi$ not using the symbol "$x$".

If we upgrade anterior reflection to work on supertransitive sets, then with specification we get $\sf ZF–Reg.$.

Now, I think this is consistent.

What is the proof of consistency of anterior reflection?

Answer 1

This is a consequence of ZF as follows.

Assume that all quantifiers of $\varphi$ appear at the front as in the normal forms. Suppose that $\varphi(\vec v)$ has complexity at most $\Sigma_n$ for some large enough $n$. By the reflection theorem, there is a rank-initial segment $V_\kappa$ that is $\Sigma_n$-correct, meaning that all $\Sigma_n$ assertions are absolute from $V_\kappa$ to the full universe $V$. We may assume that $\vec v\in V_\kappa$. So not only is $\varphi$ absolute between $V_\kappa$ and $V$, but also all subformulas of $\varphi$. In particular, if $\varphi$ is true in the full universe $V$, then it will also be true if you bound the initial quantifiers of $\varphi$ by $V_\kappa$, since it doesn't matter for those whether you quantify over all of $V$ or just $V_\kappa$, as the result is the same by absoluteness. So anterior reflection holds. $$\forall \vec v\ \exists A(A\text{ is transitive and }\varphi\leftrightarrow\varphi^A).$$ The $A$ is simply the next $\Sigma_n$ correct $V_\kappa$ above the ranks of $\vec v$.