Propriétés démontrables de l'égalité

Si $\vdash \alpha$ et si $x_1, \dots, x_k$ sont des variables, on a $\vdash \alpha[w_1/x_1] \cdots [w_k/x_k]$ pour tous termes clos $w_1, \dots, w_k$ : on généralise et l'on instancie successivement (Règles dérivées, (ii) et (iii)). C'est sous cette forme que serviront les axiomes (5).

(i) L'axiome $x = x$ donne $\vdash t = t$.

(ii) Dans l'axiome (5), prenons pour $\alpha$ la formule atomique $x = x$, et pour $\alpha'$ la formule $y = x$, obtenue en remplaçant la première occurrence de $x$ par $y$ : $$\vdash x = y \to (x = x \to y = x).$$ En substituant $t$ à $x$ et $u$ à $y$, il vient $$\vdash t = u \to (t = t \to u = t),$$ et deux modus ponens, avec l'hypothèse $T \vdash t = u$ puis avec (i), donnent $T \vdash u = t$.

(iii) Avec $\alpha$ la formule $x = z$ et $\alpha'$ la formule $y = z$, l'axiome (5) donne $\vdash x = y \to (x = z \to y = z)$ ; en substituant $u$, $t$, $v$ à $x$, $y$, $z$ : $$\vdash u = t \to (u = v \to t = v).$$ Or $T \vdash u = t$ par (ii), et $T \vdash u = v$ : deux modus ponens donnent $T \vdash t = v$.

(iv) Fixons $i$ et des variables distinctes $x_1, \dots, x_n, y$. Soit $\alpha$ la formule atomique $f\, x_1 \cdots x_n = f\, x_1 \cdots x_n$, et $\alpha'$ celle où l'occurrence de $x_i$ dans le second membre est remplacée par $y$. L'axiome (5) donne $\vdash x_i = y \to (\alpha \to \alpha')$.

Substituons $u_j$ à $x_j$ pour $j < i$, $t_j$ à $x_j$ pour $j \geqslant i$, et $u_i$ à $y$ ; avec $$w = f\, u_1 \cdots u_{i-1}\, t_i \cdots t_n$$ et $$w' = f\, u_1 \cdots u_i\, t_{i+1} \cdots t_n,$$ il vient $\vdash t_i = u_i \to (w = w \to w = w')$, et deux modus ponens, avec l'hypothèse $T \vdash t_i = u_i$ puis avec (i), donnent $T \vdash w = w'$.

On passe ainsi de $f\, t_1 \cdots t_n$ à $f\, u_1 \cdots u_n$ en $n$ égalités démontrables, que (iii) enchaîne.

Pour un symbole de relation, l'axiome (5) appliqué à $R\, x_1 \cdots x_n$ et l'hypothèse $T \vdash t_i = u_i$ donnent de même, par modus ponens, $$\begin{aligned} T \vdash {}&R\, u_1 \cdots u_{i-1}\, t_i \cdots t_n \\ &\to R\, u_1 \cdots u_i\, t_{i+1} \cdots t_n \end{aligned}$$ pour chaque $i$, et ces $n$ implications s'enchaînent par la règle des tautologies.