Why $V^B$ satisfies Separation

Question

In Chapter 14 of Jech's Set Theory, he writes the following (for the definition of $V^B$ see my question here):

Theorem 14.24. Every axiom of ZFC is valid in $V^B.$

For the proof of Separation, he writes the following:

Let $\varphi$ be a formula. We prove that for every $X\in V^B$ there is a $Y\in V^B$ such that $$(14.22) \qquad ||Y\subseteq X||=1 \text{ and } ||(\forall z\in X)(\varphi(z)\leftrightarrow z\in Y)||=1.$$ Let $Y\in V^B$ be as follows: $$\text{dom}(Y)=\text{dom}(X),\quad Y(t)=X(t)\cdot ||\varphi(t)||.$$ For every $x\in V^B$ we have $||x\in Y||=||x\in X||\cdot ||\varphi(x)||$ and this gives (14.22).

I have a few questions about this proof:

1. How are we meant to parse $||(\forall z\in X)(\varphi(z)\leftrightarrow z\in Y)||$? Am I correct to interpret it as $\prod_{z\in \text{dom}(X)}||\varphi(z)\leftrightarrow z\in Y||$? EDIT: This is incorrect. It should be $\prod_{z\in \text{dom}(X)}(X(z)\Rightarrow||\varphi(z)\leftrightarrow z\in Y||).$

2. How do we arrive at $||x\in Y||=||x\in X||\cdot ||\varphi(x)||$? I was able to get as far as $$||x\in Y||=\sum_{t\in \text{dom}(Y)}(||x=t||\cdot Y(t))=\sum_{t\in \text{dom}(X)}(||x=t||\cdot X(t)\cdot ||\varphi(t)||),$$ which almost looks like $||x\in X||\cdot ||\varphi(x)||$, but I don't understand how to relate $||\varphi(t)||$ to $||\varphi(x)||$.

3. Once we have this, how does (14.22) follow? I understand how $$||Y\subseteq X||=\prod_{t\in \text{dom}(Y)}(Y(t)\Rightarrow ||t\in X||)\geq \prod_{t\in \text{dom}(Y)}(Y(t)\Rightarrow ||t\in Y||)=1,$$ where the last equality follows from $Y(t)\leq ||t\in Y||$, but I'm having more trouble with the second part. Using the corrected interpretation from my first question, it suffices to show that $$(X(z)\Rightarrow||\varphi(z)\leftrightarrow z\in Y||)=1$$ for all $z\in \text{dom}(X)$. I believe this means I need
   $$(X(z)\Rightarrow(||\varphi(z)||\Rightarrow ||z\in Y||))=1 \text{ and }(X(z)\Rightarrow(||z\in Y||\Rightarrow||\varphi(z)||))=1.$$ The latter follows easily from $||z\in Y||\leq \varphi(z)$, but I don't see how to get the former. Can I get some help?

Answer 1

For (1): Typically, $(\forall x \in X) \phi(x)$ is taken to be purely syntactic sugar for the formula $(\forall x) (x \in X \rightarrow \varphi(x))$. From here, you would use the usual rules to say $$\lVert (\forall x) (x \in X \rightarrow \varphi(x)) \rVert = \prod_{x \in V^B} ( \lVert x \in X \rVert \Rightarrow \lVert \varphi(x) \rVert).$$ However, as Andreas Blass and you mention, there is a convenience lemma which states that this is equal to $$\prod_{t \in \operatorname{dom}(X)} (X(t) \Rightarrow \lVert \varphi(x) \rVert)$$ and this is often easier to work with.

(2): For each $t\in \operatorname{dom}(X)$, we have $\lVert x=t \rVert \cdot \lVert \varphi(t) \rVert = \lVert x=t \rVert \cdot \lVert \varphi(x) \rVert$, from which you can proceed from your expression to: $$\sum_{t \in \operatorname{dom}(X)} X(t) \cdot \lVert x=t \rVert \cdot \lVert \varphi(t) \rVert = \sum X(t) \cdot \lVert x=t \rVert \cdot \lVert \varphi(x) \rVert = \\ \left( \sum X(t) \cdot \lVert x=t \rVert \right) \cdot \lVert \varphi(x) \rVert = \lVert x \in X \rVert \cdot \lVert \varphi(x) \rVert.$$

To see that $\lVert x=t \rVert \cdot \lVert \varphi(t) \rVert = \lVert x=t \rVert \cdot \lVert \varphi(x) \rVert$, we use what should presumably have been a previous lemma. Namely: suppose $\Gamma$ is a set of (context) formulas, and $\varphi$ a target formula. Also, suppose that $\Gamma \vdash \varphi$ in pure first-order logic. Then for any assignment of free term variables of formulas in $\Gamma$ and free term variables in $\varphi$ to elements of $V^B$, and similarly for assignment of free propositional variables in $\Gamma$ and $\varphi$ to elements of $B$, we have $\prod_{\gamma \in \Gamma} \lVert \gamma \rVert \le \lVert \varphi \rVert$. (We eventually want to apply this in the special case that $\Gamma$ is the set of axioms of ZFC; but it is useful in the interim also.)

Now, $\{ x=t, \varphi(t) \} \vdash (x=t) \land \varphi(x)$ is easy to see using the substitution principle; therefore, $\lVert x=t \rVert \cdot \lVert \varphi(t) \rVert \le \lVert x=t \rVert \cdot \lVert \varphi(x) \rVert$. The converse inequality $\lVert x=t \rVert \cdot \lVert \varphi(x) \rVert \le \lVert x=t \rVert \cdot \lVert \varphi(t) \rVert$ is proved in a very similar way.

(3): Since $p \rightarrow (q \rightarrow r)$ is logically equivalent to $(p\land q) \rightarrow r$ in pure first-order logic, by applying the lemma mentioned in the previous part again, we see that $$(X(z) \Rightarrow (\lVert \varphi(z) \rVert \Rightarrow \lVert z \in Y \rVert)) = ((X(z) \cdot \lVert \varphi(z) \rVert) \Rightarrow \lVert z \in Y \rVert).$$ Therefore, to show this is equal to 1, it is sufficient to show $X(z) \cdot \lVert \varphi(z) \rVert \le \lVert z \in Y \rVert$. However, $X(z) \le \lVert z \in X \rVert$; therefore, $$X(z) \cdot \lVert \varphi(z) \rVert \le \lVert z \in X \rVert \cdot \lVert \varphi(z) \rVert = \lVert z \in Y \rVert$$ as required.