Définition de la satisfaction

La relation $\mathcal M \models \varphi\,[s]$, lue « $\mathcal M$ satisfait $\varphi$ sous $s$ », est définie par récurrence sur $\varphi$ :

$\mathcal M \models t_1 = t_2\,[s]$ si $t_1^{\mathcal M}[s] = t_2^{\mathcal M}[s]$, et $\mathcal M \models R\, t_1 \cdots t_n\,[s]$ si $(t_1^{\mathcal M}[s], \dots, t_n^{\mathcal M}[s]) \in R^{\mathcal M}$ ;

$\mathcal M \models \neg\varphi\,[s]$ si $\mathcal M \not\models \varphi\,[s]$, et $\mathcal M \models (\varphi \to \psi)\,[s]$ si $\mathcal M \not\models \varphi\,[s]$ ou $\mathcal M \models \psi\,[s]$ ;

$\mathcal M \models \forall x\, \varphi\,[s]$ si $\mathcal M \models \varphi\,[s(x \mid a)]$ pour tout $a \in M$.