Question of the proof of generalized reflection principle

Question

On page 25, Constructibility, K.J.Devlin,

Let $(W_{\alpha} | \alpha \in On)$ be a hierarchy of transitive sets, definable by a formula, $Ψ$, of LST(language of set theory) in the sense that $$W_{\alpha}=(x | Ψ(x, \alpha))$$ and suppose that:$$ \alpha <β \to W_{\alpha} \subseteq W_β$$ $$\delta \text{ is a limit ordinal} \to W_{\delta} = \bigcup_{\alpha < \delta} W_{\alpha}$$ Let $$W = \bigcup_{\alpha \in On} W_{\alpha}$$ Let $Φ (\vec{v})$ be an LST-formula with free variables amongst $\vec{v} $ (We use $\vec{v} $ to denote finite strings of variables). Let $Φ_0 (\vec{x}_0),..., Φ_n (\vec{x}_n)$ be a sequence of LST-formulas such that $Φ_n = Φ$ and for each $i = 0,..., n$, either $Φ_i$ is a primitive formula or else is obtained from previous formulas in the sequence by a direct application of negation, conjunction, or existential quantification. (The existence of such a sequence follows from the definition of a formula of LST.) We define ordinal-valued functions $f_i (\vec{x}_i), i = 0,..., n$, as follows. If $Φ_i$ is primitive or of the form $ \lnot Φ_j$ for some $j < i$, or of the form $Φ_j \land Φ_k$ for some $j , k < i$, let $ f_i (\vec{x}_i) = 0$. If $Φ_i(\vec{x}_i)$ is of the form $\exists yΦ_j(y, \vec{x}_i)$ for some $j < i$, let$f_i(\vec{x}_i)$ be the least ordinal $γ$ such that $$(\exists y \in W) Φ_j^W (y,\vec{x}_i) \to (\exists y \in W_γ) Φ_j^W (y,\vec{x}_i) $$ ($Φ^W$ is the relativίsation of $Φ$ to $W$.)

My question is how to show the existence of such $γ$. Or why there exists $W_γ$ to allow $(\exists y \in W) Φ_j^W (y,\vec{x}_i) \to (\exists y \in W_γ) Φ_j^W (y,\vec{x}_i) $?

Answer 1

There are two cases, it seems: either the antecedent is true or false.

• If the antecedent is true, then there actually is some $y \in W$ such that $\Phi_j^W ( y , \vec{x}_i )$ holds. As $W = \bigcup_{\gamma \in \mathrm{On}} W_\gamma $ the class $Y = \{ \gamma \in \mathrm{On} : ( \exists y \in W_\gamma )( \Phi^W_j ( y , \vec{x}_i ) \}$ is nonempty, and has a minimal element. Note that technically we are looking for the least $\gamma$ such that $( \exists y ) ( \Psi ( y , \gamma ) \wedge \Phi^W_j ( y , \vec{x}_i) )$ holds, but this just ensures that the class $Y$ "exists".)
• If the antecedent is false, then the implication is true for all ordinals $\gamma$, in particular for $\gamma = 0$.

Note that in this part of the proof you are not looking for a $\gamma$ such that the implication $$\large ( \exists y \in W ) \Phi^{W}_j ( y , \vec{x}_i ) \rightarrow ( \exists y \in W_\gamma ) \Phi^{W_{\color{red}{\gamma}}}_j ( y , \vec{x}_i )$$ holds. (Look for the smallish red $\color{red}{\gamma}$.)