The Boolean-valued model $V^B$ is extensional.

Question

I am currently studying forcing from Jechs Set Theory and i have encountered this seemingly innocent lemma which says:$\\$

Lemma 14.17. $V^B$ is extensional.
Proof. Let $X,Y \in V^B$. By definition of $a \Rightarrow b$ we observe that if $a \le a'$, then $(a' \Rightarrow b) \le (a \Rightarrow b)$.
Thus for any $u \in V^B$ we have $(\|u \in X\| \Rightarrow \|u \in Y\|) \le (X(u) \Rightarrow \|u \in Y\|)$ and therefore:
$\hspace{2cm} \prod\limits_{u \in V^B}(\|u \in X\| \Rightarrow \|u \in Y\|) \le \prod\limits_{u \in V^B}(X(u) \Rightarrow \|u \in Y\|)$
While the left-hand side is equal to $\|\forall u(u \in X \rightarrow u \in Y)\|$, the right-hand side is easily seen to equal $\|X \subset Y\|$. Consequently,
$\hspace{2cm} \|\forall u(u \in X \leftrightarrow u \in Y)\| \le \|X = Y\|\hspace{7.7cm}\Box$

What confuses me here is the fact that $dom(X)$ can't be all of $V^B$ since there exists some $\alpha$ such that $X \in V^B_{\alpha + 1}$ and $dom(X) \subset V^B_\alpha$. So how do we evaluate $X(u)$ for $u \not\in dom(X)$? Do we substitute with $0$? How is the proof in the book valid?
Thanks, for your patience.

Answer 1

Your guess is correct: $X(u)$ should be interpreted as $0$ if $u$ is not in the domain of $X$. This makes sense intuitively: if you think of $X(u)$ as representing a "truth value" to which $u$ is an element of $X$, then any $u$ not in the domain should be assigned a truth value of $0$.

With this correction, the proof then works, since $X(u)\Rightarrow \|u\in X\|=1$ when $u\not\in dom(X)$ and these terms do not affect the meet and so $$\prod\limits_{u \in V^B}(X(u) \Rightarrow \|u \in Y\|)=\prod\limits_{u \in dom(X)}(X(u) \Rightarrow \|u \in Y\|)=\|X\subset Y\|.$$

Answer 2

So how do we evaluate $X(u)$ for $u \not\in dom(X)$? Do we substitute with $0$?

In this proof (1) that's exactly what we do. It's a slight abuse of notation (which is very common in all of mathematics).

(1) I wouldn't be surprised if the same abuse of notation occurs in a situation where evaluating it as $0$ does not yield the desired result. Hence I don't claim generality.

Answer 3

$X$ is a partial function, since it may not defined for every argument from $V^B$ and this is not explained well in Jech's book. For a partial function, all notions involving it are contingent on the function being defined. For example, for partial functions $f$ and $g$ we have that $f = g$ if for all $x$ we have that whenever $f(x)$ is defined and $f(x) = y$, then $g(x)$ is defined and $g(x) = y$ and vice versa.