La règle qui manque

Sémantiquement, oui, et la table a deux lignes : si $v(p)=V$ alors $\neg \neg p$ et $p$ sont vraies ; si $v(p)=F$ alors $\neg \neg p$ est fausse et l'implication à vérifier est vide. Donc $\neg \neg p\models p$.

Avec les règles du chapitre, la montée échoue. Le but $p$ est atomique : aucune règle d'introduction ne s'applique, il faut donc éliminer. Le contexte ne contient que $\neg \neg p$, et les règles d'élimination de la négation donnent :

• ${\neg }_e$ : de $\neg \neg p$ et de $\neg p$ on tire $\perp$ — mais il faudrait déjà disposer de $\neg p$ ;
• ${\perp }_e$ : de $\perp$ on tire $p$ — mais il faudrait déjà disposer de $\perp$.

On peut obtenir $\Sigma ⊢\perp$ avec $\Sigma =\{\neg \neg p,\neg p\}$, ce qui donne, par ${\neg }_i$, le séquent $\neg \neg p⊢\neg \neg p$ : on tourne en rond. Il manque le pas qui transforme « supposer $\neg p$ mène à l'absurde » en « donc $p$ ».

La règle absente porte plusieurs noms — absurde classique, reductio ad absurdum, élimination de la double négation :

$$\frac{\Gamma ,\neg A⊢\perp }{\Gamma ⊢A}\text{absurde}\text{aˋ comparer aˋ}\frac{\Gamma ,A⊢\perp }{\Gamma ⊢\neg A}{\neg }_i$$

Les deux se ressemblent au point qu'on les confond, et le cours nomme d'ailleurs ${\neg }_i$ « le raisonnement par l'absurde ». Ce ne sont pourtant pas les mêmes. ${\neg }_i$ réfute : elle établit une négation, et un raisonnement direct suffit à la justifier. La règle absurde affirme : elle établit une formule positive à partir d'une réfutation de sa négation, et c'est un pas de plus.

Ce que cela change. Les huit règles du chapitre, prises seules, forment la déduction naturelle dite intuitionniste. Avec elles, on démontre déjà beaucoup : le modus ponens, barbara, la curryfication, la contraposée dans un sens, trois des quatre lois de De Morgan. On ne démontre pas $\neg \neg p\to p$, ni le tiers exclu $p\vee \neg p$, ni la loi de Peirce. Ajouter la règle absurde rend le système classique, c'est-à-dire complet pour les tables de vérité.

Le fait que ces séquents ne soient pas démontrables sans elle est un théorème, et il n'est pas au programme : ce que l'exercice établit, c'est que la recherche naturelle échoue, et que le système gagne quelque chose en acceptant la neuvième règle. Un curieux notera qu'on démontre en revanche $⊢\neg \neg (p\vee \neg p)$ avec les seules huit règles — le tiers exclu n'est pas réfutable, il est seulement indémontrable.