Solution (source code)

= Solution

In the <Henkin construction>, first extend the consistent sentence set to a complete consistent theory with witnesses in an expanded language containing fresh constants. Its <term model> has <closed terms> modulo provable equality as elements:
$$
[t]=[u]\quad\Longleftrightarrow\quad T\vdash t\dot=u.
$$
Functions are interpreted by applying their symbols to representative terms, and an atomic predicate holds of term classes exactly when the corresponding atomic sentence belongs to $T$. Equality axioms make these definitions independent of representatives. The <Henkin witness property> handles the existential step in the truth lemma, so the resulting structure satisfies $T$ and hence the original $\Sigma$.

An arbitrary sentence set need not already have enough <closed terms> or witnesses. Calling this a term model for $\Sigma$ means a term-model construction of a model satisfying $\Sigma$, usually through that witnessed completion; it does not assert that every arbitrary $\Sigma$ itself already supplies the construction.