Une hypothèse qui ne sert pas

$$\frac{\frac{\frac{}{p,q⊢p}\text{ax}}{p⊢q\to p}{\to }_i}{⊢p\to (q\to p)}{\to }_i$$

Trois nœuds, et deux décharges. Le but est une implication : ${\to }_i$, qui déplace $p$ à gauche du $⊢$. Le nouveau but $q\to p$ est encore une implication : ${\to }_i$ encore, qui déplace $q$. Le but devient $p$, présent dans le contexte : axiome.

L'hypothèse $q$ ne sert à rien, et c'est légitime. La règle ${\to }_i$ ne demande pas que $A$ soit utilisée dans la preuve de $B$, seulement qu'elle soit disponible. Autrement dit, le contexte est un ensemble d'hypothèses permises, non requises. C'est ce qu'on appelle l'affaiblissement, et c'est ce qui rend l'implication de la logique classique « matérielle » : $q\to p$ est vraie dès que $p$ est vraie, quel que soit le rapport entre $q$ et $p$.

Ce que cela contredit dans le langage courant. « Si $2+2=5$, alors la Terre est ronde » est une implication vraie, et le lecteur la trouve absurde parce qu'il attend un lien de cause à effet. Le connecteur $\to$ n'en exprime aucun. Des logiques dites pertinentes refusent précisément l'affaiblissement pour retrouver ce lien, au prix de règles beaucoup plus lourdes — elles sont hors programme, mais savoir que ce choix existe éclaire celui qui a été fait ici.