Forme prénexe
# Forme prénexe

Une formule de la logique du premier ordre est en forme prénexe si tous ses quantificateurs ($\forall$ et $\exists$) apparaissent à gauche dans cette formule. C’est-à-dire, G est en forme prénexe si et seulement si $G=Q_{1}x_{1}Q_{2}x_{2}...Q_{n}x_{n}G^{\prime }$ avec $Q_{i}\in \{\forall ,\exists \}$ et $G^{\prime }$ une formule sans quantificateurs.

Toutes les formules du premier ordre sont logiquement équivalentes à une formule en forme prénexe.

La complexité d'une formule de logique mise en forme prénexe se mesure à son premier quantificateur et au nombre d'alternance de blocs de quantificateurs universels ou existentiels qui le suivent et précèdent la formule sans quantificateur.

## Règles de transformations

Pour mettre une formule logique en forme prénexe, on peut utiliser les règles de transformation suivantes $Gauche\Rightarrow Droite$ entre formules équivalentes :

| # | Forme initiale | Forme prénexe |
| - | - | - |
| 1 | $\lnot \forall xF$ | $\exists x\lnot F$ |
| 2 | $(\forall xF)\land G$ | $\forall x(F\land G)$ |
| 3 | $(\forall xF)\lor G$ | $\forall x(F\lor G)$ |
| 4 | $(\forall xF)\rightarrow G$ | $\exists x(F\rightarrow G)$ |
| 5 | $G\land (\forall xF)$ | $\forall x(G\land F)$ |
| 6 | $G\lor (\forall xF)$ | $\forall x(G\lor F)$ |
| 7 | $G\rightarrow (\forall xF)$ | $\forall x(G\rightarrow F)$ |
| 8 | $\lnot \exists xF$ | $\forall x\lnot F$ |
| 9 | $(\exists xF)\land G$ | $\exists x(F\land G)$ |
| 10 | $(\exists xF)\lor G$ | $\exists x(F\lor G)$ |
| 11 | $(\exists xF)\rightarrow G$ | $\forall x(F\rightarrow G)$ |
| 12 | $G\land (\exists xF)$ | $\exists x(G\land F)$ |
| 13 | $G\lor (\exists xF)$ | $\exists x(G\lor F)$ |
| 14 | $G\rightarrow (\exists xF)$ | $\exists x(G\rightarrow F)$ |

La variable x ne doit avoir aucune occurrence libre dans G (voir Calcul des prédicats). Sinon renommer au préalable x par une variable nouvelle n'apparaissant pas librement dans les formules F et G.

## Remarques

Il n'y a pas de règles simples de transformation pour une formule comportant le connecteur $\leftrightarrow$ mais ces règles suffisent car $\{\lnot ,\land ,\lor ,\rightarrow \}$ est un système complet de connecteurs. Pour transformer une formule, on peut donc appliquer cette démarche :

* Supprimer les équivalences, en les remplaçant par des implications ;
* Transporter les négations devant les formules atomiques ;
* Transporter les quantificateurs en tête de la formule, en renommant les variables si nécessaire.
