# Truth values in Boolean valued models

In Devlin's "The Joy of Sets" the author introduces the Boolean valued model $V^{{\mathcal B}}$ based on a given Boolean algebra ${\mathcal B}$ and describes how to assign a truth value $\|\phi\|\in{\mathcal B}$ to any formula $\phi$ of set theory. In particular, one has the following recursion rules for quantifiers: $\|\exists u\phi(u)\|=\bigvee_{u\in V^{{\mathcal B}}} \|\phi(u)\|$ and $\|\forall u\phi(u)\|=\bigwedge_{u\in V^{{\mathcal B}}}\|\phi(u)\|$

I don't understand how this can be turned into a proper definition of $\phi$ since the indexing ranges over the proper class $V^{{\mathcal B}}$. Also, what kind of object is $\|-\|$ supposed to be in the end?

I thought about defining $\|\phi\|$ by restricting quantification to larger and larger $V^{{\mathcal B}}_{\alpha}$, but it is not clear to me why this should stabilize.

Also, I am confused since for ${{\mathcal B}}=\{0,1\}$ it seems that the existence of such a $\phi$ would contradict Tarski's undefinability theorem.

I'm grateful for any clarification!

-

The definition of $\|\varphi\|$ is separate for each formula (that is, the function $\varphi\mapsto\|\varphi\|$ is not definable, and why should it be? $\varphi$ is not an element of $V$ nor $V^\cal B$). This is a recursive construction in the meta-theory, taking a formula in the language of set theory, returning the formula for $\|\varphi\|$.
You're correct when you refer to Tarski's theorem. But this is exactly the case with the reflection theorem that states that $$V\models\varphi\implies\exists\alpha: V_\alpha\models\varphi$$
This theorem is a meta-theorem, and it cannot be internalized (uniformly) for the same reason that $\|\varphi\|$ cannot be internalized (uniformly), and for the same reason that $p\Vdash\varphi$ cannot be internalized (uniformly) when considering the internal definition using pre-dense sets below $p$ (rather than the definition using generic filters).
Thank you, Asaf & Zhen! @Asaf: Just to make sure I understand things correctly; how would, for example, the formula $\|u\in v\|$ look like explicitly? Do we prove first, for fixed $\alpha\in\text{Ord}$, the existence and uniqueness of $\|\in\|_\alpha: V^{{\mathcal B}}_\alpha\times V^{{\mathcal B}}_\alpha\to{\mathcal B}$ and $\|=\|_\alpha: V^{{\mathcal B}}_\alpha\times V^{{\mathcal B}}_\alpha\to{\mathcal B}$ satisfying the desired extensionality, and then take as $\|u\in y\|$ the formula $\exists\alpha\in\text{Ord}: x=\|\in\|_\alpha(u,v)$, and similar for $\|u=y\|$? – Hanno May 18 '14 at 11:12