Lemme de coïncidence

Par récurrence sur les termes, la valeur d'un terme ne dépend que des valeurs de ses variables ; les cas atomiques s'en déduisent, et les connecteurs passent directement.

Pour $\forall x\, \varphi$, les variables libres sont celles de $\varphi$ privées de $x$. Pour tout $a \in M$, les valuations $s(x \mid a)$ et $s'(x \mid a)$ coïncident donc sur les variables libres de $\varphi$, et l'hypothèse de récurrence donne $$\begin{aligned} \mathcal M &\models \varphi\,[s(x \mid a)] \\ \iff \mathcal M &\models \varphi\,[s'(x \mid a)]. \end{aligned}$$ On conclut en quantifiant sur $a$.