Well-definedness of Boolean-valued semantics

For input names s,t let C be the union of their descendant cones, including s,t. It is a set: iterate the operation adjoining first coordinates of pair entries through omega and take the union; Replacement and Union suffice. It is closed under subnames. On $C\times C$ assign the complexity $c(u,v)=(\max ({\mathrm{rk}}_B(u),{\mathrm{rk}}_B(v)),\min ({\mathrm{rk}}_B(u),{\mathrm{rk}}_B(v)))$ and order these ordinal pairs lexicographically. Any nonempty set of them has a least first coordinate and then a least second coordinate. Lowering either name rank strictly while retaining the other strictly lowers this sorted pair.

Recurse on the set $\{E,I\}\times C\times C$, with a triple preceding another whenever its complexity is smaller. The relation is well-founded by step 1.1 and setlike because its whole domain is a set. In I(u,v), every requested E(u,w) has w a subname of v; in E(u,v), the requested I(w,v) or I(w,u) lowers respectively the rank of u or v, allowing the coordinate swap. Thus every requested value is at smaller complexity. The sets of requested terms are set images of the pair entries, and completeness supplies their unique joins and meets. F3 gives existence and uniqueness of E and I on this domain.

For two descendant-closed sets the intersection is descendant-closed. Induction on the same ordinal-pair complexity shows their recursive values agree for all pairs in the intersection, since the defining clauses request only subname pairs there. The values therefore do not depend on the cone chosen. A single formula saying that a set-domain recursion on the canonical cone has a specified output defines the global atomic values. Any rival satisfies these clauses on each cone and agrees by uniqueness. No order of all pairs of names was claimed to be setlike.

Now induct externally through one fixed finite formula. Atomic values are definable by step 3.1. Negation, conjunction and other finite Boolean operations preserve definability and uniqueness. For an existential whose matrix value is already a definable class function, Separation on B forms the set of attained matrix values over all names, and completeness gives its unique supremum. This is a new defining formula for each fixed formula, not a uniform truth predicate. The same construction inside a ground model uses only its internally formed cones, images and subsets of B, so internal completeness suffices and no external completeness is inferred.