En logique du premier ordre, on cherche souvent à simplifier la structure des formules.
- Forme Normale Prénexe : Une formule est en forme prénexe si tous ses quantificateurs ($\forall, \exists$) sont regroupés au début de la formule. Toute formule peut être transformée en une formule logiquement équivalente qui est en forme prénexe. Exemple : $\forall x \exists y \forall z, P(x,y,z)$.
- Satisfiabilité : Une formule est satisfiable s’il existe au moins un modèle (une interprétation) qui la rend vraie.
- Équisatisfiabilité : Deux formules $\varphi$ et $\psi$ sont équisatisfiables si ($\varphi$ est satisfiable $\iff \psi$ est satisfiable). C’est une notion plus faible que l’équivalence logique : deux formules équisatisfiables ne sont pas nécessairement vraies dans les mêmes modèles, mais si l’une a un modèle, l’autre en a un aussi.
Pour toute formule $\varphi$ de la logique du premier ordre, il existe une formule $\varphi_S$ en forme normale de Skolem qui est équisatisfiable avec $\varphi$.
Une formule est en forme normale de Skolem si elle est en forme prénexe et ne contient que des quantificateurs universels ($\forall$).
Démonstration (par construction)
La démonstration est constructive : elle décrit un algorithme, appelé skolémisation, qui transforme une formule en sa forme de Skolem.
Étape 1 : Conversion en Forme Prénexe
On commence par transformer la formule $\varphi$ en une formule logiquement équivalente $\varphi’$ en forme prénexe.
Étape 2 : Élimination des Quantificateurs Existentiels (Skolémisation)
On parcourt les quantificateurs de $\varphi’$ de gauche à droite. Chaque fois que l’on rencontre un quantificateur existentiel $\exists$, on l’élimine de la manière suivante :
-
Cas 1 : Le $\exists$ n’est précédé d’aucun $\forall$.
Si la formule est de la forme $\exists y, \psi(y, \dots)$, on introduit un nouveau symbole de constante $c$ (une « constante de Skolem ») qui n’apparaît nulle part ailleurs. On remplace la formule par $\psi(c, \dots)$.
Intuition : Si la formule originale est vraie, c’est qu’il existe un objet ayant la propriété $\psi$. On donne simplement un nom, $c$, à cet objet. -
Cas 2 : Le $\exists$ est précédé par des $\forall$.
Si la formule est de la forme $\forall x_1 \dots \forall x_k \exists y, \psi(x_1, \dots, x_k, y, \dots)$, la valeur de $y$ qui satisfait $\psi$ peut dépendre des valeurs de $x_1, \dots, x_k$. On introduit alors un nouveau symbole de fonction $f$ à $k$ arguments (une « fonction de Skolem »). On remplace la formule par : $$ \forall x_1 \dots \forall x_k, \psi(x_1, \dots, x_k, f(x_1, \dots, x_k), \dots) $$ Intuition : La fonction $f$ représente le choix d’un $y$ valide pour chaque combinaison de $x_1, \dots, x_k$. L’existence d’une telle fonction est garantie par l’Axiome du Choix.
On répète ce processus jusqu’à ce que tous les quantificateurs existentiels aient été éliminés. La formule résultante est la forme normale de Skolem $\varphi_S$.
Implications et Utilisation
Le principal intérêt de la skolémisation est en démonstration automatique de théorèmes.
- Principe de Réfutation : Pour prouver qu’un théorème $\psi$ découle d’une théorie $T$ (i.e., $T \models \psi$), la plupart des démonstrateurs automatiques tentent de prouver que $T \cup \{\neg\psi\}$ est insatisfiable (n’a aucun modèle).
- Conversion en Clauses : La skolémisation est l’étape clé pour transformer la formule $T \cup \{\neg\psi\}$ en un ensemble de formules sans quantificateurs (appelées clauses), qui peuvent ensuite être traitées par des algorithmes comme la résolution.
- Équisatisfiabilité : Le fait que la skolémisation préserve la satisfiabilité (et l’insatisfiabilité) est crucial. Si la forme skolemisée de $T \cup \{\neg\psi\}$ est insatisfiable, alors la formule originale l’était aussi, et le théorème est prouvé.