Problème — 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é.