Commuter une conjonction

Posons $\Gamma =\{p\wedge q\}$.

$$\frac{\frac{\frac{}{\Gamma ⊢p\wedge q}\text{ax}}{\Gamma ⊢q}{\wedge }_e^d\frac{\frac{}{\Gamma ⊢p\wedge q}\text{ax}}{\Gamma ⊢p}{\wedge }_e^g}{\Gamma ⊢q\wedge p}{\wedge }_i$$

La méthode se lit dans l'arbre. Le but $q\wedge p$ est une conjonction : sa forme désigne ${\wedge }_i$, qui demande deux prémisses, $\Gamma ⊢q$ et $\Gamma ⊢p$. Chacune est atomique, donc chacune s'obtient par élimination — ici ${\wedge }_e$ appliquée à l'hypothèse, du côté voulu.

Cinq nœuds, et surtout : on n'a jamais eu à choisir. Chaque étape était forcée par la forme du but ou du contexte. C'est ce que la méthode du cours appelle « déterministe presque partout », et c'est ce qui rend ces preuves courtes.

Attention à l'ordre des prémisses de ${\wedge }_i$. La règle conclut $A\wedge B$ de $\Gamma ⊢A$ et $\Gamma ⊢B$, dans cet ordre. Le but étant ici $q\wedge p$, la prémisse gauche doit établir $q$ — donc appliquer ${\wedge }_e^d$, l'élimination droite, à l'hypothèse $p\wedge q$. C'est le croisement qu'on écrit à l'envers une fois sur deux.