Lemme 1Arithmétique dans PA

Règles de démonstration dans l'arithmétique de Peano

L'arithmétique de Peano $\mathsf{PA}$ est celle de Théorèmes r.e. : six des axiomes de l'arithmétique de Robinson, et le schéma de récurrence. Elle démontre le septième, $\mathrm Q_3$ (Gödel-Rosser, (iii)), donc tout ce que démontre $\mathsf Q$ , par le lemme de remplacement de la preuve de Théorème de Craig. En particulier, les calculs de Calculs dans Q valent dans $\mathsf{PA}$ , ainsi que les instances de $\mathrm Q_1$ , $\mathrm Q_2$ , $\mathrm Q_4$ à $\mathrm Q_7$ par des termes quelconques, écrites au début de leur preuve, et, pour tout terme $t$ où ne figure pas la variable $w$ , l'instance $\neg(t = 0) \to \exists w\, (t = S\,w)$ du point (iii) de Calculs dans Q, obtenue par le point (ii) de Calcul à variables libres.

Dans tout ce chapitre, $\Gamma$ désigne un ensemble fini de formules, closes ou non, et l'on écrit $\Gamma \vdash_{\mathsf{PA}} \varphi$ pour $\mathsf{PA} \cup \Gamma \vdash \varphi$ , et $\vdash_{\mathsf{PA}} \varphi$ quand $\Gamma$ est vide. Dire que, sous les hypothèses $H_1, \dots, H_p$ , on a $C$ , c'est dire que $\{H_1, \dots, H_p\} \vdash_{\mathsf{PA}} C$ . Par le point (i) de Calcul à variables libres, toute formule $\psi$ telle que $\vdash_{\mathsf{PA}} \psi$ ou $\vdash \psi$ peut alors servir sous ces hypothèses, et la règle des tautologies s'y applique ; c'est ainsi qu'on emploie sous hypothèses les instances des axiomes, le remplacement d'un terme et les règles de l'égalité, points (v) et (vi) du même nœud. On écrit $t + u + r$ pour $(t + u) + r$ , et $t \times u + r$ pour $(t \times u) + r$ .

Énoncé

Soit $\Gamma$ un ensemble fini de formules, $\alpha$ , $\beta$ , $\varphi$ , $\psi$ des formules et $x$ une variable.

(i) Hypothèses. Si $\Gamma \vdash_{\mathsf{PA}} \varphi$ et si $x$ n'est libre dans aucune formule de $\Gamma$ , alors $\Gamma \vdash_{\mathsf{PA}} \forall x\, \varphi$ . Si $\Gamma \cup \{\varphi\} \vdash_{\mathsf{PA}} \psi$ et si $x$ n'est libre ni dans $\psi$ ni dans aucune formule de $\Gamma$ , alors $\Gamma \cup \{\exists x\, \varphi\} \vdash_{\mathsf{PA}} \psi$ . Si une variable $b$ ne figure ni dans $\varphi$ , ni dans $\psi$ , ni dans aucune formule de $\Gamma$ , et si $\Gamma \cup \{\varphi[b/x]\} \vdash_{\mathsf{PA}} \psi$ , alors $\Gamma \cup \{\exists x\, \varphi\} \vdash_{\mathsf{PA}} \psi$ .

(ii) Monotonie. Si $\Gamma \vdash_{\mathsf{PA}} \alpha \to \beta$ et si $x$ n'est libre dans aucune formule de $\Gamma$ , alors $\Gamma \vdash_{\mathsf{PA}} \forall x\, \alpha \to \forall x\, \beta$ et $\Gamma \vdash_{\mathsf{PA}} \exists x\, \alpha \to \exists x\, \beta$ .

Les points (i) et (ii) valent encore quand on remplace $\mathsf{PA}$ par une théorie quelconque, en particulier par la théorie vide, qui donne $\vdash$ .

(iii) Récurrence. Si $x$ n'est libre dans aucune formule de $\Gamma$ , si $\Gamma \vdash_{\mathsf{PA}} \varphi[0/x]$ et si $\Gamma \cup \{\varphi\} \vdash_{\mathsf{PA}} \varphi[S\,x/x]$ , alors $\Gamma \vdash_{\mathsf{PA}} \varphi$ et $\Gamma \vdash_{\mathsf{PA}} \forall x\, \varphi$ .

(iv) Substitution simultanée. Soit $T$ une théorie, $x_1, \dots, x_k$ des variables distinctes et $t_1, \dots, t_k$ des termes dont aucune variable n'est quantifiée dans $\alpha$ . Si $T \vdash \alpha$ , alors $T \vdash \alpha[t_1, \dots, t_k / x_1, \dots, x_k]$ .

Démonstration

(i) Montrons, par récurrence sur une démonstration formelle de $\varphi$ à partir de $\mathsf{PA} \cup \Gamma$ , que $\Gamma \vdash_{\mathsf{PA}} \forall x\, \gamma$ pour chacune de ses formules $\gamma$ . Si $\gamma$ est un axiome logique, $\forall x\, \gamma$ en est un aussi, puisque les axiomes logiques sont toutes les généralisations des formules des groupes (1) à (5) de Démonstrations formelles. Si $\gamma$ est un axiome de $\mathsf{PA}$ , c'est un énoncé, et si $\gamma$ est dans $\Gamma$ , la variable $x$ n'y est pas libre : dans les deux cas, l'axiome (4) $\gamma \to \forall x\, \gamma$ et le modus ponens concluent. Si $\gamma$ se déduit de $\beta$ et de $\beta \to \gamma$ par modus ponens, on a par hypothèse $\forall x\, \beta$ et $\forall x\, (\beta \to \gamma)$ , et l'axiome (3) $\forall x\, (\beta \to \gamma) \to (\forall x\, \beta \to \forall x\, \gamma)$ et deux modus ponens donnent $\forall x\, \gamma$ .

Pour l'élimination, le point (i) de Calcul à variables libres donne $\Gamma \vdash_{\mathsf{PA}} \varphi \to \psi$ , puis $\Gamma \vdash_{\mathsf{PA}} \neg\psi \to \neg\varphi$ par l'instance $(P \to Q) \to (\neg Q \to \neg P)$ . Ce qui précède donne $\Gamma \vdash_{\mathsf{PA}} \forall x\, (\neg\psi \to \neg\varphi)$ , et l'axiome (3) donne $\Gamma \vdash_{\mathsf{PA}} \forall x\, \neg\psi \to \forall x\, \neg\varphi$ . Comme $x$ n'est pas libre dans $\psi$ , l'axiome (4) donne $\vdash \neg\psi \to \forall x\, \neg\psi$ , et la règle des tautologies donne $\Gamma \vdash_{\mathsf{PA}} \neg\forall x\, \neg\varphi \to \psi$ , c'est-à-dire $\Gamma \vdash_{\mathsf{PA}} \exists x\, \varphi \to \psi$ (Quantificateurs) ; le modus ponens conclut sous l'hypothèse supplémentaire $\exists x\, \varphi$ .

Enfin, si $b$ ne figure ni dans $\varphi$ , ni dans $\psi$ , ni dans $\Gamma$ , ce qui précède, appliqué à la variable $b$ , donne $\Gamma \cup \{\exists b\, \varphi[b/x]\} \vdash_{\mathsf{PA}} \psi$ , et le renommage du point (iii) de Calcul à variables libres donne $\vdash \exists x\, \varphi \to \exists b\, \varphi[b/x]$ , puisque $b$ ne figure pas dans $\varphi$ .

(ii) Par (i), $\Gamma \vdash_{\mathsf{PA}} \forall x\, (\alpha \to \beta)$ , et l'axiome (3) donne la première implication. Pour la seconde, l'instance $(P \to Q) \to (\neg Q \to \neg P)$ donne $\Gamma \vdash_{\mathsf{PA}} \neg\beta \to \neg\alpha$ , la première donne $\Gamma \vdash_{\mathsf{PA}} \forall x\, \neg\beta \to \forall x\, \neg\alpha$ , et la même instance donne $\Gamma \vdash_{\mathsf{PA}} \neg\forall x\, \neg\alpha \to \neg\forall x\, \neg\beta$ .

Ces deux preuves n'emploient des axiomes de $\mathsf{PA}$ que le fait que ce sont des énoncés ; elles valent mot pour mot pour toute théorie, et pour la théorie vide.

(iii) Soit $I$ la formule $\big(\varphi[0/x] \wedge \forall x\, (\varphi \to \varphi[S\,x/x])\big) \to \forall x\, \varphi$ . Sa clôture universelle $\forall x_{i_1} \cdots \forall x_{i_g}\, I$ est un axiome de $\mathsf{PA}$ , et $g$ applications du point (iii) de Règles dérivées donnent $\vdash_{\mathsf{PA}} I$ . Le théorème de la déduction, sous la forme (i) de Calcul à variables libres, donne $\Gamma \vdash_{\mathsf{PA}} \varphi \to \varphi[S\,x/x]$ , et (i) donne $\Gamma \vdash_{\mathsf{PA}} \forall x\, (\varphi \to \varphi[S\,x/x])$ , puisque $x$ n'est pas libre dans $\Gamma$ . Avec $\Gamma \vdash_{\mathsf{PA}} \varphi[0/x]$ et $\vdash_{\mathsf{PA}} I$ , l'instance $P \to (Q \to (((P \wedge Q) \to R) \to R))$ donne $\Gamma \vdash_{\mathsf{PA}} \forall x\, \varphi$ . Enfin, $x$ est substituable à elle-même dans $\varphi$ , et l'axiome (2) $\forall x\, \varphi \to \varphi$ donne $\Gamma \vdash_{\mathsf{PA}} \varphi$ .

(iv) Soit $w_1, \dots, w_k$ des variables distinctes, différentes des $x_i$ , qui ne figurent ni dans $\alpha$ ni dans les $t_j$ ; sans cette précaution, un $x_i$ absent de $\alpha$ pourrait servir de $w_j$ , et une étape ultérieure remplacerait des lettres venues d'une autre variable. On substitue successivement $w_1$ à $x_1$ , …, $w_k$ à $x_k$ par le point (ii) de Calcul à variables libres : chaque $w_i$ , absente de la formule où on la substitue, y est substituable, et l'on obtient $T \vdash \alpha'$ , où $\alpha'$ porte la lettre $w_i$ exactement aux places des occurrences libres de $x_i$ dans $\alpha$ . On n'a remplacé que des occurrences libres : les blocs $\forall v$ de $\alpha'$ sont ceux de $\alpha$ , et aucune variable des $t_j$ n'y est quantifiée. On substitue ensuite successivement $t_1$ à $w_1$ , …, $t_k$ à $w_k$ : chaque $t_i$ est substituable, puisque aucune variable de $t_i$ n'est quantifiée, et chaque étape remplace exactement les lettres $w_i$ venues des occurrences libres de $x_i$ , puisque les $w_j$ ne figurent pas dans les termes $t_l$ déjà placés. Le résultat est $\alpha[t_1, \dots, t_k / x_1, \dots, x_k]$ .

□

Remarque

Voici une première récurrence. L'énoncé $\forall x\, \neg(S\,x = x)$ est vrai dans $\mathcal N$ , mais $\mathsf Q$ ne le démontre pas : dans la structure $\mathcal M$ de la deuxième remarque de Calculs dans Q, on a $S\,a = a$ , et le théorème de correction conclut. Dans $\mathsf{PA}$ , prenons $\varphi = \neg(S\,x = x)$ et $\Gamma$ vide. La formule $\varphi[0/x] = \neg(S\,0 = 0)$ est une instance de $\mathrm Q_1$ . Sous l'hypothèse $\neg(S\,x = x)$ , l'instance $S\,S\,x = S\,x \to S\,x = x$ de $\mathrm Q_2$ et la contraposition donnent $\neg(S\,S\,x = S\,x)$ , qui est $\varphi[S\,x/x]$ . Le point (iii) donne $\vdash_{\mathsf{PA}} \forall x\, \neg(S\,x = x)$ : la récurrence exclut exactement les éléments comme $a$ , que les axiomes de $\mathsf Q$ , qui ne parlent que d'un pas à la fois, laissent passer.

Remarque

La condition « $x$ n'est libre dans aucune formule de $\Gamma$ » est indispensable, et l'erreur la plus répandue est de l'oublier en raisonnant sous une hypothèse qui porte sur la variable de récurrence. Soit $\Gamma = \{x = S\,0\}$ et $\varphi = \neg(x = S\,0)$ . On a $\vdash_{\mathsf{PA}} \varphi[0/x]$ par le point (ii) de Calculs dans Q, et $\Gamma \cup \{\varphi\}$ , qui contient une formule et sa négation, démontre $\varphi[S\,x/x]$ . Pourtant $\Gamma \vdash_{\mathsf{PA}} \varphi$ est faux : il donnerait $\vdash_{\mathsf{PA}} x = S\,0 \to \neg(x = S\,0)$ , donc $\vdash_{\mathsf{PA}} \neg(x = S\,0)$ , puis $\vdash_{\mathsf{PA}} \neg(S\,0 = S\,0)$ par instanciation, alors que $\mathsf{PA}$ est cohérente (Gödel-Rosser, (iii)). Le pas de récurrence doit valoir pour un $x$ dont les hypothèses ne disent rien ; une hypothèse sur $x$ change en même temps que lui.

Remarque

Le schéma prend la clôture universelle : les variables libres de $\varphi$ autres que $x$ sont des paramètres, et le point (iii) est la récurrence avec paramètres, alors que la preuve de $\mathrm Q_3$ au nœud Gödel-Rosser n'en avait pas besoin. Les hypothèses de $\Gamma$ où $x$ n'est pas libre jouent le même rôle. Les nœuds qui suivent n'emploient que ces règles et celles de Calcul à variables libres ; le point (iv) étend aux formules quantifiées la substitution simultanée de ce nœud, qui ne portait que sur les formules sans quantificateur.

Repose sur

Représentation dans l'arithmétique de Robinson et théorème de Gödel-Rosser

Sert à

Lois de l'addition et de la multiplication dans l'arithmétique de Peano