Le modèle des termes clos

Par le point (iii) du lemme de Lindenbaum, $(t = u) \in \widehat T$ équivaut à $\widehat T \vdash t = u$ ; on emploie librement les propriétés de l'égalité démontrable.

(i) Si $[t] = [u]$, alors $u \in [u]$, puisque $\widehat T \vdash u = u$, donc $u \in [t]$, c'est-à-dire $\widehat T \vdash t = u$.

Réciproquement, supposons $\widehat T \vdash t = u$. Si $v \in [u]$, alors $\widehat T \vdash u = v$, donc $\widehat T \vdash t = v$ par transitivité, et $v \in [t]$ : ainsi $[u] \subset [t]$. Comme $\widehat T \vdash u = t$ par symétrie, le même raisonnement donne $[t] \subset [u]$.

(ii) Le domaine $M$ est non vide, puisqu'il contient $[c]$ pour une constante $c$. Si $[t_i] = [u_i]$ pour tout $i$, alors $\widehat T \vdash t_i = u_i$ par (i), et le point (iv) de l'égalité démontrable donne $\widehat T \vdash f\, t_1 \cdots t_n = f\, u_1 \cdots u_n$, donc $[f\, t_1 \cdots t_n] = [f\, u_1 \cdots u_n]$.

Il donne aussi $\widehat T \vdash R\, t_1 \cdots t_n \to R\, u_1 \cdots u_n$ : si $R\, t_1 \cdots t_n \in \widehat T$, alors $\widehat T \vdash R\, u_1 \cdots u_n$, donc $R\, u_1 \cdots u_n \in \widehat T$ ; la réciproque s'obtient en échangeant les rôles, par symétrie. Ainsi $f^{\mathcal M}$ est une application de $M^n$ dans $M$, et $R^{\mathcal M}$ une partie de $M^n$.

(iii) Par récurrence sur $t$ : $c^{\mathcal M}[s] = [c]$, et si $t = f\, t_1 \cdots t_n$, alors $$\begin{aligned} t^{\mathcal M}[s] &= f^{\mathcal M}(t_1^{\mathcal M}[s], \dots, t_n^{\mathcal M}[s]) \\ &= f^{\mathcal M}([t_1], \dots, [t_n]) = [t]. \end{aligned}$$ Un terme clos n'ayant pas de variable, la valuation n'intervient pas.