Probleme – La correction, les règles qui restent

On raisonne par induction sur la dérivation, et l'on montre à chaque règle : si les prémisses sont sémantiquement correctes, la conclusion l'est. « $\Gamma \models C$ » signifie : toute valuation $v$ qui satisfait toutes les formules de $\Gamma$ satisfait $C$.

1. Les quatre règles simples.

${\wedge }_e^g$. Soit $v$ un modèle de $\Gamma$. Par hypothèse d'induction, $v$ satisfait $A\wedge B$ ; la table de $\wedge$ impose alors que $v$ satisfasse $A$.

${\vee }_i^g$. Soit $v$ un modèle de $\Gamma$. Par hypothèse d'induction $v$ satisfait $A$ ; la table de $\vee$ donne alors $A\vee B$ vraie.

${\neg }_e$. Soit $v$ un modèle de $\Gamma$. Par hypothèse d'induction $v$ satisfait $\neg A$ et satisfait $A$ — ce qui est impossible. Il n'existe donc aucun modèle de $\Gamma$, et l'énoncé « tout modèle de $\Gamma$ satisfait $\perp$ » est vrai par vacuité.

${\perp }_e$. Même argument : par hypothèse d'induction tout modèle de $\Gamma$ satisfait $\perp$, or aucune valuation ne satisfait $\perp$ ; donc $\Gamma$ n'a pas de modèle, et $\Gamma \models C$ pour n'importe quel $C$.

Les deux dernières sont le même raisonnement, et c'est celui qu'on saute d'ordinaire : un contexte contradictoire n'a pas de modèle, donc il implique tout. C'est ici, et nulle part ailleurs, que « de l'absurde on tire tout » reçoit sa justification sémantique.

2. ${\vee }_e$. Soit $v$ un modèle de $\Gamma$. La première prémisse donne $v\models A\vee B$, donc $v$ satisfait $A$ ou satisfait $B$.

• Si $v\models A$ : alors $v$ est un modèle de $\Gamma \cup \{A\}$, et la deuxième prémisse donne $v\models C$.
• Si $v\models B$ : alors $v$ est un modèle de $\Gamma \cup \{B\}$, et la troisième donne $v\models C$.

Dans les deux cas $v\models C$. Le soin à prendre est de vérifier que $v$ est bien un modèle du contexte enrichi — ce qui suppose qu'il satisfaisait déjà $\Gamma$, et c'est le cas. C'est le même geste que dans ${\to }_i$.

3. ${\neg }_i$. Soit $v$ un modèle de $\Gamma$. Deux cas.

• Si $v/\models A$ : alors $v\models \neg A$, ce qu'on voulait.
• Si $v\models A$ : alors $v$ est un modèle de $\Gamma \cup \{A\}$, et la prémisse donne $v\models \perp$ — impossible. Ce cas ne se produit donc jamais.

Dans tous les cas possibles, $v\models \neg A$.

Le théorème est donc établi : si $\Gamma ⊢C$ alors $\Gamma \models C$, et la démonstration tient en une page parce qu'un arbre de preuve est un type inductif — chapitre chap:induction — sur lequel on raisonne comme sur n'importe quel arbre.

4. Le procédé de réfutation, et sa limite. La contraposée donne : si $\Gamma /\models C$, alors $\Gamma /⊢C$. Une seule valuation suffit — c'est l'exercice 28.3.

Mais ce procédé ne s'applique pas à $⊢p\vee \neg p$, et c'est le point délicat. Ce séquent est une conséquence sémantique : $p\vee \neg p$ est une tautologie, aucune valuation ne la réfute. La correction ne dit donc rien contre lui, et pourtant il n'est pas démontrable avec les huit règles.

Ce qu'il faut en conclure. La correction est un outil de réfutation incomplet. Pour montrer qu'un séquent sémantiquement valide n'est pas démontrable dans un système donné, il faut une autre sémantique — une sémantique qui distingue exactement ce que ce système-là démontre. C'est ce que font les modèles de Kripke pour la logique intuitionniste, et c'est franchement hors programme. Ce que l'étudiant doit retenir est plus simple, et plus utile : la correction réfute les séquents faux, elle ne dit rien sur les séquents vrais mais indémontrables. Les deux moitiés du lien entre $⊢$ et $\models$ ne sont pas symétriques, et seule la première est au programme.