[proofplan] We first enlarge the finite list of formulas so that it contains all subformulas needed for an induction on complexity. The only non-formal case is the existential step: for each existential subformula, we assign to each tuple of parameters an ordinal bound below which a witness can be found whenever a witness exists in $V$. We then prove that the ordinals closed under these finitely many witness-rank requirements form a closed unbounded class. Finally, for any such closed ordinal $\alpha$, induction on formulas gives equivalence of truth in $V$ and in $V_\alpha$ for the original formulas. [/proofplan] [step:Close the finite family under subformulas] For each formula $\rho \in \Phi$, let $\rho^\dagger$ denote a formula obtained from $\rho$ by replacing the connectives $\vee$, $\to$, $\leftrightarrow$ and universal quantifiers by their standard first-order abbreviations using only atomic formulas, $\neg$, $\wedge$, and existential quantifiers. This replacement is purely logical: for every structure $M$ for the language $\{\in\}$ and every assignment $s$ of the free variables of $\rho$ into $M$, \begin{align*} M \models \rho[s] \quad \iff \quad M \models \rho^\dagger[s]. \end{align*} Thus the replacement preserves truth both in $V$ and in each structure $(V_\alpha,\in)$. Let $\Sigma$ be the finite set of all subformulas of the formulas $\rho^\dagger$ with $\rho \in \Phi$. Thus every normalized formula $\rho^\dagger$ belongs to $\Sigma$, and whenever $\exists x\,\psi(x,y_1,\dots,y_m)$ belongs to $\Sigma$, the formula $\psi(x,y_1,\dots,y_m)$ also belongs to $\Sigma$. For an ordinal $\alpha$, define $V_\alpha$ by the usual cumulative hierarchy: \begin{align*} V_0 &= \varnothing, \\ V_{\beta+1} &= \mathcal{P}(V_\beta), \\ V_\lambda &= \bigcup_{\beta<\lambda} V_\beta \quad \text{for limit ordinals } \lambda. \end{align*} We shall prove reflection for every formula in $\Sigma$. Since each original formula $\rho \in \Phi$ is logically equivalent to its normalized formula $\rho^\dagger$ in every structure for $\{\in\}$, this implies reflection for every original formula in $\Phi$. [/step] [step:Define ordinal bounds for existential witnesses] Fix an existential formula $\theta(y_1,\dots,y_m)$ in $\Sigma$ of the form \begin{align*} \theta(y_1,\dots,y_m) \equiv \exists x\,\psi(x,y_1,\dots,y_m). \end{align*} Define the following metatheoretic class function: \begin{align*} F_\theta: V^m &\to \operatorname{Ord} \\ (a_1,\dots,a_m) &\mapsto \begin{cases} \min\{\beta \in \operatorname{Ord} : \exists x \in V_\beta \text{ such that } V \models \psi(x,a_1,\dots,a_m)\}, & \text{if such } x \text{ exists}, \\ 0, & \text{otherwise}. \end{cases} \end{align*} The function $F_\theta$ is used only externally in the metatheory; when we form sets of bounds below, we use only its restrictions to set-sized domains $V_\alpha^m$. The minimum exists whenever the first case applies, because if some witness $x$ exists, then $x \in V_{\operatorname{rank}(x)+1}$. Let $\mathcal{F}$ be the finite collection of all functions $F_\theta$ obtained from existential formulas $\theta \in \Sigma$. [/step] [step:Construct a closed unbounded class of ordinals closed under witness bounds] Call an ordinal $\alpha$ closed under $\mathcal{F}$ if, for every function $F_\theta \in \mathcal{F}$ of arity $m$ and every tuple $(a_1,\dots,a_m) \in V_\alpha^m$, \begin{align*} F_\theta(a_1,\dots,a_m) < \alpha. \end{align*} We prove that the class $C$ of ordinals closed under $\mathcal{F}$ is closed and unbounded. First, $C$ is unbounded. Let $\gamma$ be any ordinal. Here $\mathbb{N}=\{1,2,3,\dots\}$ denotes the set of positive natural numbers. Define an increasing sequence of ordinals $(\alpha_n)_{n \in \mathbb{N}}$ recursively by choosing $\alpha_1 > \gamma$, and, once $\alpha_n$ is given, choosing $\alpha_{n+1}$ strictly larger than every ordinal in the set \begin{align*} \{F_\theta(a_1,\dots,a_m) : F_\theta \in \mathcal{F},\ (a_1,\dots,a_m) \in V_{\alpha_n}^m\}. \end{align*} This is a set of ordinals because $\mathcal{F}$ is finite and each $V_{\alpha_n}$ is a set. Let \begin{align*} \alpha = \sup_{n \in \mathbb{N}} \alpha_n. \end{align*} Then $\alpha > \gamma$. If $(a_1,\dots,a_m) \in V_\alpha^m$, then each $a_i$ belongs to some $V_{\alpha_{n_i}}$, so the finite tuple belongs to $V_{\alpha_N}^m$ for some $N \in \mathbb{N}$. By construction, \begin{align*} F_\theta(a_1,\dots,a_m) < \alpha_{N+1} \leq \alpha. \end{align*} Since $\alpha$ is a limit ordinal, this gives $F_\theta(a_1,\dots,a_m) < \alpha$. Hence $\alpha \in C$. Second, $C$ is closed. Let $(\alpha_i)_{i \in I}$ be an increasing cofinal sequence of ordinals in $C$, where $I$ is a directed index set for the displayed increasing sequence, and let \begin{align*} \lambda = \sup_{i \in I} \alpha_i. \end{align*} Fix $F_\theta \in \mathcal{F}$ of arity $m$. If $m=0$, choose any $i \in I$. Since $\alpha_i \in C$, \begin{align*} F_\theta() < \alpha_i \leq \lambda. \end{align*} If $m\geq 1$ and $(a_1,\dots,a_m) \in V_\lambda^m$, then for each $k \in \{1,\dots,m\}$ there is an ordinal $\beta_k < \lambda$ such that $a_k \in V_{\beta_k}$. Let \begin{align*} \beta = \sup\{\beta_1,\dots,\beta_m\}. \end{align*} Since $(\alpha_i)_{i \in I}$ is cofinal in $\lambda$, choose $i \in I$ such that $\beta < \alpha_i$. Then $(a_1,\dots,a_m) \in V_{\alpha_i}^m$. Since $\alpha_i \in C$, \begin{align*} F_\theta(a_1,\dots,a_m) < \alpha_i \leq \lambda. \end{align*} Thus $\lambda \in C$. Therefore $C$ is closed and unbounded. [/step] [step:Prove reflection by induction on formula complexity] Let $\alpha \in C$. We prove by induction on formulas $\varphi(v_1,\dots,v_n) \in \Sigma$ that for every tuple $(a_1,\dots,a_n) \in V_\alpha^n$, \begin{align*} V \models \varphi(a_1,\dots,a_n) \quad \iff \quad V_\alpha \models \varphi(a_1,\dots,a_n). \end{align*} For atomic formulas, the assertion follows because $V_\alpha$ is transitive: for $a,b \in V_\alpha$, the truth of $a=b$ and $a \in b$ is the same in $V_\alpha$ as in $V$. The Boolean cases follow directly from the induction hypothesis. For example, if $\varphi \equiv \neg \psi$, then \begin{align*} V \models \neg \psi(a) &\iff \text{not } V \models \psi(a) \\ &\iff \text{not } V_\alpha \models \psi(a) \\ &\iff V_\alpha \models \neg \psi(a). \end{align*} The case $\varphi \equiv \psi_0 \wedge \psi_1$ is identical, using the induction hypothesis for both components. It remains to handle the existential case. Suppose \begin{align*} \varphi(y_1,\dots,y_m) \equiv \exists x\,\psi(x,y_1,\dots,y_m), \end{align*} and let $(a_1,\dots,a_m) \in V_\alpha^m$. If $V_\alpha \models \exists x\,\psi(x,a_1,\dots,a_m)$, then there is $x \in V_\alpha$ such that \begin{align*} V_\alpha \models \psi(x,a_1,\dots,a_m). \end{align*} By the induction hypothesis applied to $\psi$, \begin{align*} V \models \psi(x,a_1,\dots,a_m), \end{align*} so $V \models \exists x\,\psi(x,a_1,\dots,a_m)$. Conversely, suppose $V \models \exists x\,\psi(x,a_1,\dots,a_m)$. Let $F_\varphi$ denote the witness-bound function associated to the existential formula $\varphi$. By the definition of $F_\varphi$, there is some $x \in V_{F_\varphi(a_1,\dots,a_m)}$ such that \begin{align*} V \models \psi(x,a_1,\dots,a_m). \end{align*} Since $\alpha$ is closed under $\mathcal{F}$ and $(a_1,\dots,a_m) \in V_\alpha^m$, \begin{align*} F_\varphi(a_1,\dots,a_m) < \alpha. \end{align*} Therefore $x \in V_\alpha$. Applying the induction hypothesis to $\psi$ gives \begin{align*} V_\alpha \models \psi(x,a_1,\dots,a_m), \end{align*} and hence \begin{align*} V_\alpha \models \exists x\,\psi(x,a_1,\dots,a_m). \end{align*} This completes the induction. [/step] [step:Conclude the closed unbounded reflection theorem] Every ordinal $\alpha \in C$ reflects every formula in $\Sigma$, and therefore reflects every formula in the original finite family $\Phi$. Since $C$ is unbounded in the ordinals, the class of reflection points for $\Phi$ is unbounded, so for every ordinal $\gamma$ there is some reflecting ordinal $\alpha>\gamma$. It remains to justify closedness for the actual class of reflection points. Let $(\alpha_i)_{i \in I}$ be an increasing cofinal sequence of ordinals each reflecting every formula in $\Sigma$, and let \begin{align*} \lambda = \sup_{i \in I} \alpha_i. \end{align*} We prove by induction on formulas $\varphi(v_1,\dots,v_n) \in \Sigma$ that for every tuple $(a_1,\dots,a_n) \in V_\lambda^n$, \begin{align*} V \models \varphi(a_1,\dots,a_n) \quad \iff \quad V_\lambda \models \varphi(a_1,\dots,a_n). \end{align*} The atomic and Boolean cases are identical to the induction already carried out for $\alpha \in C$. For the existential case, write \begin{align*} \varphi(y_1,\dots,y_m) \equiv \exists x\,\psi(x,y_1,\dots,y_m), \end{align*} and let $(a_1,\dots,a_m) \in V_\lambda^m$. If $V \models \varphi(a_1,\dots,a_m)$, choose $i \in I$ such that all parameters $a_1,\dots,a_m$ lie in $V_{\alpha_i}$; when $m=0$, choose any $i \in I$. Since $\alpha_i$ reflects $\varphi$, there is $x \in V_{\alpha_i} \subset V_\lambda$ such that \begin{align*} V_{\alpha_i} \models \psi(x,a_1,\dots,a_m), \end{align*} and reflection at $\alpha_i$ gives $V \models \psi(x,a_1,\dots,a_m)$. By the induction hypothesis for $\psi$ at $\lambda$, we get \begin{align*} V_\lambda \models \psi(x,a_1,\dots,a_m), \end{align*} so $V_\lambda \models \varphi(a_1,\dots,a_m)$. Conversely, if $V_\lambda \models \varphi(a_1,\dots,a_m)$, then some $x \in V_\lambda$ satisfies $V_\lambda \models \psi(x,a_1,\dots,a_m)$. The induction hypothesis for $\psi$ gives $V \models \psi(x,a_1,\dots,a_m)$, hence $V \models \varphi(a_1,\dots,a_m)$. Thus $\lambda$ reflects every formula in $\Sigma$, and therefore every formula in $\Phi$. The actual class of reflection points for $\Phi$ is closed and unbounded. [/step]