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[modifier | modifier le code]

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[modifier | modifier le code]

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.

Articles connexes[modifier | modifier le code]