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?

  • 4
    $\begingroup$ This comment will probably be removed as inappropriate, but I feel this question illustrates the problem with many of your posts. This is a legitimate question touching on the important Reflection Theorem of ZF, but it is an easy exercise for anyone who has gotten to that result in their first course on set theory. Could you please read a standard book on set theory like Jech, and start asking questions based on that? It seems like you have been trapped in a fascination with formal syntax and axioms for years, and you never get around to learning the actual content of set theory. $\endgroup$ Feb 29 at 12:02

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

  • $\begingroup$ Just want to make sure. To be pedantic, when you say the "initial quantifiers of $\varphi$" you mean the segment on the LEFT. So for example $\forall A \exists x \forall y: \psi$ so here $\forall A$ , or $\forall A \exists x$ would be examples of proper initial quantifiers. Because, that's what I mean by "anterior" in my stated qualification. $\endgroup$ Feb 28 at 20:57
  • 1
    $\begingroup$ Yes, that is what I meant. $\endgroup$ Feb 29 at 15:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.