7. Quantificateurs et règles supplémentaires

7. Quantificateurs et règles supplémentaires

7.1 Spécification universelle

À partir de ∀x A(x), on peut obtenir A(t) pour un terme admissible t. Par exemple :

∀x(homme(x)→mortel(x)) donne homme(Socrate)→mortel(Socrate).

Cette instanciation doit précéder le modus ponens avec homme(Socrate).

7.2 Spécification existentielle

À partir de ∃x A(x), on introduit un témoin frais c et on travaille avec A(c). Le symbole frais signifie seulement « un objet qui satisfait la propriété »; il ne doit pas être confondu avec une constante déjà porteuse d'une autre information.

Si un existentiel se trouve sous la portée de variables universelles, son témoin peut dépendre de celles-ci. On le remplace alors par une fonction de Skolem :

• ∀x∃z P(x,z) devient, dans la transformation appropriée, P(x,f(x));
• ∀x∀y∃z Q(x,y,z) utilise z := f(x,y).

Cette dépendance formalise la différence entre « pour chaque objet, il existe un choix » et « il existe un choix unique pour tous ».

7.3 Règles propositionnelles conservées

Les règles du §4 continuent de s'appliquer lorsque A, B et C sont des formules du premier ordre. La difficulté supplémentaire consiste à instancier les quantificateurs et à unifier les termes avant de faire correspondre les prémisses.