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 ssi $G=Q_1 x_1 Q_2 x_2 ... Q_n x_n G^{\prime}$ avec $Q_i \in \{\forall, \exists\}$.

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

Pour mettre une formule logique en forme prénexe, on peut utiliser les règles suivantes:

1. $\lnot \forall x F \Rightarrow \exists x \lnot F$
2. $(\forall x F) \land G \Rightarrow \forall x (F \land G)$
3. $(\forall x F) \lor G \Rightarrow \forall x (F \lor G)$
4. $(\forall x F)\supset G \Rightarrow \exists x(F \supset G)$
5. $G \land (\forall x F) \Rightarrow \forall x (G \land F)$
6. $G \lor (\forall x F) \Rightarrow \forall x (G \lor F)$
7. $G \supset (\forall x F) \Rightarrow \forall x (G \supset F)$
8. $\lnot \exists x F \Rightarrow \forall x \lnot F$
9. $(\exists x F) \land G \Rightarrow \exists x (F \land G)$
10. $(\exists x F) \lor G \Rightarrow \exists x (F \lor G)$
11. $(\exists x F)\supset G \Rightarrow \forall x(F \supset G)$
12. $G \land (\exists x F) \Rightarrow \exists x (G \land F)$
13. $G \lor (\exists x F) \Rightarrow \exists x (G \lor F)$
14. $G \supset (\exists x F) \Rightarrow \exists x (G \supset F)$

La variable x ne doit avoir aucune occurrence libre dans G (voir Calcul des prédicats). Sinon, utiliser un renommage de x en x'.

Ce document provient de « Forme pr%C3%A9nexe ».