Boolean-valued semantics for names

In ZF let B be a complete set Boolean algebra with $0\mathrm{\ne }1$, using the abstract completeness clause of Completeness, regular opens, and order continuity. Use the name construction of Forcing names and their rank with coefficients in B, including zero. Write E(s,t) and I(s,t) for Boolean equality and membership values, prescribed by

$I(s,t)={\bigvee }_{⟨u,b⟩\in t}(b\wedge E(s,u)),$ $E(s,t)=({\bigwedge }_{⟨u,b⟩\in s}(\mathrm{\neg }b\vee I(u,t)))\wedge ({\bigwedge }_{⟨u,b⟩\in t}(\mathrm{\neg }b\vee I(u,s)))\mathrm{.}$

Existence and uniqueness of this atomic recursion are proved in the following lemma using Recursion on well-founded setlike relations on sets of descendant pairs. Put $\mathrm{\parallel }s\in t\mathrm{\parallel }=I(s,t)$ and $\mathrm{\parallel }s=t\mathrm{\parallel }=E(s,t)$. Boolean connectives use the corresponding Boolean operations. For each fixed formula phi, define its existential value by

$\mathrm{\parallel }\mathrm{\exists }x\varphi (x,t)\mathrm{\parallel }=\bigvee \{b\in B:\mathrm{\exists }\text{ B-name }s(b=\mathrm{\parallel }\varphi (s,t)\mathrm{\parallel })\}\mathrm{.}$

The join ranges over the set of attained values, not over a set of all names. This is a formula-by-formula definition; it asserts neither a uniform truth predicate for V nor a generic truth theorem. Empty joins are zero and empty meets are one. Completeness inside a ground model refers only to its subsets of B; no external completeness or absoluteness of quantified Boolean values is asserted.