Truth lemma for the term quotient

By term induction, the denotation of a term $u$ whose variables lie in the tuple is $[u[\bar{t}\mathrm{/}\bar{x}]]$. At a variable this is the given value, at a constant it is F1, and at $f(u_1,\dots ,u_r)$ the induction hypotheses and F1 give $[f(u_1[\bar{t}\mathrm{/}\bar{x}],\dots ,u_r[\bar{t}\mathrm{/}\bar{x}])]$, the required substituted term. Closed insertions do not acquire free variables; sequential substitution at distinct variables agrees here with simultaneous substitution, since inserted terms contain no free variables.

For equality atoms step 1.1 gives equality of classes iff the two closed terms are equivalent, which is exactly membership of their equality in $H$. For a relation atom, step 1.1 and its definition in F1 identify truth with membership of the substituted atom. F5 ensures the result is unchanged if any representative is replaced by an equivalent term.

Suppose the equivalence has been proved for immediate subformulas, with arbitrary finite representative tuples. At $\mathrm{\neg }\psi$, its semantic truth means failure of $\psi$; the induction hypothesis and F2 translate that to membership of the closed negation. At $\psi \wedge \theta$, truth means truth of both subformulas, which the hypotheses and F2 identify with membership of the closed conjunction. Both calculations are equivalences.

For $\varphi =\mathrm{\exists }y\psi$, substitute the supplied closed terms for the free variables other than $y$ in $\psi$, obtaining a matrix $\rho$ with free variables at most $y$. The closed instance of $\varphi$ is literally $\mathrm{\exists }y\rho$. If ${\mathcal{M}}_H,a\models \mathrm{\exists }y\psi$, take its one witness class $b$ and one closed term $u$ with $b=[u]$. The induction hypothesis for $\psi$ with the updated finite tuple gives $\rho [u\mathrm{/}y]\in H$. F2 gives $\mathrm{\exists }y\rho \in H$. Free-for composition here is legitimate because all inserted terms are closed: binders cannot capture them, and insertions in distinct free positions do not interfere; equivalently their semantic updates agree by F3.

Conversely if $\mathrm{\exists }y\rho \in H$, F2 supplies a closed term $u$ with $\rho [u\mathrm{/}y]\in H$. The induction hypothesis for $\psi$ gives ${\mathcal{M}}_H,a[y:=[u]]\models \psi$, hence the existential formula is true. If $y$ is vacuous, the same argument uses the nonempty quotient and the unchanged instance. These two directions establish the constructor case.

The atom, Boolean and existential cases exhaust the primitive syntax, so F4 proves the equivalence for every formula. For a sentence the tuple is empty and the closed instance is the sentence itself; each member of $H$ is therefore true in the quotient. At any induction step only finitely many representative classes and at most one additional witness are involved; finite existential selections are available in ZF and no global representative function is constructed.