title: Forme prénexe
text: # 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.
  