Lemme de vérité

L'énoncé $\exists x_0\, (x_0 = x_0)$ a un témoin, qui est une constante de $\mathcal L'$ : le modèle des termes clos est donc défini.

La hauteur $h(\sigma)$ d'une formule est le nombre d'occurrences de $\neg$, de $\to$ et de $\forall$ qu'elle contient. Si $\varphi$ n'a pas d'autre variable libre que $x$ et si $t$ est un terme clos, $\varphi[t/x]$ est un énoncé, de même hauteur que $\varphi$, puisqu'un terme ne contient aucun de ces symboles.

Montrons l'équivalence par récurrence sur $h(\sigma)$, pour tous les énoncés à la fois. Par la lecture unique, $\sigma$ est atomique, ou de la forme $\neg\tau$, $\tau \to \rho$ ou $\forall x\, \varphi$, avec $\tau$, $\rho$ des énoncés de hauteur plus petite et $\varphi$ une formule de hauteur $h(\sigma) - 1$ sans autre variable libre que $x$.

Cas atomique. Les termes d'un énoncé atomique sont clos. Par le point (iii) de Modèle des termes clos, $\mathcal M \models t = u$ équivaut à $[t] = [u]$, donc à $(t = u) \in \widehat T$ par (i).

De même, $\mathcal M \models R\, t_1 \cdots t_n$ équivaut à $([t_1], \dots, [t_n]) \in R^{\mathcal M}$, c'est-à-dire, par la définition de $R^{\mathcal M}$ et son indépendance des représentants, à $R\, t_1 \cdots t_n \in \widehat T$.

Négation. $\mathcal M \models \neg\tau$ équivaut à $\mathcal M \not\models \tau$, donc, par hypothèse de récurrence, à $\tau \notin \widehat T$, et donc à $\neg\tau \in \widehat T$, puisque exactement l'un de $\tau$ et $\neg\tau$ appartient à $\widehat T$ (Lemme de Lindenbaum, (iii)).

Implication. Si $\tau \notin \widehat T$, alors $\neg\tau \in \widehat T$, et l'instance de tautologie $\neg\tau \to (\tau \to \rho)$ donne $\widehat T \vdash \tau \to \rho$ ; si $\rho \in \widehat T$, l'instance $\rho \to (\tau \to \rho)$ donne de même $\widehat T \vdash \tau \to \rho$ ; dans les deux cas, $(\tau \to \rho) \in \widehat T$.

Réciproquement, si $(\tau \to \rho) \in \widehat T$ et $\tau \in \widehat T$, le modus ponens donne $\widehat T \vdash \rho$, donc $\rho \in \widehat T$.

Ainsi $(\tau \to \rho) \in \widehat T$ équivaut à « $\tau \notin \widehat T$ ou $\rho \in \widehat T$ », c'est-à-dire, par hypothèse de récurrence, à « $\mathcal M \not\models \tau$ ou $\mathcal M \models \rho$ », qui est la définition de $\mathcal M \models \tau \to \rho$.

Quantificateur. Soit $s$ une valuation. Par la définition de la satisfaction, $\mathcal M \models \forall x\, \varphi$ signifie $\mathcal M \models \varphi\,[s(x \mid a)]$ pour tout $a \in M$. Tout $a \in M$ s'écrit $[t] = t^{\mathcal M}[s]$ pour un terme clos $t$, et le lemme de substitution, qui s'applique puisque $t$ est substituable à $x$, donne $$\begin{aligned} \mathcal M &\models \varphi[t/x]\,[s] \\ \iff \mathcal M &\models \varphi\,[s(x \mid t^{\mathcal M}[s])]. \end{aligned}$$

Ainsi $\mathcal M \models \forall x\, \varphi$ équivaut à $\mathcal M \models \varphi[t/x]$ pour tout terme clos $t$, donc, par hypothèse de récurrence, à $\varphi[t/x] \in \widehat T$ pour tout terme clos $t$.

Il reste à voir que cette dernière condition équivaut à $\forall x\, \varphi \in \widehat T$. Si $\forall x\, \varphi \in \widehat T$, l'axiome (2) donne $\widehat T \vdash \varphi[t/x]$, donc $\varphi[t/x] \in \widehat T$, pour tout $t$.

Si $\forall x\, \varphi \notin \widehat T$, alors $\neg\forall x\, \varphi \in \widehat T$, et le point (v) des règles dérivées donne $\widehat T \vdash \exists x\, \neg\varphi$. La propriété des témoins fournit une constante $c$ telle que $$\widehat T \vdash \exists x\, \neg\varphi \to \neg\varphi[c/x] ;$$ ainsi $\widehat T \vdash \neg\varphi[c/x]$, donc $\neg\varphi[c/x] \in \widehat T$ et $\varphi[c/x] \notin \widehat T$ : la condition est en défaut pour le terme clos $c$.