Previous Next Contents

2  Sémantique

Nous voulons que FÙF' soit vraie exactement quand F et F' sont toutes les deux vraies. Ce disant, nous avons tenté de préciser la signification des formules, et c'est le rôle de la sémantique. C'est ici essentiellement que la logique classique diffère des autres.

En logique propositionnelle classique, chaque formule est censée être soit vraie soit fausse. Formellement, l'ensemble des valeurs de vérité est l'ensemble B={T,F} des booléens, où T¹F. La signification des connecteurs est définie à l'aide de fonctions des booléens vers les booléens. Ces fonctions sont représentées par des tables de vérité. Les voici pour les connecteurs fondamentaux :
Ù F T
F F F
T F T
Ú F T
F F T
T T T
¬  
F T
T F
Þ F T
F T T
T F T

Par exemple, si F est supposé vraie (T), et F' est supposé fausse (F), alors FÞF' doit être faux. (Le premier argument est en colonne, le second en ligne dans les tables de vérité.) Ceci définit des fonctions binaires et , ou et imp de B×B vers B, et une fonction unaire non de B vers B.

La signification d'une formule F dépend des valeurs de vérité supposées des variables, et nous définissons formellement :


Définition 7  Une affectation or interprétation r est une application de l'ensemble X des variables propositionnelles vers B.

La sémantique [F]r d'une formule F dans l'affectation r est définie par récurrence structurelle sur F par :


Nous dirons qu'une formule F est vraie dans l'affectation r si et seulement si [F]r=T, and est fausse dans r si et seulement si [F]r=F.


Définition 8  Soit F une formule propositionnelle, et r une affectation.

Nous disons que r est un modèle de F, ou que r satisfait F, et nous écrivons r|=F, si et seulement si [F]r=T.

Nous disons qu'un ensemble G de formules entraîne F, et nous écrivons G|=F, si et seulement si toutes les affectations satisfaisant toutes les formules de G en même temps (les modèles de G) sont aussi des modèles de F, c'est-à-dire quand r|=Y pour tout YÎ G implique r|=F.

F est valide si et seulement si F est vraie dans toute affectation ([F]r=T pour tout r, noté |=F), et est invalide sinon. Une formule propositionnelle valide est aussi appelée une tautologie.

F est satisfiable si et seulement si elle est vraie dans au moins une affectation ([F]r=T pour un certain r, i.e., elle a un modèle), et est insatisfiable sinon.


Toutes les formules valides sont satisfiables, et toutes les formules insatisfiables sont invalides. Ceci divise l'espace des formules en trois catégories : les valides (toujours vraies), les insatisfiables (toujours fausses), et les formules à la fois invalides et satisfiables (parfois vraies, parfois fausses). Ceci est illustré comme suit :

Valide
|
Invalide et satisfiable
|
Insatisfiable

Ensuite, la validité et l'insatisfiabilité se correspondent via négation : F est valide si et seulement si ¬F est insatisfiable, F est insatisfiable si et seulement si ¬F est valide. Donc la négation non envoie le diagramme ci-dessus au même, mais retourné. Observer que le point ``invalide et satisfiable'' reste à la même place.

En un sens, les affectations (au niveau sémantique) jouent le même rôle que les substitutions (au niveau syntaxique) :


Théorème 9   Pour toute substitution s et toute affectation r, soit sr l'affectation qui envoie toute variable A vers [s(A)]r.

Pour toute formule F, pour toute substitution s et toute affectation r, [Fs]r = [F](sr).
Preuve : Par récurrence structurelle sur F : laissé en exercice. ¤


Corollaire 10   Soit F une formule propositionnelle. Si F est valide (resp. insatisfiable), alors Fs est valide (resp. insatisfiable) pour toute substitution s.




Previous Next Contents