Aller au contenu
Topos Uranos
Français

Conséquence et équivalence sémantiques

Résumé

Cette leçon passe de la valeur de vérité d’une formule aux relations entre formules. Elle définit la conséquence sémantique à partir d’un ensemble de prémisses, fini ou infini, et précise les lectures du signe de la conséquence, y compris celle de sa négation, qui dit que quelque chose n’est pas valide et non qu’il est contradictoire. Elle utilise les valeurs des connecteurs écrites comme des polynômes, ce qui transforme la vérification d’une loi en un calcul, et démontre les propriétés structurelles de la conséquence (réflexivité, monotonie, coupure et transitivité), le théorème de déduction sémantique et la réduction de la conséquence à l’insatisfaisabilité, sur laquelle s’appuiera la méthode de résolution. Elle définit ensuite l’équivalence sémantique, prouve que c’est une relation d’équivalence qui coïncide avec la conséquence mutuelle et avec la validité de la double implication, et démontre par induction sur la complexité les deux théorèmes qui permettent de travailler avec elle : le remplacement d’une occurrence d’une sous-formule par une autre équivalente et la substitution uniforme de formules aux variables. Avec eux, elle établit le catalogue des lois avec leurs noms corrects et simplifie des formules par des chaînes d’équivalences, sans tables de vérité.

Objectifs d’apprentissage

  1. Décider si une formule est conséquence sémantique d’un ensemble de formules, fini ou infini, en exhibant une valuation qui la falsifie ou en démontrant qu’il n’en existe pas.
  2. Démontrer et appliquer les propriétés de la conséquence, le théorème de déduction sémantique et la réduction de la conséquence à l’insatisfaisabilité.
  3. Établir des équivalences sémantiques par des tables de vérité, par le calcul avec les valeurs et par des chaînes d’équivalences, en nommant correctement chaque loi.
  4. Démontrer par induction sur la complexité le théorème de remplacement sémantique et celui de substitution uniforme, et distinguer quand s’applique chacun d’eux.

Ce que l’on utilise de la leçon précédente

La leçon sur la sémantique de la logique propositionnelle a donné un sens aux formules, et cette leçon le tient pour acquis. Une valuation est une fonction v ⁣:V→{0,1}v\colon V \to \{0, 1\}, qui attribue à chaque variable une valeur de vérité, 11 (vrai) ou 00 (faux). Par le théorème de définition par récurrence sur les formules, de la leçon sur l’induction, chaque valuation se prolonge d’une manière unique à toutes les formules au moyen de la clause de la négation conjointe, la seule nécessaire, parce que la langue n’a qu’un seul connecteur :

v((φ↓ψ))=1  ⇔  v(φ)=0,    v(ψ)=0v((\varphi \downarrow \psi)) = 1 \;\Leftrightarrow\; v(\varphi) = 0, \;\; v(\psi) = 0

Par l’unicité du prolongement, on écrit v(φ)v(\varphi) aussi pour la valeur du prolongement ; la lettre vv sans indice désigne toujours une valuation (et v′v', ww, uu, d’autres), tandis que les variables portent toujours leur indice. Comme dans la leçon sur la formalisation, pp, qq, rr, ss et tt nomment les variables v1v_1 à v5v_5, et V(φ)V(\varphi) est l’ensemble des variables de φ\varphi. On dit que vv satisfait φ\varphi, et on écrit v⊨φv \models \varphi, lorsque v(φ)=1v(\varphi) = 1, et qu’elle la falsifie, v⊭φv \not\models \varphi, lorsque v(φ)=0v(\varphi) = 0. Une formule est valide (ou tautologie), et on écrit ⊨φ\models \varphi, si toute valuation la satisfait ; satisfaisable, si une valuation au moins la satisfait ; insatisfaisable (ou antilogie), si aucune ne la satisfait ; contingente, si elle est satisfaisable sans être valide. Une valuation satisfait un ensemble Γ\Gamma de formules, v⊨Γv \models \Gamma, lorsqu’elle satisfait chacune d’elles, et Γ\Gamma est satisfaisable si une valuation au moins le satisfait, et insatisfaisable dans le cas contraire. Enfin, ⊤:=(v1→v1)\top := (v_1 \rightarrow v_1) et ⊥:=¬⊤\bot := \neg\top, de sorte que v(⊤)=1v(\top) = 1 et v(⊥)=0v(\bot) = 0 pour toute valuation.

De cette leçon, on utilise en outre deux résultats. Le premier est le lemme de coïncidence : si deux valuations coïncident sur les variables de φ\varphi, elles coïncident sur φ\varphi ; par lui, la valeur d’une formule à nn variables ne dépend que de 2n2^{n} combinaisons, et sa table de vérité est finie. Le second est le théorème des valeurs des connecteurs dérivés, qui calcule à partir des abréviations officielles la valeur de chaque connecteur comme un polynôme en les valeurs des composantes. Si a=v(φ)a = v(\varphi) et b=v(ψ)b = v(\psi) :

v(¬φ)=1−a,v((φ∨ψ))=a+b−ab,v((φ∧ψ))=abv(\neg\varphi) = 1 - a, \qquad v((\varphi \vee \psi)) = a + b - ab, \qquad v((\varphi \wedge \psi)) = ab
v((φ→ψ))=1−a(1−b),v((φ↔ψ))=ab+(1−a)(1−b),v((φ⊻ψ))=a+b−2abv((\varphi \rightarrow \psi)) = 1 - a(1 - b), \qquad v((\varphi \leftrightarrow \psi)) = ab + (1 - a)(1 - b), \qquad v((\varphi \veebar \psi)) = a + b - 2ab

Les démonstrations de cette leçon consistent, presque toutes, à comparer des valeurs de vérité, et ces polynômes permettent de le faire par un calcul au lieu d’un parcours de cas. Leur seule règle supplémentaire est que 00 et 11 sont les seuls nombres qui coïncident avec leur carré : si xx vaut 00 ou 11, alors x2=xx^{2} = x et x(1−x)=0x(1 - x) = 0. Il convient d’avoir en outre sous la main trois autres écritures des mêmes valeurs, que l’on obtient en développant les produits :

v((φ↓ψ))=(1−a)(1−b),v((φ∨ψ))=1−(1−a)(1−b),v((φ↔ψ))=1−a−b+2abv((\varphi \downarrow \psi)) = (1 - a)(1 - b), \qquad v((\varphi \vee \psi)) = 1 - (1 - a)(1 - b), \qquad v((\varphi \leftrightarrow \psi)) = 1 - a - b + 2ab

La première est la clause de la négation conjointe (le produit de 1−a1 - a et 1−b1 - b vaut 11 exactement lorsque a=b=0a = b = 0) ; la deuxième dit que la disjonction vaut 00 seulement si les deux composantes valent 00 ; la troisième, que la double implication vaut 11 si a=ba = b (car 1−2a+2a2=11 - 2a + 2a^{2} = 1) et 00 si a≠ba \neq b (car alors a+b=1a + b = 1 et ab=0ab = 0).