Conséquence logique, implication, et ex falso

Exercice · niveau 2 · informatique (MP2I/MPI), chapitre 20 — Logique propositionnelle

Énoncé

Montrer que $φ ⊨ ψ$ si et seulement si $⊨ φ \to ψ$ .
Déterminer, parmi les quatre assertions suivantes, celles qui sont vraies :

$p ⊨ p \lor q, p \land q ⊨ p, p ⊨ p \land q, p \lor q ⊨ p .$

Que vaut $p \land \neg p ⊨ q$ ?

Corrigé

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

$φ ⊨ ψ$ signifie : pour toute valuation $v$ , si $[[φ]]_{v} = V$ alors $[[ψ]]_{v} = V$ .
$⊨ φ \to ψ$ signifie : pour toute valuation $v$ , $[[φ \to ψ]]_{v} = V$ , c'est-à-dire $[[φ]]_{v} = F$ ou $[[ψ]]_{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 ( $⊨$ à gauche) à une notion sur une formule ( $⊨$ tout court). Combiné à la proposition du cours — $φ$ tautologique $⟺$ $\neg φ$ insatisfiable —, il ramène toute question de conséquence logique à sat : tester $φ ⊨ ψ$ , c'est tester que $φ \land \neg ψ$ 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 ⊨ p \lor q$ : ajouter une disjonction affaiblit, donc conserve la vérité.
$p \land q ⊨ p$ : retirer un facteur d'une conjonction affaiblit aussi.
$p \neq ⊨ p \land q$ : contre-modèle $p = V$ , $q = F$ . On ne tire pas $q$ de rien.
$p \lor q \neq ⊨ 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 $ψ$ , et la vérification est immédiate : $p \land \neg p$ n'a aucun modèle, donc l'assertion « tout modèle de $p \land \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.

Les autres exercices de ce chapitre Le cours du chapitre

Un blocage sur cet exercice ? Le tuteur d'Adloun guide par questions, sans donner la réponse.