Solution (source code)

= Solution

The <cumulative-hierarchy reflection principle> says that for every finite collection $\Phi$ of formulas and every <ordinal> $\gamma$, there is an <ordinal> $\alpha>\gamma$ such that for all $\varphi\in\Phi$ and all parameters $a_1,\ldots,a_n\in V_\alpha$,
$$
\boxed{\varphi(a_1,\ldots,a_n)\ \Longleftrightarrow\
(V_\alpha,\in)\models\varphi(a_1,\ldots,a_n).}
$$
Equivalently, all quantifiers on the right are relativized to $V_\alpha$. It is a theorem schema of <ZF> for finite lists of formulas, with reflecting stages arbitrarily high. It does not assert one set-sized stage elementary for every formula at once. By beginning above the ranks of any specified finite parameter list, the parameters can also be required to belong to the reflecting stage.