Boolean truth for a supplied generic extension

F3 supplies internally the values of each fixed formula on its parameters. In particular, all atomic term families, and each fixed existential's set of attained values, are members of $M$ by its Replacement or Separation. All their elements are actual elements of $\mathbb{B}$ by transitivity. F5 identifies all ground subnames and their ranks with the external ones. Thus F1 applies to these families, although the externally supplied $G$ need not belong to $M$. No assertion of absoluteness of existential Boolean values is needed.

Fix ground names $s,t$. Their descendant closure $C\in M$ is a set closed under subnames: take the union of the finite iterations adjoining first coordinates of pair entries. On $C\times C$, order the complexity pairs $(\max ({\mathrm{rk}}_{\mathbb{B}}(u),{\mathrm{rk}}_{\mathbb{B}}(v)),\min ({\mathrm{rk}}_{\mathbb{B}}(u),{\mathrm{rk}}_{\mathbb{B}}(v)))$ lexicographically. Any nonempty set of these pairs has a least first coordinate and then a least second coordinate. Lowering either rank and retaining the other lowers this sorted pair, even when the coordinates exchange positions. Consequently simultaneous induction for equality and membership is legitimate: if some pair fails one of the two assertions, a least-complexity failing pair has all recursive subname pairs correct.

For membership, F2 and F1 give $I(s,t{)}^M\in G$ exactly when some $⟨u,b⟩\in t$ satisfies $b\wedge E(s,u{)}^M\in G$. In a proper Boolean filter this is equivalent to $b\in G$ and $E(s,u{)}^M\in G$: one direction uses upward closure and the other meet closure. Since $u$ is a proper subname of $t$, induction changes the equality clause to ${\mathrm{val}}_G(s)={\mathrm{val}}_G(u)$. F4 now identifies the existence of this pair exactly with ${\mathrm{val}}_G(s)\in {\mathrm{val}}_G(t)$. This proves both membership directions at this pair.

For equality, F1 applied to each of the two ground meets in F2 says $E(s,t{)}^M\in G$ exactly when every $⟨u,b⟩\in s$ satisfies $\mathrm{\neg }b\vee I(u,t{)}^M\in G$, and every $⟨u,b⟩\in t$ satisfies $\mathrm{\neg }b\vee I(u,s{)}^M\in G$. Ultrafilterhood makes $\mathrm{\neg }b\vee d\in G$ equivalent to the implication $b\in G\Rightarrow d\in G$. Indeed, if $b\mathrm{\notin }G$ then $\mathrm{\neg }b\in G$; if $d\in G$ the join is in $G$; and if both the join and $b$ are in $G$, their meet lies below $d$, so $d\in G$. Each membership call lowers the complexity by step 1.2. The induction hypotheses and F4 therefore identify the two conditions respectively with ${\mathrm{val}}_G(s)\subseteq {\mathrm{val}}_G(t)$ and the reverse inclusion. Actual Extensionality makes their conjunction equivalent to equality of the valuations. Both equality directions hold.

The simultaneous induction in steps 2.1–2.2 proves the assertion for all atomic formulas on ground names. Empty names cause no exception: their membership joins are zero and their empty equality requirements are one, matching empty valuation. A zero coefficient never belongs to $G$, and its implication clause is one, so zero coefficients impose no unwanted membership or equality condition. Since any two names admit the set descendant domain of step 1.2, this argument covers all the ground-name parameters.

Induct now on a fixed finite formula, using negation, conjunction and existential quantification as primitive logical operations. By F1, $\mathrm{\neg }b\in G$ iff $b\mathrm{\notin }G$, and $b\wedge c\in G$ iff both are in $G$. The corresponding external satisfaction clauses and the formula induction hypothesis establish the assertion for negation and conjunction, in both directions. Other finite Boolean connectives are their usual logical abbreviations.

For an existential with ground tuple $\vec{t}$, put $A=\{b\in \mathbb{B}:M\models \mathrm{\exists }\text{ Boolean name }s(b=\mathrm{\parallel }\psi (s,\vec{t})\mathrm{\parallel })\}$. This is the internally defined attained-value set in F2, so $A\in M$ by step 1.1. F1 says $\bigvee {}^{M}A\in G$ iff some $b\in A\cap G$ exists. Membership in this actual set $A$ means there is a witness name $s\in M$ with internal matrix value $b$; this is the semantics of the displayed existential in the supplied set structure $M$, and namehood agrees by F5. The formula induction hypothesis turns $b\in G$ into $M[G]\models \psi ({\mathrm{val}}_G(s),{\mathrm{val}}_G(\vec{t}))$. Conversely every witness in $M[G]$ has a ground name by F4, so an existentially true matrix supplies an attained value in $G$ and hence the join in $G$. This proves both existential directions without choosing a name for every element simultaneously.

The finite formula induction proves the statement, including universal quantification by negation and existential quantification. It concerns external satisfaction for the set structures supplied, with one Boolean defining formula for each fixed object-language formula. The proof used neither a uniform truth predicate for the universe nor a Boolean validity proof for any ZF axiom. The only choices of names or join witnesses were single existential witnesses within implications, so the argument remains in ZF.