Solution (source code)

= Solution

Extend the <first-order variable assignment> recursively to <first-order terms> by
$$
\widetilde v(x_i)=v(x_i),\qquad\widetilde v(f(t))=f^{\mathcal A}(\widetilde v(t)).
$$
For atomic formulas, $\mathcal A\models t=s[v]$ exactly when $\widetilde v(t)=\widetilde v(s)$. Extend to the Boolean connectives by their <truth tables>, for example implication is false exactly when its antecedent is true and its consequent false. Quantifiers use modified <first-order variable assignments>:
$$
\begin{aligned}
\mathcal A\models\forall x_i\,\theta[v]&\iff\text{for every }a\in A,\quad\mathcal A\models\theta[v(x_i\mapsto a)],\\
\mathcal A\models\exists x_i\,\theta[v]&\iff\text{for some }a\in A,\quad\mathcal A\models\theta[v(x_i\mapsto a)].
\end{aligned}
$$
This recursion defines <satisfaction for a set structure> for every <first-order formula>.