Skolémisation

En logique mathématique, la skolémisation d'une formule du calcul des prédicats est une transformation de cette formule, qui, dans le cas d'une forme prénexe, consiste à éliminer toutes les occurrences de quantificateur existentiel en utilisant de nouveaux symboles de fonction (un par quantification existentielle), tout en conservant la satisfaisabilité de la formule.

La terminologie fait référence au logicien Thoralf Skolem et les fonctions introduites, que l'on peut voir comme des fonctions de choix, sont appelées fonctions de Skolem.

Définition

Intuitivement, si on a une formule du type $\forall x\,\exists y\,P(x,y)$ on peut se dire que pour chaque $x$ il existe (au moins) un $y$ tel que $P(x,y)$ est vrai, on peut donc supposer qu'il y a une fonction $f(x)$ qui nous fournit un « bon » $y$ pour chaque $x$. Ceci nous permet de réécrire la formule comme $\forall x\,P(x,f(x))$.

Il est plus simple de décrire la skolémisation pour une formule sous forme prénexe, c'est-à-dire avec tous les quantificateurs au début (ce qui est toujours possible, en appliquant les équivalences connues). Dans ce cas, chaque occurrence d'une variable $y$ quantifiée existentiellement est remplacée par un terme $f(x_{1},\ldots ,x_{n})$ où $x_{1},\ldots ,x_{n}$ sont les variables quantifiées universellement dont les quantificateurs apparaissent avant celui de $y$. S'il n'y a aucun quantificateur universel avant $\exists y$, $f$ sera une fonction 0-aire, c'est-à-dire une constante. Pour chaque variable à skolémiser il faut choisir un nouveau nom de fonction qui n’apparaît pas déjà dans la formule.

La formule obtenue, qui est une formule prénexe n'ayant que des quantificateurs universels en tête, est parfois dite sous forme normale de Skolem. Il n'y a pas unicité (même au nom des symboles de fonctions près, et à équivalence près de la partie propositionnelle) de la forme normale de Skolem d'une formule donnée.

Exemples

1. La formule $\forall x\exists y\forall zP(x,y,z)$ n'est pas sous forme normale de Skolem car elle contient un quantificateur existentiel. La skolémisation remplace $y$ par $f(x)$, où $f$ est une nouvelle fonction et supprime le quantificateur $\exists y$. La formule résultante est $\forall x\forall zP(x,f(x),z)$.
2. La formule $\forall x\,\exists y\,(\mathrm {Etudiant} (x)\to (\mathrm {Fac} (y)\land \mathrm {Inscrit} (x,y)))$ peut être skolémisée en $\forall x(\mathrm {Etudiant} (x)\to (\mathrm {Fac} (f(x))\land \mathrm {Inscrit} (x,f(x)))$
3. La formule $\forall x\,\exists y\,\forall z\,\exists u\,(R(x,y)\land S(y,z,u))$ peut être skolémisée en $\forall x\,\forall z\,(R(x,f(x))\land S(f(x),z,g(x,z)))$ ($y$ dépend uniquement de $x$, $u$ dépend de $x$ et de $z$)
4. La formule $\exists x\,\forall y\,(x>y)$ deviendra $\forall y\,(c>y)$, où $c$ est une constante.

Propriétés

La version skolémisée d'une formule ne lui est en général pas équivalente (le langage étant étendu). Néanmoins :

– tout modèle (ou même bien sûr sa restriction au langage initial) de la formule skolémisée est modèle de la formule initiale ;

– tout modèle de la formule initiale peut en présence de l'Axiome du Choix être étendu en un modèle de la formule skolémisée, obtenu en conservant les interprétations des symboles de la signature initiale, et en interprétant correctement les nouveaux symboles de fonction introduits par la skolemisation.

Une formule close et sa forme de Skolem sont donc dans ZFC ce que l'on appelle équisatisfaisables, ou équicohérentes : l'une possède un modèle si, et seulement si l'autre en possède un.

Utilisation

En raisonnement automatique et en programmation logique (p. ex. dans le langage Prolog), on utilise fréquemment le principe de résolution de Robinson ; or cette règle d'inférence ne s'applique que sur des formules dont les variables sont toutes quantifiées universellement (en fait sur des clauses) : il suffit donc d'appliquer la skolémisation avant de pouvoir appliquer la résolution.

Herbrandisation

On appelle aussi herbrandisation, du nom du logicien français Jacques Herbrand, la transformation duale de la skolémisation, qui traduit tous les quantificateurs universels en fonctions. Cela revient à skolemiser la négation de la formule : la négation de la formule herbrandisée est équisatisfaisable avec la négation de la formule initiale. La forme de Herbrand d'une formule est donc universellement valide (ou, par complétude, démontrable) si et seulement si la formule initiale l'est. Pas plus que la forme de Skolem, et pour les mêmes raisons (le langage est enrichi au cours de la transformation), la forme de Herbrand d'une formule n'est en général équivalente à celle-ci.

Par exemple, la formule

$F:=\forall y\exists x[R(y,x)\wedge \neg \exists zS(x,z)]$

devient, par herbrandisation,

$F^{H}=\exists x[R(c,x)\wedge \neg S(x,f(x))].$

La variable $y$ est remplacée par une constante, c'est-à-dire une fonction 0-aire, car la quantification universelle $\forall y$ ne dépend d'aucune quantification existentielle. En revanche, la quantification $\forall z\neg S$, à laquelle se résume $\neg \exists zS$, dépend de la quantification existentielle $\exists x$ ; c'est pourquoi la variable $z$ est traduite par une fonction $f(x)$.

Annexes

Articles connexes

• Élimination des quantificateurs
• Théorème de Herbrand
• Calcul des prédicats
• Théorie des modèles
• Modèle

Bibliographie

• Th. Skolem, « Sur la logique mathématique », in Jean Largeault, Logique mathématique. Textes, Paris, Armand Collin, Épistémologie, 1972, p. 91-108.
• (en) Dirk van Dalen (de), Logic and Structure, Third edition, ed. Springer-Verlag, Berlin Heidelberg, 1994. Chapitre « 3.4 Skolem Functions or How to Enrich Your Language », pp. 136-142 (de la 3^e édition). (ISBN 3-540-57839-0) et (ISBN 0-387-57839-0).
• Michel de Rougemont et Richard Lassaigne, Logique et fondements de l'informatique (logique du premier ordre, calculabilité et lambda calcul), Partie 3.3 : Formules prénexes. Formes de Skolem, Hermes Science Publications, 1997. (ISBN 2-86601-380-8)