Proposition 4Arithmétisation de la syntaxe

Occurrences libres et énoncés

On lit sur les positions des lettres la définition de Formules, variables libres. Comme dans la lecture unique, le bloc $\forall x$ compte pour un seul symbole. Dans une formule, chaque lettre $\forall$ est suivie de la variable de son bloc : les termes ne contiennent pas $\forall$ , et la seule règle qui introduit $\forall$ l'écrit suivi d'une variable.

Une occurrence d'une variable $x$ dans un mot $w$ est donc un rang $j$ où figure la lettre $x$ , sans que la lettre de rang $j - 1$ , s'il y en a une, soit $\forall$ . Une sous-formule de $w$ est un facteur de $w$ qui est une formule.

L'occurrence de rang $j$ est dans la portée d'un quantificateur $\forall x$ s'il existe une sous-formule $\forall x\, \psi$ de $w$ , commençant au rang $i$ , telle que $j$ soit le rang d'une lettre de $\psi$ , c'est-à-dire $i + 2 \leqslant j < l'$ , où $l'$ est le rang qui suit la dernière lettre de $\psi$ . Elle est liée si c'est le cas, libre sinon ; $x$ est une variable libre de $w$ si elle y a une occurrence libre.

C'est bien la définition de Formules, variables libres quand $w$ est une formule. Par récurrence sur la construction, chaque lettre $\forall$ d'une formule, au rang $i$ , commence une sous-formule $\forall x\, \psi$ issue de la règle du quantificateur, dont $\psi$ est la portée. Par le lemme des poids de la lecture unique, aucune formule n'est un préfixe propre d'une autre : $\psi$ est donc l'unique facteur commençant au rang $i + 2$ qui soit une formule, et les facteurs considérés ci-dessus sont exactement les portées des quantificateurs.

Énoncé

Les relations suivantes sont primitives récursives :

(i) $\mathrm{Oc}(N, j)$ : « $j$ est une occurrence de variable dans le mot de code $N$ » ;

(ii) $\mathrm{Lib}(N, j)$ : « $j$ est une occurrence libre » ;

(iii) $\mathrm{VL}(N, k)$ : « $a_k$ est une variable libre du mot de code $N$ » ;

(iv) l'ensemble $\mathrm{En}$ des codes des énoncés.

Démonstration

Les définitions se traduisent mot pour mot, avec $l = \mathrm{lg}(N)$ : $\begin{aligned} \mathrm{Oc}(N, j) \iff{} &j < l \wedge (N)^j \geqslant 8 \\ &\wedge \big(j = 0 \vee (N)^{j \mathbin{\dot{-}} 1} \neq 3\big). \end{aligned}$

L'occurrence $j$ est liée si et seulement si $\mathrm{Li}(N, j)$ , où $\begin{aligned} \mathrm{Li}(N, j) \iff{} &\exists i < j\ \exists l' < l + 1 \\ &\big((N)^i = 3 \\ &\wedge (N)^{i+1} = (N)^j \\ &\wedge i + 2 \leqslant j < l' \\ &\wedge \mathrm{Fm}(\mathrm{sm}(N, i + 2, l'))\big). \end{aligned}$ En effet, une sous-formule $\forall x\, \psi$ commençant au rang $i$ s'écrit avec $(N)^i = 3$ , la variable $x$ au rang $i + 1$ , et $\psi = \mathrm{sm}(N, i + 2, l')$ ; elle est contenue dans le mot, d'où les bornes $i < j$ et $l' \leqslant l$ .

Puis $\mathrm{Lib}(N, j) \iff \mathrm{Oc}(N, j) \wedge \neg \mathrm{Li}(N, j)$ , ensuite $\begin{aligned} \mathrm{VL}(N, k) \iff \exists j < l\ \big(&\mathrm{Lib}(N, j) \\ &\wedge (N)^j = k\big), \end{aligned}$ et enfin $\mathrm{En}(N) \iff \mathrm{Fm}(N) \wedge \forall j < l\ \neg\mathrm{Lib}(N, j)$ .

Toutes ces relations sont primitives récursives par Clôture, (i) et (iii), Codage des mots, (i), et Formules.

□

Remarque

Dans $\varphi = {\to}\, {=}\, x_0\, 0\, \forall x_0\, {=}\, x_0\, x_1$ , les occurrences de variables sont aux rangs $2$ , $7$ et $8$ ; le rang $5$ est la variable du bloc $\forall x_0$ . Le rang $7$ est lié, avec le témoin $i = 4$ et $l' = 9$ ; le rang $2$ est libre, faute de lettre $\forall$ avant lui ; le rang $8$ est libre, car le seul quantificateur porte sur $x_0$ . Les variables libres de $\varphi$ sont $x_0$ et $x_1$ , et $x_0$ a aussi une occurrence liée, comme dans la remarque de Formules, variables libres.

Les rangs des lettres de

\varphi

: la portée du bloc

\forall x_0

est le facteur des rangs

6

8

, qui est une formule, et l'arc bleu relie le bloc à l'occurrence qu'il lie. Les occurrences libres, en rouge, sont celles qu'aucun témoin

(i, l')

ne couvre.

Remarque

L'erreur la plus répandue est de compter la lettre $x$ du bloc $\forall x$ comme une occurrence. L'énoncé $\forall x_0\, (x_0 = x_0)$ aurait alors une occurrence libre de $x_0$ , celle du bloc, qui n'est dans la portée d'aucun quantificateur, et ne serait plus un énoncé. C'est pourquoi la relation $\mathrm{Oc}$ écarte les rangs qui suivent une lettre $\forall$ .

Remarque

La relation $\mathrm{Li}$ ne calcule pas la fin de la portée : elle demande seulement qu'il en existe une qui convienne, ce qu'une quantification bornée exprime. Le lemme des poids garantit qu'il y en a au plus une, et c'est lui qui identifie ce facteur à la portée de Formules, variables libres ; une fois cette identification faite, la relation $\mathrm{Li}$ n'a plus besoin de l'unicité.

Repose sur

Les formules forment un ensemble primitif récursif

Sert à

Substitution et substituabilité