La contraposée

Posons $\Gamma =\{p\to q\}$, puis ${\Gamma }_1=\Gamma \cup \{\neg q\}$ et ${\Gamma }_2={\Gamma }_1\cup \{p\}$.

$$\frac{\frac{\frac{\frac{}{{\Gamma }_2⊢\neg q}\text{ax}\frac{\frac{}{{\Gamma }_2⊢p\to q}\text{ax}\frac{}{{\Gamma }_2⊢p}\text{ax}}{{\Gamma }_2⊢q}{\to }_e}{{\Gamma }_2⊢\perp }{\neg }_e}{{\Gamma }_1⊢\neg p}{\neg }_i}{\Gamma ⊢\neg q\to \neg p}{\to }_i$$

La lecture de bas en haut. Le but $\neg q\to \neg p$ est une implication : ${\to }_i$ décharge $\neg q$. Le nouveau but $\neg p$ est une négation : ${\neg }_i$ décharge $p$ et demande $\perp$. Pour obtenir $\perp$, il faut une formule et sa négation : le contexte offre $\neg q$, il reste donc à établir $q$, ce que $p\to q$ et $p$ donnent par ${\to }_e$. Sept nœuds, et aucun choix.

Ce que la preuve emploie, et ce qu'elle n'emploie pas. Elle n'utilise que ${\to }_i$, ${\to }_e$, ${\neg }_i$, ${\neg }_e$ et l'axiome — pas de raisonnement par l'absurde classique. C'est important pour la suite : la contraposée dans ce sens-ci est démontrable avec les seules règles du chapitre.

Le sens réciproque, lui, ne l'est pas. Le séquent $\neg q\to \neg p⊢p\to q$ est pourtant une conséquence sémantique — la table de vérité le confirme sur ses quatre lignes. On essaie : ${\to }_i$ décharge $p$, le but devient $q$, atomique ; on cherche dans le contexte de quoi produire $q$, et l'on ne trouve que $\neg q\to \neg p$, qui produit $\neg p$ à condition d'avoir $\neg q$… que l'on n'a pas. La montée s'arrête. C'est le sujet de l'exercice 28.9, et il n'y manque qu'une règle.