Forme prénexe

Une formule de la logique du premier ordre est en forme prénexe si tous ses quantificateurs (${\displaystyle \forall }$ et ${\displaystyle \exists }$) apparaissent à gauche dans cette formule. C’est-à-dire, G est en forme prénexe si et seulement si ${\displaystyle G=Q_{1}x_{1}Q_{2}x_{2}...Q_{n}x_{n}G^{\prime }}$ avec ${\displaystyle Q_{i}\in \{\forall ,\exists \}}$ et ${\displaystyle 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 ${\displaystyle Gauche\Rightarrow Droite}$ entre formules équivalentes :

#	Forme initiale	Forme prénexe
1	${\displaystyle \lnot \forall xF}$	${\displaystyle \exists x\lnot F}$
2	${\displaystyle (\forall xF)\land G}$	${\displaystyle \forall x(F\land G)}$
3	${\displaystyle (\forall xF)\lor G}$	${\displaystyle \forall x(F\lor G)}$
4	${\displaystyle (\forall xF)\rightarrow G}$	${\displaystyle \exists x(F\rightarrow G)}$
5	${\displaystyle G\land (\forall xF)}$	${\displaystyle \forall x(G\land F)}$
6	${\displaystyle G\lor (\forall xF)}$	${\displaystyle \forall x(G\lor F)}$
7	${\displaystyle G\rightarrow (\forall xF)}$	${\displaystyle \forall x(G\rightarrow F)}$
8	${\displaystyle \lnot \exists xF}$	${\displaystyle \forall x\lnot F}$
9	${\displaystyle (\exists xF)\land G}$	${\displaystyle \exists x(F\land G)}$
10	${\displaystyle (\exists xF)\lor G}$	${\displaystyle \exists x(F\lor G)}$
11	${\displaystyle (\exists xF)\rightarrow G}$	${\displaystyle \forall x(F\rightarrow G)}$
12	${\displaystyle G\land (\exists xF)}$	${\displaystyle \exists x(G\land F)}$
13	${\displaystyle G\lor (\exists xF)}$	${\displaystyle \exists x(G\lor F)}$
14	${\displaystyle G\rightarrow (\exists xF)}$	${\displaystyle \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 ${\displaystyle \leftrightarrow }$ mais ces règles suffisent car ${\displaystyle \{\lnot ,\land ,\lor ,\rightarrow \}}$ est un système complet de connecteurs. Pour transformer une formule, on peut donc appliquer cette démarche :

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

Articles connexes

• Élimination des quantificateurs
• Théorème de Herbrand
• Calcul des prédicats
• Skolémisation
• Théorie des modèles
• Modèle