The closed-term quotient structure

Let $H$ be a consistent, deductively closed, complete Henkin sentence theory in a set signature $L^{\mathrm{\prime }}$ with a seed constant $c_{\ast }$. Let $C$ be the set of closed $L^{\mathrm{\prime }}$-terms and $s\sim t$ mean $(s=t)\in H$. By Provable equality is a congruence on closed terms, this is an equivalence relation and a congruence. The closed-term model ${\mathcal{M}}_H$ has carrier $C\mathrm{/}\sim =\{[t]:t\in C\}$, where $[t]=\{s\in C:s\sim t\}$, and interpretations

$c^{{\mathcal{M}}_H}=[c],f^{{\mathcal{M}}_H}([t_1],\dots ,[t_n])=[f(t_1,\dots ,t_n)],$ $R^{{\mathcal{M}}_H}([t_1],\dots ,[t_n])⟺R(t_1,\dots ,t_n)\in H\mathrm{.}$

The earlier congruence proves that these values and truth assignments do not depend on representatives. Each finite tuple of classes has a tuple of representatives by finite induction, so the function interpretation is total; its value is unique, and defining its graph does not select representatives for the entire carrier. All graphs and relations are sets by Separation and Replacement. The seed gives $[c_{\ast }]$ in the carrier, so it is nonempty. Equality is literal equality of classes, not an additional relation. Thus this is a structure in the sense of Structures and variable assignments. Its satisfaction of $H$ is a separate truth-lemma conclusion.