Conséquence logique, implication, et ex falso

1. Les deux énoncés disent la même chose, mot pour mot.

• $\phi \models \psi$ signifie : pour toute valuation $v$, si $[[\phi ]{]}_v=V$ alors $[[\psi ]{]}_v=V$.
• $\models \phi \to \psi$ signifie : pour toute valuation $v$, $[[\phi \to \psi ]{]}_v=V$, c'est-à-dire $[[\phi ]{]}_v=F$ ou $[[\psi ]{]}_v=V$.

Or « si $A$ alors $B$ » et « non-$A$ ou $B$ » sont la même assertion — c'est la décomposition de l'implication, appliquée cette fois au méta-niveau. D'où l'équivalence.

C'est le résultat le plus utile du chapitre, parce qu'il fait passer d'une notion sur les ensembles de modèles ($\models$ à gauche) à une notion sur une formule ($\models$ tout court). Combiné à la proposition du cours — $\phi$ tautologique $⟺$ $\neg \phi$ insatisfiable —, il ramène toute question de conséquence logique à sat : tester $\phi \models \psi$, c'est tester que $\phi \wedge \neg \psi$ n'a pas de modèle. Trois notions, un seul algorithme.

2. Les deux premières sont vraies, les deux dernières fausses — vérifié sur les quatre valuations.

• $p\models p\vee q$ : ajouter une disjonction affaiblit, donc conserve la vérité.
• $p\wedge q\models p$ : retirer un facteur d'une conjonction affaiblit aussi.
• $p/\models p\wedge q$ : contre-modèle $p=V$, $q=F$. On ne tire pas $q$ de rien.
• $p\vee q/\models p$ : contre-modèle $p=F$, $q=V$. Savoir que l'un des deux est vrai ne dit pas lequel — et c'est toute la difficulté de la disjonction, en logique comme dans un programme.

3. C'est vrai, pour n'importe quelle $\psi$, et la vérification est immédiate : $p\wedge \neg p$ n'a aucun modèle, donc l'assertion « tout modèle de $p\wedge \neg p$ est modèle de $q$ » porte sur l'ensemble vide et est vraie sans rien à démontrer. C'est le principe dit ex falso quodlibet : d'une contradiction, tout se déduit.

Ce que cela coûte en pratique. Une base de données de faits qui contient une contradiction devient inutilisable : tout s'en déduit, y compris ce qui est faux. Et un système de contraintes insatisfiable ne rend pas « presque une solution », il rend n'importe quoi. C'est pourquoi un solveur commence toujours par la question de la satisfiabilité, et non par celle de la conséquence.