Prénexe (forme)

Imaginez une phrase logique qui répète « pour tout » et « il existe » au milieu de plusieurs propriétés. La mettre en forme prénexe revient à ranger toutes ces annonces au début, dans un ordre précis. Le reste de la phrase ne contient alors plus aucun quantificateur.

Ce rangement ne change pas ce que la formule affirme. Il rend seulement sa structure plus visible : d'abord les objets dont on parle, puis les relations qui doivent être vraies entre eux. L'ordre des annonces compte et ne peut pas être modifié librement.

Dans une formule du calcul des prédicats, un quantificateur universel affirme qu'une propriété vaut pour tout objet, tandis qu'un quantificateur existentiel affirme qu'au moins un objet convient. Une formule est en forme prénexe lorsque tous ces quantificateurs forment un préfixe placé avant une matrice qui n'en contient aucun. Si les variables liées successives sont notées x₁, …, x_n, cette structure s'écrit :

Chaque symbole Q_i est soit « pour tout », soit « il existe », et M désigne la matrice sans quantificateur. La transformation commence habituellement par éliminer les connecteurs définis à partir d'autres, puis pousse les négations jusqu'aux formules atomiques. Les variables liées sont renommées si nécessaire. Un quantificateur peut ensuite franchir un connecteur seulement si sa variable n'est pas libre dans l'autre membre.

La formule obtenue est logiquement équivalente à la formule de départ dans le cadre usuel de la logique du premier ordre à domaine non vide. La forme prénexe n'est généralement pas unique : des renommages de variables liées et certains ordres de quantificateurs de même nature donnent d'autres écritures équivalentes. En revanche, échanger librement un quantificateur universel et un quantificateur existentiel peut changer le sens.

Considérons deux prédicats : P(x) exprime une propriété de l'objet x, et R(x, y) une relation entre les objets x et y. La formule de départ nie qu'il existe un objet x possédant P et relié par R à tout objet y :

1. On fait franchir le quantificateur existentiel à la négation : il devient universel.

2. La négation de la conjonction devient une disjonction. La négation du quantificateur universel portant sur y devient existentielle. On obtient : $\mathrm{\forall }x(\mathrm{\neg }P(x)\vee \mathrm{\exists }y\mathrm{\neg }R(x,y))\backslash forall\; x\backslash ,\backslash bigl(\backslash neg\; P(x)\backslash lor\backslash exists\; y\backslash ,\backslash neg\; R(x,y)\backslash bigr)$

3. La variable y n'est pas libre dans ¬P(x). Son quantificateur peut donc passer devant la disjonction sans capturer de variable.

Le résultat est la forme prénexe suivante :

Le contrôle est direct : le préfixe contient les deux quantificateurs, tandis que la matrice entre parenthèses n'en contient plus. Les trois écritures successives restent équivalentes dans un domaine non vide.

Pour vérifier qu'une formule est déjà prénexe, on lit d'abord son début. Tous les quantificateurs doivent s'y suivre, et aucun ne doit réapparaître dans la matrice. Si l'un d'eux reste à l'intérieur, une remontée est encore nécessaire.

Lors d'une transformation, on renomme d'abord les variables liées qui pourraient se rencontrer. Ce geste évite qu'un quantificateur déplacé ne capture une variable qui était libre. On vérifie ensuite, connecteur par connecteur, que la variable remontée n'est pas libre dans l'autre membre.

En démonstration automatique, la forme prénexe expose immédiatement la succession des choix universels et existentiels. Si le but est plutôt de simplifier les connecteurs sans déplacer les quantificateurs, une forme normale portant seulement sur les négations répond mieux à ce besoin.

Forme normale négative. Après élimination des implications et des biconditionnelles, elle ne contient plus que les connecteurs ¬, ∧ et ∨, et exige que les négations portent directement sur des formules atomiques. Elle peut laisser des quantificateurs à l'intérieur de la formule. Une formule dont les négations sont bien placées sans que ses quantificateurs soient tous en tête n'est donc pas prénexe.

Forme normale de Skolem. La skolémisation élimine des quantificateurs existentiels à l'aide de nouveaux symboles de fonction ou de constante. Elle préserve la possibilité de trouver un modèle, mais pas, en général, l'équivalence formule par formule. Une simple remontée des quantificateurs, elle, produit une formule équivalente.

Forme normale conjonctive. Elle organise les connecteurs de la partie propositionnelle en conjonction de disjonctions. Le test porte sur l'organisation de la matrice, non sur la position des quantificateurs ; une formule peut satisfaire l'une de ces formes sans satisfaire l'autre.

Capture de variable. Déplacer un quantificateur alors que sa variable est libre dans l'autre membre modifie les liaisons. Le symptôme est qu'une occurrence auparavant libre se retrouve sous la portée du quantificateur. Il faut renommer la variable liée avant le déplacement seulement si elle risque de capturer une occurrence libre ou d'entrer en collision avec une autre variable ; sinon, aucun renommage préalable n'est nécessaire.

Ordre des quantificateurs. Deux quantificateurs de même nature peuvent permuter, mais un universel et un existentiel ne s'échangent pas en général. Le test consiste à lire leur dépendance : « pour chaque x, il existe un y » n'impose pas qu'un même y convienne à tous les x.

Domaine vide. Certaines règles de remontée utilisées sans précaution supposent le cadre standard où le domaine contient au moins un objet. Si une sémantique autorise un domaine vide, il faut contrôler séparément chaque équivalence au lieu d'appliquer mécaniquement la procédure habituelle.

Écriture non unique. Deux préfixes différents peuvent décrire des formes prénexes équivalentes. Le symptôme d'une fausse erreur est un simple changement de noms de variables liées ou la permutation de quantificateurs indépendants de même nature. Il faut comparer les portées et la matrice, pas seulement l'écriture.

La forme prénexe sépare deux informations : le préfixe décrit l'alternance des choix universels et existentiels, tandis que la matrice rassemble les contraintes sans quantificateur. Cette séparation facilite l'étude de la complexité logique et prépare certaines procédures de démonstration automatique. Le nombre d'alternances dans le préfixe devient alors un trait structurel à examiner, sans se réduire au simple nombre total de quantificateurs.