Working in the first order language of set theory.

Let $\varphi^{*B}$ be the formula obtained from $\varphi$ by merely bounding *all* open quantifiers in $\varphi$ by the symbol "$B$".

Here a bounded quantifier in $\varphi$ can only be via $\in$ or $\subseteq$ relations, otherwise it's considered open. But, the bounding by $B$ to form $\varphi^{*B}$ is restricted via $\in$ relation.

**Bounding Reflection**: if $\varphi$ is a formula that doesn't use the symbol "$B$", then: $$ \forall \vec{v} \, \exists B \, (\varphi \to \varphi^{*B})$$

This can prove: pairing, union, power, infinity, and some instances of Replacement. I'm not sure if it can prove full replacement, but I don't think so.

Is this consistent with the axiom schema of Separation?

This question is related to this one , which virtually differs only in requiring bounding of open quantifiers to be closed anteriorly; that is, if an open quantifier is bounded by $B$ then all prior open quantifiers must be bounded by $B$, thereby only ensuring an *initial* segment of open quantifiers in $\varphi$ to be bounded by $B$, thus may be named as *anterior bounding reflection*. However, here a complete bounding of all open quantifiers by $B$ is required.

The rationale is that if this is solved to the positive, then an anterior bounded pathology to reflection would be excluded, and since this answer suggests no posterior pathology to reflection, therefore anterior bounding reflection may stand a chance of being consistent.

7more comments