Les techniques de la logique classique

Les règles à l’intérieur d’un contexte

Dans la leçon sur les systèmes déductifs formels a été fixé le système de Łukasiewicz : les schémas d’axiomes A1, A2 et A3, la règle du modus ponens (MP) et la notion de déduction à partir d’un ensemble $\Gamma$ de prémisses, avec ses premières propriétés : la réflexivité (Réfl : si $\varphi \in \Gamma$, alors $\Gamma \vdash \varphi$), la monotonie (Mon : si $\Gamma \subseteq \Delta$ et $\Gamma \vdash \varphi$, alors $\Delta \vdash \varphi$), la coupure (Coupure), le modus ponens entre déductions (si $\Gamma \vdash \varphi$ et $\Gamma \vdash (\varphi \rightarrow \psi)$, alors $\Gamma \vdash \psi$, que l’on cite aussi comme MP), le théorème de déduction (TD : si $\Gamma \cup \{\varphi\} \vdash \psi$, alors $\Gamma \vdash (\varphi \rightarrow \psi)$) et sa réciproque (RTD). Les leçons sur les quatre techniques de déduction et sur les symétries des connecteurs ont ajouté le syllogisme hypothétique (SH), l’échange des prémisses (EP), la double négation (DN), la contraposition (CP) sous ses trois formes, le remplacement des équivalents (Rempl), les symétries (Sym) et les formes équivalentes de la disjonction et de la conjonction. La première de ces leçons, après avoir démontré la double négation, a en outre complété le système du cours par une seconde règle primitive, le remplacement de la double négation (RDN) : si $\chi'$ résulte de $\chi$ par le remplacement d’une occurrence d’une sous-formule $\theta$ par $\neg\neg\theta$, ou d’une occurrence de $\neg\neg\theta$ par $\theta$, de $\chi$ on infère $\chi'$. Désormais, $\vdash$ se rapporte à ce système (A1 à A3, MP et RDN), dans lequel continuent de valoir la réflexivité, la monotonie, la coupure, le théorème de déduction et sa réciproque ; les techniques de cette leçon en sont des règles dérivées, bien qu’aucune de leurs démonstrations n’invoque RDN directement : la règle agit par l’intermédiaire des formes équivalentes et du remplacement des équivalents, que la leçon sur les symétries a démontrés avec elle.

Or, en mathématiques, personne ne raisonne sans prémisses : on raisonne à partir de certains axiomes, des hypothèses d’un théorème et de ce que l’on a supposé pour discuter un cas. S’il en est ainsi, une technique de raisonnement n’est utile que si elle est énoncée avec un ensemble $\Gamma$ de prémisses que l’on transporte de ligne en ligne. Il s’ensuit que chaque règle de cette leçon est énoncée et démontrée pour un $\Gamma$ quelconque ; le cas sans prémisses est le cas particulier $\Gamma = \emptyset$, et non l’inverse.

Les démonstrations sont des déductions sur les déductions : chaque ligne affirme que quelque chose est déductible à partir d’un ensemble, $\Gamma \vdash \varphi$, et sa justification renvoie à des lignes antérieures. Dans ces démonstrations, « Prémisse » marque les lignes que l’énoncé de la règle tient pour acquises, et le nom d’un axiome (A1, A3) ou d’un théorème déjà démontré (comme Id, le théorème $\vdash (\varphi \rightarrow \varphi)$) marque une ligne $\Gamma \vdash \varphi$ dans laquelle $\varphi$ est une instance de ce schéma ou de ce théorème, déductible à partir de n’importe quel ensemble.

La leçon sur quatre techniques de déduction a démontré, avec la monotonie et la coupure, le lemme « du résultat à la règle », qui rend possible cette manière de travailler : si $\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta$ et $\Gamma \vdash \alpha_{i}$ pour chaque $i$, alors $\Gamma \vdash \beta$. Avec $n = 1$, appliqué dans chaque sens d’une équivalence $\alpha \dashv\vdash \alpha'$, il dit que $\Gamma \vdash \alpha$ si et seulement si $\Gamma \vdash \alpha'$. Par conséquent, toute règle déjà démontrée et toute équivalence déjà démontrée s’appliquent aux lignes d’une déduction avec prémisses : si une ligne dit $\Gamma \vdash (\varphi \rightarrow \psi)$, la contraposition permet d’écrire en dessous $\Gamma \vdash (\neg\psi \rightarrow \neg\varphi)$ et de la justifier par « CP » et le numéro de la ligne. Pour les deux formes équivalentes de la leçon sur les symétries, dont on se servira sans cesse, on écrit « Éq » :

Il faut insister sur le fait que la première de ces équivalences n’est pas une définition ; la seconde, comme l’a montré la leçon sur les symétries, est une identité de chaînes, mais on la cite comme Éq avec la première. Par définition, $(\varphi \vee \psi)$ est $\neg(\varphi \downarrow \psi)$ et $(\neg\varphi \rightarrow \psi)$ est $(\neg\neg\varphi \vee \psi)$, qui sont des chaînes distinctes ; lire l’une comme l’autre « par définition de l’implication » est l’erreur que cette leçon évite. « Déf », en revanche, est réservé à l’écriture de la même chaîne sous un autre nom, comme lorsqu’on lit $(\varphi \rightarrow \psi)$ comme $(\neg\varphi \vee \psi)$.