Instanciation universelle

De manière symbolique, la représentation de cette règle en tant que schéma d'axiome est :

(∀x A(x)) → A(a/x), avec la condition que a soit librement substituable à x dans A.

où a est un terme, et où A(a/x), appelé « substitution uniforme de x par a dans A » est le résultat de la substitution de toute occurrence libre de x dans A par a. La représentation en tant que règle d'inférence est :

Si ⊢ ∀x A alors ⊢ A(a/x) ou ${\displaystyle {\frac {\forall xA}{A(a/x)}}}$

Il faut prendre garde au cas où a est un terme qui contient des variables qui apparaissent liées dans A; si une occurrence de x apparait dans A dans le champ d'une de ces quantifications, la substitution « naïve » est fausse. C'est le phénomène dit de capture de variable. On a plusieurs solutions. Si la substitution est la substitution naïve, il faut interdire les substitutions avec capture de variable. C'est une solution qui fonctionne théoriquement, mais qui demande par exemple une règle de renommage des variables liées. On peut travailler également (il y a plusieurs façons de le réaliser) sur des formules à renommage des variables liées près, c'est-à-dire que l'on modifie la substitution pour qu'elle renomme les variables liées de façon satisfaisante en cas de capture de variables. La substitution n'est alors plus le simple remplacement d'occurrences d'une même lettre par un mot, mais tient compte de la structure logique de la formule.

L'exemple suivant illustre le phénomène de capture de variable. Dans la formule ${\displaystyle \forall x\exists y\ pere(x,y)}$, la variable x apparait dans le champ du quantificateur y. Si l'on souhaite substituer un terme a qui contient y, par exemple y lui-même, et que l'on utilise la substitution naïve, on a la dérivation suivante qui est erronée :

${\displaystyle {\frac {\forall x\exists y\ pere(x,y)}{\exists y\ pere(y,y)}}}$

La prémisse dit que tout individu x a un père y (qui dépend de x). La dérivation erronée conclut que l'individu y est son propre père, ce qui ne découle évidemment pas de la première affirmation. L'erreur vient du fait qu'il n'est pas permis de substituer directement y (ou un terme qui contiendrait y) à x, car dans la prémisse, x apparait dans le champ du quantificateur existentiel sur y, et donc y, au lieu d'être une variable libre de la conclusion, se trouve capturée par ce quantificateur.

Une déduction correcte est, à renommage des variables liées près :

${\displaystyle {\frac {\forall x\exists y\ pere(x,y)}{\exists z\ pere(y,z)}}}$

L'instanciation universelle est réalisée par la règle d'élimination de la déduction naturelle (énoncée indépendamment par Gerhard Gentzen et Stanislaw Jaskowski en 1934)[1]. C'est en quelque sorte un cas particulier de la règle gauche du quantificateur universel dans le calcul des séquents du même Gentzen. On la réalise souvent par un schéma d'axiomes dans un système à la Hilbert.

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Universal instantiation » (voir la liste des auteurs).

• Modus ponens
• Modus tollens