Proposition 1Σ₁-complétude formalisée et (D3)

Gabarits à plusieurs places et codes des instances à plusieurs paramètres

Les conventions sont celles de Substitution dépliée et de Formules des instances. Un gabarit à $r$ places est une suite finie $G = (g_0, \dots, g_{m-1})$ dont chaque terme est un entier ou l'un des signes $\diamond_1, \dots, \diamond_r$, qui peuvent ne pas tous y figurer. Pour des termes fonctionnels $\tau_1, \dots, \tau_r$, notés $\bar\tau$, on définit le terme fonctionnel $\llbracket G \rrbracket(\bar\tau)$ par récurrence sur $m$ : la suite vide donne $0$ ; si $G'$ est $G$ suivi de l'entier $c$, alors $\llbracket G' \rrbracket(\bar\tau) = \mathrm{aj}\big(\llbracket G \rrbracket(\bar\tau), \underline c\big)$ ; si $G'$ est $G$ suivi du signe $\diamond_i$, alors $\llbracket G' \rrbracket(\bar\tau) = \mathrm{conc}\big(\llbracket G \rrbracket(\bar\tau), \tau_i\big)$. Pour $r = 1$, ce sont les gabarits de Substitution dépliée. Le terme $\tau_i$ ne figure dans $\llbracket G \rrbracket(\bar\tau)$ que si $\diamond_i$ figure dans $G$ : ajouter ou retirer une place qui ne figure pas ne change pas le terme fonctionnel. On note $GH$ la suite $G$ suivie de la suite $H$, $G[H/\diamond_i]$ le gabarit obtenu en remplaçant chaque signe $\diamond_i$ de $G$ par la suite $H$, et $\bar\tau[\sigma]_i$ la suite $\bar\tau$ dont le $i$-ième terme est remplacé par $\sigma$.

Soit $\bar x = (x_1, \dots, x_r)$ une suite de variables distinctes, avec $x_i = a_{k_i}$. Pour un mot $w = a_{c_0} \cdots a_{c_{m-1}}$, le gabarit $G_{\bar x}(w)$ a pour terme de rang $j$ le signe $\diamond_i$ si $c_j = k_i$, et l'entier $c_j$ si $c_j$ n'est aucun des $k_i$ : on marque, lettre à lettre, toutes les lettres $x_i$. On pose $\ulcorner w \urcorner_{\bar x}(\bar\tau) = \llbracket G_{\bar x}(w) \rrbracket(\bar\tau)$ et, pour des termes $s_1, \dots, s_r$ du langage, $$\begin{aligned} &\ulcorner w[\dot s_1, \dots, \dot s_r/\bar x] \urcorner \\ &\quad = \ulcorner w \urcorner_{\bar x}\big(\mathrm{num}(s_1), \dots, \mathrm{num}(s_r)\big), \end{aligned}$$ abrégé $\ulcorner w[\dot{\bar s}/\bar x] \urcorner$ ; quand les $s_i$ sont les variables $x_i$ elles-mêmes, on écrit $\ulcorner w(\dot{\bar x}) \urcorner$. Pour $r = 0$, c'est un terme fonctionnel clos, dont $\mathsf{PA}$ démontre l'égalité avec le chiffre $\underline{\ulcorner w \urcorner}$, par le texte de Substitution dépliée ; on les emploie l'un pour l'autre.

Les $x_i$ sont des paramètres de $w$ si aucune d'elles n'est quantifiée dans $w$, au sens de Calcul à variables libres ; pour une formule, c'est dire qu'aucune lettre $\forall$ n'est suivie d'une lettre $x_i$, puisque chaque lettre $\forall$ d'une formule est suivie de la variable de son bloc (Variables libres). Chaque lettre $x_i$ est alors une occurrence libre : elle ne suit pas une lettre $\forall$, et aucun bloc $\forall x_i$ ne la lie. Ainsi $G_{\bar x}(w)$ marque exactement les occurrences libres des $x_i$ ; pour $r = 1$, c'est le gabarit $G_k(w)$ de Substitution dépliée, de sorte que $\ulcorner w[\dot y/x] \urcorner$ est le code de Formules des instances. Pour des termes $t_i$, le mot de code $\ulcorner w \urcorner_{\bar x}(\ulcorner t_1 \urcorner, \dots, \ulcorner t_r \urcorner)$ est la substitution simultanée $w[t_1, \dots, t_r/\bar x]$, et, pour des entiers $n_1, \dots, n_r$, le point (iv) de Termes fonctionnels donne $\vdash_{\mathsf{PA}} \ulcorner w[\dot{\bar y}/\bar x] \urcorner[\underline{n_1}, \dots, \underline{n_r}/\bar y] = \underline{\ulcorner w[\underline{n_1}, \dots, \underline{n_r}/\bar x] \urcorner}$.

La définition lettre à lettre rend le calcul des gabarits immédiat. On a $G_{\bar x}(uv) = G_{\bar x}(u)\, G_{\bar x}(v)$ pour des mots $u$ et $v$ ; en notation préfixée, avec $(c)$ pour le gabarit réduit à l'entier $c$, $$\begin{aligned} G_{\bar x}(\neg\varphi) &= (1)\, G_{\bar x}(\varphi), \\ G_{\bar x}({\to}\, \varphi\, \psi) &= (2)\, G_{\bar x}(\varphi)\, G_{\bar x}(\psi), \\ G_{\bar x}(\forall z\, \varphi) &= (3)(c)\, G_{\bar x}(\varphi), \\ G_{\bar x}({=}\, t\, u) &= (0)\, G_{\bar x}(t)\, G_{\bar x}(u), \end{aligned}$$ pour $z = a_c$ hors de $\bar x$, de même pour $S$, $+$ et $\times$, et $G_{\bar x}(x_i) = (\diamond_i)$. Enfin, si $u$ est une variable hors de $\bar x$ qui ne figure pas dans $w$, et $x$ une variable hors de $\bar x$ qui n'est pas quantifiée dans $w$, alors $G_{\bar x, u}(w[u/x]) = G_{\bar x, x}(w)$ : renommer un paramètre ne change pas le gabarit, donc $\ulcorner w[u/x] \urcorner_{\bar x, u}(\bar\tau, \tau)$ et $\ulcorner w \urcorner_{\bar x, x}(\bar\tau, \tau)$ sont le même terme fonctionnel.