= Solution
In the presence of <equality>, two syntactically different <closed terms> can be asserted equal by the <Henkin theory>, so the raw <first-order term> domain from part (b) must be replaced by a <quotient set>. Define
$$
t\sim u\quad\Longleftrightarrow\quad (t=u)\in H.
$$
The <equality> <axioms> give reflexivity, symmetry and transitivity, so this is an <equivalence relation>. Their substitution consequences make it a <congruence relation on a first-order structure>: replacing an input by an equivalent <first-order term> preserves equivalence of <function> values and preserves membership of <atomic formulas> in $H$.
Take domain $\{[t]:t\text{ is a closed term}\}$. Define a <function symbol> by $f([t_1],\ldots,[t_n])=[f(t_1,\ldots,t_n)]$, and relations by the same membership test as before using representatives. The <congruence relation on a first-order structure> makes these definitions independent of representatives. Actual identity of <equivalence classes> now agrees with the formal <equality> <first-order sentences> in $H$:
$$
\boxed{[t]=[u]\quad\Longleftrightarrow\quad(t=u)\in H.}
$$
This supplies the <equality> case of the <truth lemma for a Henkin term model>; the <logical connective> and <quantifier> cases then proceed exactly as in the <Henkin construction>. Thus the <term model> built from the <quotient set> is a genuine <first-order model> with <equality> interpreted as identity.
Back to article page
