Probleme – Distributivité, dans les deux sens

1. Le sens direct. Posons $\Gamma =\{p\wedge (q\vee r)\}$, puis ${\Gamma }_q=\Gamma \cup \{q\}$ et ${\Gamma }_r=\Gamma \cup \{r\}$, et notons $C=(p\wedge q)\vee (p\wedge r)$. On note ${\pi }_X$ la dérivation $\frac{\frac{}{X⊢p\wedge (q\vee r)}\text{ax}}{X⊢p}{\wedge }_e^g$, valable pour tout contexte $X$ contenant $p\wedge (q\vee r)$.

$$\frac{\frac{\frac{}{\Gamma ⊢p\wedge (q\vee r)}\text{ax}}{\Gamma ⊢q\vee r}{\wedge }_e^d\frac{\frac{{\pi }_{{\Gamma }_q}\frac{}{{\Gamma }_q⊢q}\text{ax}}{{\Gamma }_q⊢p\wedge q}{\wedge }_i}{{\Gamma }_q⊢C}{\vee }_i^g\frac{\frac{{\pi }_{{\Gamma }_r}\frac{}{{\Gamma }_r⊢r}\text{ax}}{{\Gamma }_r⊢p\wedge r}{\wedge }_i}{{\Gamma }_r⊢C}{\vee }_i^d}{\Gamma ⊢C}{\vee }_e$$

Treize nœuds, vérifiés règle par règle. La structure est celle qu'on attend : le contexte contient une disjonction, donc on raisonne par cas ; dans chaque cas on reconstruit une conjonction et on l'injecte du bon côté.

2. La réciproque. Posons $\Delta =\{(p\wedge q)\vee (p\wedge r)\}$, ${\Delta }_1=\Delta \cup \{p\wedge q\}$, ${\Delta }_2=\Delta \cup \{p\wedge r\}$, et $D=p\wedge (q\vee r)$. On nomme les deux branches du raisonnement par cas :

$$\mathcal{U}=\frac{\frac{\frac{}{{\Delta }_1⊢p\wedge q}\text{ax}}{{\Delta }_1⊢p}{\wedge }_e^g\frac{\frac{\frac{}{{\Delta }_1⊢p\wedge q}\text{ax}}{{\Delta }_1⊢q}{\wedge }_e^d}{{\Delta }_1⊢q\vee r}{\vee }_i^g}{{\Delta }_1⊢D}{\wedge }_i$$

$$\mathcal{V}=\frac{\frac{\frac{}{{\Delta }_2⊢p\wedge r}\text{ax}}{{\Delta }_2⊢p}{\wedge }_e^g\frac{\frac{\frac{}{{\Delta }_2⊢p\wedge r}\text{ax}}{{\Delta }_2⊢r}{\wedge }_e^d}{{\Delta }_2⊢q\vee r}{\vee }_i^d}{{\Delta }_2⊢D}{\wedge }_i$$

et l'arbre se referme en un seul pas :

$$\frac{\frac{}{\Delta ⊢(p\wedge q)\vee (p\wedge r)}\text{ax}\mathcal{U}\mathcal{V}}{\Delta ⊢D}{\vee }_e$$

Quatorze nœuds, et la même charpente retournée : cette fois c'est le but qui est une conjonction, donc ${\wedge }_i$, et la disjonction est encore dans le contexte, donc encore ${\vee }_e$.

3. Le coût comparé. Avec trois variables propositionnelles, une table de vérité a $2^3=8$ lignes : elle est ici plus rapide à écrire que l'arbre. C'est le petit cas, et il ne prouve rien.

Si $p$, $q$ et $r$ désignent des formules à dix variables chacune, disjointes, la table en compte $2^{30}=1073741824$, soit un milliard de lignes. Et les deux arbres ci-dessus ne changent pas d'une ligne : ils ont toujours treize et quatorze nœuds. Les règles ne regardent jamais l'intérieur des formules — seulement leur connecteur principal.

Voilà, chiffrée, la première des deux raisons que le programme donne au chapitre : la vérification par table est de nature exponentielle, la preuve ne l'est pas. Elle ne l'est pas parce qu'elle est schématique — un arbre de preuve établit un schéma valable pour toutes les substitutions, là où la table énumère les cas d'une instance.