Forme prénexe

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

Une formule de la logique du premier ordre est en forme prénexe si tous ses quantificateurs ( et ) apparaissent à gauche dans cette formule. C’est-à-dire, G est en forme prénexe si et seulement si avec et 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 entre formules équivalentes :

# Forme initiale Forme prénexe
1
2
3
4
5
6
7
8
9
10
11
12
13
14

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 mais ces règles suffisent car 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[modifier | modifier le code]