I am trying to understand the proof of the following proposition from Halbeisen's Set Theory book:
$\textbf{Proposition}$: Every symmetric submodel $\hat{V}$ of $V[G]$ is a transitive model of $\textsf{ZF}$ which contains $V$, i.e., $V \subseteq \hat{V} \subseteq V[G]$ and $\hat{V} \vDash \textsf{ZF}$.
My problem is with his proof that $\hat{V}$ satisfies the Axiom Schema of Seperation:
Let $\varphi(x,y_{1},\dots, y_{n})$ be a first-order formula with free-variables as shown, $u,a_{1},\dots, a_{n} \in \hat{V}$ and let $\mathring{u},\mathring{a}_{1},\dots, \mathring{a}_{n}$ be the corresponding hereditarily symmetric $\mathbb{P}$-names for these sets. He claims that we have to find a hereditarily symmetric $\mathbb{P}$-name for the set \begin{equation*} w = \{v \in u: \varphi(v,a_{1},\dots, a_{n})\}. \end{equation*} However, I think there is some sort of mistake here. Shouldn't the quantifiers in the fomrmula $\varphi$ be restricted to $\hat{V}$?
Towards this end he considers the set name $\mathring{\overline{u}} := \{\langle \mathring{v},p\rangle: \exists q \in \mathbb{P}[p \leq q \wedge \langle \mathring{v},q\rangle \in \mathring{u}]\}$ and defines
\begin{equation*}
\mathring{w} = \{\langle \mathring{v},p\rangle \in \mathring{\overline{u}}: p \Vdash \varphi(\mathring{v},\mathring{a}_{1},\dots, \mathring{a}_{n})\}
\end{equation*}
Now he claims that $\mathring{w}_{G} = w$ and proceeds with his proof. However, the Truth Lemma for the forcing relation $\Vdash$ works only for truth in $V[G]$ and not truth in $\hat{V}$. Is there is a corresponding version of forcing relation $\Vdash$ that works for symmetric submodels? Is there something obvious that I am missing about this proof.
Yes. There is a symmetric forcing relation. Yes, it is the obvious thing, where we restrict the definition to names which are heteditarily symmetric names. Yes, it does have a Truth Lemma and it is well behaved.
Now, I don't have the book in front of me, but if you work with $\hat V$, then you are interpreting $w$ in that model, so there is no need to relativise the formula. But in general, yes, you are correct that the quantifers need to be restricted to that model.
I can see how an author will make mistakes like that, and how they might fall through the cracks when proofreading.