Forme prénexe

Un article de Wikipédia, l'encyclopédie libre.

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'.