Substitution et lemme de substitution

Montrons d'abord que, si l'on remplace par $t$ certaines occurrences de $x$ dans un terme, on obtient un terme, et dans une formule, une formule ; en particulier $\varphi[t/x]$ est une formule. On raisonne par récurrence sur la longueur, avec la lecture unique, en notant que remplacer des lettres d'un mot $w_1 w_2$ revient à remplacer celles de $w_1$, puis celles de $w_2$, et à concaténer.

Une variable devient $t$ ou reste elle-même, une constante reste elle-même. Dans $f\, u_1 \cdots u_n$, les lettres remplacées sont dans les $u_i$, et le résultat est $f$ suivi de $n$ termes. De même, $= u_1\, u_2$ et $R\, u_1 \cdots u_n$ donnent des formules atomiques, et $\neg\varphi$, $\to \varphi\, \psi$ donnent $\neg$ ou $\to$ suivi de formules. Dans $\forall y\, \varphi$, la lettre $y$ qui suit $\forall$ marque le quantificateur et n'est jamais remplacée : le résultat est $\forall y$ suivi d'une formule.

Venons au lemme. Posons $s' = s(x \mid t^{\mathcal M}[s])$. Pour les termes, on montre par récurrence sur $u$ que la valeur de $u[t/x]$ sous $s$ est celle de $u$ sous $s'$. Si $u = x$, les deux valent $t^{\mathcal M}[s]$ ; si $u$ est une autre variable ou une constante, $u[t/x] = u$ et $s'$ coïncide avec $s$ sur $u$. Si $u = f\, u_1 \cdots u_n$, alors $u[t/x] = f\, u_1[t/x] \cdots u_n[t/x]$, et l'on applique $f^{\mathcal M}$ aux valeurs, égales par hypothèse de récurrence.

Pour les formules, on raisonne par récurrence sur $\varphi$ ; les cas atomiques découlent du cas des termes, et les connecteurs passent directement.

Pour $\varphi = \forall y\, \psi$ : si $x$ n'est pas libre dans $\varphi$, la substitution ne change rien et le lemme de coïncidence conclut.

Sinon $y \neq x$, et l'hypothèse de substituabilité impose que $y$ ne figure pas dans $t$ ; ainsi $t$ a la même valeur sous $s$ et sous $s(y \mid a)$ pour tout $a$. Le terme $t$ est encore substituable à $x$ dans $\psi$, et, $x$ et $y$ étant distincts, $s(y \mid a)(x \mid b) = s(x \mid b)(y \mid a)$ pour tous $a$, $b$. On applique alors l'hypothèse de récurrence à $\psi$ sous chaque valuation $s(y \mid a)$, et l'on conclut en quantifiant sur $a$.