Tables d'addition et de multiplication, valeurs des termes et formules atomiques sous la démontrabilité formalisée

Toutes les formules poussées sous $\mathrm{Prf}_T$ par le point (iii) de Instanciation à plusieurs paramètres sont ici sans quantificateur, de sorte que leurs variables en sont des paramètres ; ce sont des instances des axiomes de $\mathsf Q$, ou des formules que démontrent les règles de l'égalité de Calcul à variables libres, (vi), et la règle des tautologies. On note $\mathrm{D1}$ et $\mathrm{D2}$ les points (iii) et (iv) de Instanciation à plusieurs paramètres. Une égalité entre valeurs, comme $a + 0 = a$, se transporte dans un code par le remplacement appliqué au terme fonctionnel $\mathrm{num}(\cdot)$.

(i) Addition. Montrons, par récurrence sur $b$, avec le paramètre $a$, la formule $\Phi(b) = \mathrm{Prf}_T(\ulcorner (z_1 + z_2 = z_3)[\dot a, \dot b, (a + b)^{\boldsymbol\cdot}] \urcorner)$. Pour $0$, $\mathrm D1$ appliqué à l'axiome $z_1 + 0 = z_1$ ($\mathrm Q_4$), avec la valeur $a$, donne $\mathrm{Prf}_T(\ulcorner (z_1 + 0 = z_1)[\dot a/z_1] \urcorner)$. Ce code est celui de $\Phi(0)$ : la formule $z_1 + 0 = z_1$ s'obtient de $z_1 + z_2 = z_3$ en substituant $0$ à $z_2$ et $z_1$ à $z_3$, et le point (iii) de Gabarits à plusieurs places donne le code rempli par $\mathrm{num}(a)$, $\mathrm{num}(0)$ et $\mathrm{num}(a)$ ; on transporte enfin $\mathrm{num}(a) = \mathrm{num}(a + 0)$, par $\mathrm Q_4$.

Pour le pas, soit $c$ la valeur de $a + b$, et considérons, avec les places $z_1, z_2, z_3$ et les valeurs $a, b, c$, les formules $\theta_1 = (z_1 + S\,z_2 = S(z_1 + z_2))$, axiome $\mathrm Q_5$, $\theta_2 = (z_1 + z_2 = z_3 \to S(z_1 + z_2) = S\,z_3)$, et $\theta_3 = (\theta_1 \to (S(z_1 + z_2) = S\,z_3 \to z_1 + S\,z_2 = S\,z_3))$, que démontrent les règles de l'égalité. Par $\mathrm D1$, elles sont démontrables sous $\mathrm{Prf}_T$ avec ces valeurs. L'hypothèse de récurrence, où l'on transporte $\mathrm{num}(a + b) = \mathrm{num}(c)$, et $\mathrm D2$ appliqué à $\theta_2$ donnent $\mathrm{Prf}_T(\ulcorner (S(z_1 + z_2) = S\,z_3)[\dot a, \dot b, \dot c] \urcorner)$ ; deux applications de $\mathrm D2$ à $\theta_3$, avec $\theta_1$, donnent $\mathrm{Prf}_T(\ulcorner (z_1 + S\,z_2 = S\,z_3)[\dot a, \dot b, \dot c] \urcorner)$. Par le point (iii) de Gabarits à plusieurs places, appliqué deux fois, ce code est celui de $z_1 + z_2 = z_3$ rempli par $\mathrm{num}(a)$, $\mathrm{num}(S\,b)$ et $\mathrm{num}(S\,c)$, et l'on transporte $S\,c = S(a + b) = a + S\,b$, par $\mathrm Q_5$ : c'est $\Phi(S\,b)$. La récurrence (Récurrence dans PA, (iii)) conclut.

Multiplication. Même récurrence sur $b$. Pour $0$, $\mathrm D1$ appliqué à $z_1 \times 0 = 0$ ($\mathrm Q_6$) donne le code de $z_1 \times z_2 = z_3$ rempli par $\mathrm{num}(a)$, $\mathrm{num}(0)$, $\mathrm{num}(0)$, et l'on transporte $\mathrm{num}(0) = \mathrm{num}(a \times 0)$. Pour le pas, soit $c$ la valeur de $a \times b$ et $d$ celle de $c + a$, et prenons les places $z_1, z_2, z_3, z_4$ avec les valeurs $a, b, c, d$. L'axiome $\mathrm Q_7$ donne $z_1 \times S\,z_2 = z_1 \times z_2 + z_1$ ; l'hypothèse de récurrence et la formule $z_1 \times z_2 = z_3 \to z_1 \times z_2 + z_1 = z_3 + z_1$ donnent, par $\mathrm D2$, $z_1 \times z_2 + z_1 = z_3 + z_1$ sous $\mathrm{Prf}_T$ ; la table d'addition, où l'on substitue $c$ et $a$ à $a$ et $b$ (Termes fonctionnels, (ii) (b)), donne $z_3 + z_1 = z_4$, puisque le code de $z_1 + z_2 = z_3$ rempli par $\mathrm{num}(c)$, $\mathrm{num}(a)$, $\mathrm{num}(d)$ est le même terme fonctionnel que celui de $z_3 + z_1 = z_4$ rempli par les quatre valeurs. Deux applications de la transitivité, poussée sous $\mathrm{Prf}_T$ par $\mathrm D1$ et $\mathrm D2$, donnent $z_1 \times S\,z_2 = z_4$, qui est $z_1 \times z_2 = z_3$ rempli par $\mathrm{num}(a)$, $\mathrm{num}(S\,b)$ et $\mathrm{num}(d)$, la place $z_3$ ne figurant plus ; on transporte $d = a \times b + a = a \times S\,b$, par $\mathrm Q_7$.

(ii) Montrons, par récurrence sur $a$, la formule $\forall b\, \big(\neg(a = b) \to \mathrm{Prf}_T(\ulcorner \neg(z_1 = z_2)[\dot a, \dot b] \urcorner)\big)$. Pour $0$, sous l'hypothèse $\neg(0 = b)$, la symétrie et l'instance $\neg(b = 0) \to \exists w\, (b = S\,w)$ (Récurrence dans PA) permettent de raisonner sous $b = S\,b'$, pour une variable nouvelle $b'$. $\mathrm D1$ appliqué à $\neg(0 = S\,z_2)$, conséquence de $\mathrm Q_1$ et de la symétrie, avec la valeur $b'$, donne un code qui est, par le point (iii) de Gabarits à plusieurs places, celui de $\neg(z_1 = z_2)$ rempli par $\mathrm{num}(0)$ et $\mathrm{num}(S\,b')$ ; on transporte $S\,b' = b$, et l'on élimine $b'$.

Pour le pas, sous l'hypothèse de récurrence et sous $\neg(S\,a = b)$, distinguons $b = 0$ et $b = S\,b'$. Si $b = 0$, $\mathrm D1$ appliqué à $\neg(S\,z_1 = 0)$, avec la valeur $a$, donne le code de $\neg(z_1 = z_2)$ rempli par $\mathrm{num}(S\,a)$ et $\mathrm{num}(0)$. Si $b = S\,b'$, alors $\neg(a = b')$, puisque $a = b'$ donnerait $S\,a = b$ ; l'hypothèse de récurrence, instanciée par $b'$, donne $\mathrm{Prf}_T(\ulcorner \neg(z_1 = z_2)[\dot a, \dot b'] \urcorner)$, et $\mathrm D1$ et $\mathrm D2$, appliqués à la contraposée $\neg(z_1 = z_2) \to \neg(S\,z_1 = S\,z_2)$ de $\mathrm Q_2$, donnent le code de $\neg(S\,z_1 = S\,z_2)$, c'est-à-dire celui de $\neg(z_1 = z_2)$ rempli par $\mathrm{num}(S\,a)$ et $\mathrm{num}(S\,b')$. On transporte $S\,b' = b$, on généralise en $b$, et la récurrence conclut ; l'instanciation par $b$ donne l'énoncé.

(iii) Par récurrence sur la construction de $t$, en métathéorie. Si $t$ est $0$, le code est celui de $0 = z$ rempli par $\mathrm{num}(0)$, c'est-à-dire celui de l'énoncé $0 = 0$, et $\mathrm D1$, sans paramètre, conclut. Si $t$ est $x_i$, c'est le code de $x_i = x_i$, et $\mathrm D1$ appliqué à cette formule conclut. Si $t$ est $S\,t_1$, l'hypothèse de récurrence donne $\mathrm{Prf}_T(\ulcorner (t_1 = z)[\dot{\bar x}, \dot t_1] \urcorner)$ ; $\mathrm D1$ appliqué à $t_1 = z \to S\,t_1 = S\,z$, avec les valeurs $\bar x$ et une variable $y$ à laquelle on substitue ensuite $t_1$, puis $\mathrm D2$, donnent le code de $S\,t_1 = S\,z$ rempli par $\mathrm{num}(t_1)$, qui est celui de $S\,t_1 = z$ rempli par $\mathrm{num}(S\,t_1)$, par le point (ii) de Gabarits à plusieurs places.

Si $t$ est $t_1 + t_2$, soit $z'$ et $z''$ des variables nouvelles, distinctes. L'hypothèse de récurrence donne les codes de $t_1 = z'$ et de $t_2 = z''$, remplis par $\mathrm{num}(t_1)$ et $\mathrm{num}(t_2)$, et la table d'addition, où l'on substitue $t_1$ et $t_2$ à des variables $a$ et $b$ prises hors de ces termes, donne celui de $z' + z'' = z$, rempli par $\mathrm{num}(t_1)$, $\mathrm{num}(t_2)$ et $\mathrm{num}(t_1 + t_2)$, qui est le même terme fonctionnel que le code de $z_1 + z_2 = z_3$ rempli par ces valeurs. Avec les places $\bar x, z', z'', z$ et ces valeurs, $\mathrm D1$ et $\mathrm D2$ appliqués à $t_1 = z' \to (t_2 = z'' \to t_1 + t_2 = z' + z'')$, puis à la transitivité $t_1 + t_2 = z' + z'' \to (z' + z'' = z \to t_1 + t_2 = z)$, donnent le code de $t_1 + t_2 = z$, où les places $z'$ et $z''$ ne figurent plus. Le cas de $\times$ est le même, avec la table de multiplication.

(iv) Soit $z$ et $z'$ des variables nouvelles, distinctes. Sous l'hypothèse $t = u$, on transporte $\mathrm{num}(u) = \mathrm{num}(t)$ dans le code que (iii) donne pour $u = z$ ; avec celui de $t = z$, $\mathrm D1$ et $\mathrm D2$ appliqués à $t = z \to (u = z \to t = u)$, avec les places $\bar x, z$ et les valeurs $\bar x, t$, donnent le code de $t = u$, où la place $z$ ne figure pas. Sous l'hypothèse $\neg(t = u)$, le point (ii), où l'on substitue $t$ et $u$ à $a$ et $b$, donne le code de $\neg(z = z')$ rempli par $\mathrm{num}(t)$ et $\mathrm{num}(u)$, et (iii) ceux de $t = z$ et de $u = z'$ ; $\mathrm D1$ et trois applications de $\mathrm D2$ à $t = z \to (u = z' \to (\neg(z = z') \to \neg(t = u)))$, que démontrent les règles de l'égalité, donnent le code de $\neg(t = u)$. Le théorème de la déduction conclut dans les deux cas.