Problème — De Morgan : trois lois, et la quatrième

1. Les quatre sont valides. Sur les quatre valuations de $\{p,q\}$, chacune des quatre implications est vraie ; c'est un calcul de seize lignes, vérifié par programme. Les quatre lois sont donc, sémantiquement, sur le même pied.

2. La première paire. Sens direct, avec $\Gamma =\{\neg (p\vee q)\}$ :

$$\mathcal{U}=\frac{\frac{}{\Gamma ,p⊢\neg (p\vee q)}\text{ax}\frac{\frac{}{\Gamma ,p⊢p}\text{ax}}{\Gamma ,p⊢p\vee q}{\vee }_i^g}{\Gamma ,p⊢\perp }{\neg }_e$$

$$\mathcal{V}=\frac{\frac{}{\Gamma ,q⊢\neg (p\vee q)}\text{ax}\frac{\frac{}{\Gamma ,q⊢q}\text{ax}}{\Gamma ,q⊢p\vee q}{\vee }_i^d}{\Gamma ,q⊢\perp }{\neg }_e$$

$$\frac{\frac{\mathcal{U}}{\Gamma ⊢\neg p}{\neg }_i\frac{\mathcal{V}}{\Gamma ⊢\neg q}{\neg }_i}{\Gamma ⊢\neg p\wedge \neg q}{\wedge }_i$$

Réciproque, avec $\Delta =\{\neg p\wedge \neg q\}$ et ${\Delta }_1=\Delta \cup \{p\vee q\}$ :

$$\mathcal{U}=\frac{\frac{\frac{}{{\Delta }_1,p⊢\neg p\wedge \neg q}\text{ax}}{{\Delta }_1,p⊢\neg p}{\wedge }_e^g\frac{}{{\Delta }_1,p⊢p}\text{ax}}{{\Delta }_1,p⊢\perp }{\neg }_e$$

$$\mathcal{V}=\frac{\frac{\frac{}{{\Delta }_1,q⊢\neg p\wedge \neg q}\text{ax}}{{\Delta }_1,q⊢\neg q}{\wedge }_e^d\frac{}{{\Delta }_1,q⊢q}\text{ax}}{{\Delta }_1,q⊢\perp }{\neg }_e$$

$$\frac{\frac{\frac{}{{\Delta }_1⊢p\vee q}\text{ax}\mathcal{U}\mathcal{V}}{{\Delta }_1⊢\perp }{\vee }_e}{\Delta ⊢\neg (p\vee q)}{\neg }_i$$

Onze nœuds chacune, vérifiées règle par règle.

3. La troisième loi, avec $\Sigma =\{\neg p\vee \neg q\}$ et ${\Sigma }_1=\Sigma \cup \{p\wedge q\}$ :

$$\mathcal{U}=\frac{\frac{}{{\Sigma }_1,\neg p⊢\neg p}\text{ax}\frac{\frac{}{{\Sigma }_1,\neg p⊢p\wedge q}\text{ax}}{{\Sigma }_1,\neg p⊢p}{\wedge }_e^g}{{\Sigma }_1,\neg p⊢\perp }{\neg }_e$$

$$\mathcal{V}=\frac{\frac{}{{\Sigma }_1,\neg q⊢\neg q}\text{ax}\frac{\frac{}{{\Sigma }_1,\neg q⊢p\wedge q}\text{ax}}{{\Sigma }_1,\neg q⊢q}{\wedge }_e^d}{{\Sigma }_1,\neg q⊢\perp }{\neg }_e$$

$$\frac{\frac{\frac{}{{\Sigma }_1⊢\neg p\vee \neg q}\text{ax}\mathcal{U}\mathcal{V}}{{\Sigma }_1⊢\perp }{\vee }_e}{\Sigma ⊢\neg (p\wedge q)}{\neg }_i$$

Le schéma est toujours le même : pour établir une négation, on suppose la formule et l'on vise $\perp$ ; pour se servir d'une disjonction du contexte, on raisonne par cas.

4. La quatrième résiste. Le but $\neg p\vee \neg q$ est une disjonction. Les seules règles d'introduction sont ${\vee }_i^g$ et ${\vee }_i^d$, qui exigent d'établir $\neg p$ ou $\neg q$ — c'est-à-dire de choisir un côté. Or l'hypothèse $\neg (p\wedge q)$ ne dit rien sur celui des deux qui est faux ; elle dit seulement qu'ils ne sont pas vrais tous les deux. La montée est bloquée avant même de commencer.

C'est la même impasse qu'à l'exercice 28.9, et c'est la même règle qui manque. Avec la règle absurde, la preuve existe : on suppose $\neg (\neg p\vee \neg q)$, on en tire successivement $\neg \neg p$ et $\neg \neg q$, donc $p$ et $q$ par élimination de la double négation, donc $p\wedge q$, ce qui contredit l'hypothèse.

Ce que ce problème met en évidence. Sémantiquement, les quatre lois sont indiscernables : quatre tables, quatre fois « valide ». Syntaxiquement, trois sont démontrables avec les huit règles du chapitre et la quatrième ne l'est pas. Il y a donc, entre $\models$ et $⊢$, un écart qui n'est pas une simple différence de méthode : c'est un écart de portée, et la table du cours qui oppose sémantique et syntaxe s'en trouve complétée d'une ligne. La combler demande la neuvième règle — et c'est cette règle-là, exactement, qui fait passer de la logique intuitionniste à la logique classique.