Instanciation universelle

En logique, l'instanciation universelle (également appelée Dictum de omni) est une règle d'inférence qui permet, à partir d'une vérité sur l'ensemble des membres d'une classe d'entités, d'inférer une vérité sur une entité particulière de cette classe. Elle est généralement considérée comme une règle de quantification pour le quantificateur universel, mais elle peut également être énoncée en tant qu'axiome. C'est l'un des principes de bases de la théorie de la quantification. Exemple : « Tous les hommes sont mortels. Socrate est un homme. Donc Socrate est mortel. » 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 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.