Lois de De Morgan et de distributivité

Les leçons précédentes de cette unité ont construit, l’une sur l’autre, les outils de la déduction : le système d’axiomes et le modus ponens, les quatre techniques de base et le remplacement de la double négation, les symétries des connecteurs et les techniques de la logique classique. Cette leçon n’ajoute aucune règle nouvelle ; elle les fait travailler ensemble. S’il en est ainsi, son intérêt ne tient pas tant aux énoncés, que l’on connaît peut-être d’autres cours, qu’à la manière de les obtenir : chaque ligne doit être justifiée par un axiome, une prémisse, une définition, l’une des deux règles primitives ou un résultat déjà démontré, et aucune ne peut s’appuyer sur ce qui « semble évident ».

Ce que l’on utilise et comment on l’enchaîne

De la leçon sur les systèmes déductifs formels, on prend les axiomes A1, A2 et A3 de Łukasiewicz, le modus ponens (MP), aussi avec prémisses, la réflexivité (Réfl : si $\varphi \in \Gamma$, alors $\Gamma \vdash \varphi$), la monotonie (Mon), la coupure (Coupure : si $\Gamma \vdash \varphi_i$ pour chaque $i$ et $\Gamma \cup \{\varphi_1, \ldots, \varphi_n\} \vdash \psi$, alors $\Gamma \vdash \psi$), le théorème de déduction (TD) et l’équivalence prouvable ($\varphi \dashv\vdash \psi$ si $\{\varphi\} \vdash \psi$ et $\{\psi\} \vdash \varphi$), avec ses propriétés : elle est réflexive, symétrique et transitive, et, si $\varphi \dashv\vdash \psi$, alors $\Gamma \vdash \varphi$ si et seulement si $\Gamma \vdash \psi$. De la leçon sur les quatre techniques de déduction, la double négation (DN : $\varphi \dashv\vdash \neg\neg\varphi$), la contraposition (CP), en particulier $(\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \neg\varphi)$, et la seconde règle primitive du système du cours, le remplacement de la double négation (RDN), avec lequel le théorème de déduction reste valable : si $\chi'$ résulte de $\chi$ en remplaçant une occurrence d’une sous-formule $\theta$ par $\neg\neg\theta$, ou une occurrence de $\neg\neg\theta$ par $\theta$, de $\chi$ on infère $\chi'$ ; la ligne ainsi obtenue de la ligne $i$ se justifie RDN$(i)$. Parmi ses conséquences immédiates figurent $(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi)$, $(\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi)$ et, en général, $\chi \dashv\vdash \chi'$ lorsque $\chi'$ résulte de $\chi$ par RDN ; il s’ensuit que RDN$(i)$ s’applique aussi à une ligne de la forme $\chi \dashv\vdash \varphi$, pour changer une double négation dans $\varphi$. De la leçon sur les symétries des connecteurs, le remplacement des équivalents (Rempl) et les symétries (Sym), parmi lesquelles $(\varphi \vee \psi) \dashv\vdash (\psi \vee \varphi)$ et $(\varphi \wedge \psi) \dashv\vdash (\psi \wedge \varphi)$.

De la leçon sur les techniques de la logique classique, on prend, toutes avec un ensemble $\Gamma$ de prémisses, les règles suivantes. L’introduction de la disjonction ($\vee$I) : si $\Gamma \vdash \varphi$, alors $\Gamma \vdash (\varphi \vee \psi)$ et $\Gamma \vdash (\psi \vee \varphi)$. L’élimination de la disjonction ($\vee$E, syllogisme disjonctif) : si $\Gamma \vdash (\varphi \vee \psi)$ et $\Gamma \vdash \neg\varphi$, alors $\Gamma \vdash \psi$. L’introduction de la conjonction ($\wedge$I) : si $\Gamma \vdash \varphi$ et $\Gamma \vdash \psi$, alors $\Gamma \vdash (\varphi \wedge \psi)$. L’élimination de la conjonction ($\wedge$E) : si $\Gamma \vdash (\varphi \wedge \psi)$, alors $\Gamma \vdash \varphi$ et $\Gamma \vdash \psi$. Le tiers exclu (TE) : $\vdash (\varphi \vee \neg\varphi)$. Et le raisonnement par disjonction des cas (Cas) sous ses deux formes : si $\Gamma \cup \{\varphi\} \vdash \chi$ et $\Gamma \cup \{\neg\varphi\} \vdash \chi$, alors $\Gamma \vdash \chi$ ; et si $\Gamma \cup \{\varphi\} \vdash \chi$, $\Gamma \cup \{\psi\} \vdash \chi$ et $\Gamma \vdash (\varphi \vee \psi)$, alors $\Gamma \vdash \chi$. Dans les déductions, la première forme se cite avec deux lignes, Cas$(i, j)$, et la seconde, avec trois, Cas$(i, j, k)$, dans l’ordre de l’énoncé : les deux cas et, à la fin, la disjonction. Cette leçon rappelle en outre que toute règle déjà démontrée vaut à l’intérieur d’un contexte $\Gamma$, et c’est ainsi qu’on utilise ici la double négation et la contraposition.

Noms d’une chaîne et formules équivalentes

Rappelons, d’après la leçon sur le langage de la logique propositionnelle, que les connecteurs autres que $\downarrow$ sont des abréviations avec une définition officielle et unique : $\neg\varphi := (\varphi \downarrow \varphi)$, $(\varphi \vee \psi) := \neg(\varphi \downarrow \psi)$, $(\varphi \wedge \psi) := \neg(\neg\varphi \vee \neg\psi)$, $(\varphi \rightarrow \psi) := (\neg\varphi \vee \psi)$, $(\varphi \leftrightarrow \psi) := ((\varphi \rightarrow \psi) \wedge (\psi \rightarrow \varphi))$ et $(\varphi \veebar \psi) := \neg(\varphi \leftrightarrow \psi)$. Une définition n’affirme rien sur les formules : elle donne un second nom à une chaîne qui existait déjà. Il s’ensuit que, si deux expressions désignent la même chaîne, l’une peut être mise à la place de l’autre n’importe où, y compris à l’intérieur d’une formule plus grande, car ce qu’on écrit est la même suite de cercles et de disques. Ainsi, $\neg(\varphi \wedge \psi)$ et $\neg\neg(\neg\varphi \vee \neg\psi)$ sont la même chaîne : la seconde résulte de l’écriture, à l’intérieur de la première, du dépliage de la conjonction. Dans les déductions, ce changement de nom se justifie par « Déf », suivi du connecteur que l’on déplie ou que l’on replie.

Or une équivalence prouvable n’est pas une identité. Dire que $\varphi \dashv\vdash \neg\neg\varphi$, c’est dire que chacune se déduit de l’autre, non qu’elles soient la même chaîne : $\neg\neg\varphi$ est beaucoup plus longue que $\varphi$. Par conséquent, savoir que $\varphi \dashv\vdash \varphi'$ n’autorise pas, sans plus, à écrire $\varphi'$ à la place de $\varphi$ à l’intérieur d’une formule plus grande. Cela n’autorise pas non plus à « nier les deux côtés » : que de $\varphi \dashv\vdash \varphi'$ découle $\neg\varphi \dashv\vdash \neg\varphi'$ est un théorème, le remplacement des équivalents, dont la démonstration utilise la contraposition, et non une opération évidente. Il y a un seul cas où le système autorise directement le remplacement, en n’importe quel endroit d’une formule : celui de $\theta$ par $\neg\neg\theta$, ou l’inverse, qui est la règle RDN ; et la leçon sur les systèmes déductifs a montré, avec le marquage, que même ce cas ne se déduit pas des axiomes et du modus ponens, de sorte qu’il a fallu le postuler. Ce soin n’est pas de la pédanterie ; c’est ce qui distingue une démonstration d’une manipulation de symboles qui pourrait, appliquée à d’autres connecteurs ou dans d’autres systèmes, conduire à des faussetés.

Deux résultats fixent avec précision ce qui est permis. Le premier est la proposition sur les propriétés de l’équivalence prouvable de la leçon sur les systèmes déductifs formels : si $\Gamma \vdash \varphi$ et $\varphi \dashv\vdash \varphi'$, alors $\Gamma \vdash \varphi'$, de sorte qu’une équivalence prouvable peut s’appliquer à la formule entière d’une ligne ; et l’équivalence prouvable est réflexive, symétrique et transitive, de sorte que les équivalences s’enchaînent (si $\chi \dashv\vdash \varphi$ et $\varphi \dashv\vdash \varphi'$, alors $\chi \dashv\vdash \varphi'$) et que deux expressions qui désignent la même chaîne sont, par réflexivité, prouvablement équivalentes. Le second, le lemme suivant, rassemble, pour qu’on puisse la citer commodément, l’extension du remplacement des équivalents à la disjonction et à la conjonction, que la leçon sur les symétries démontre pour la négation, l’implication et la négation conjointe et étend à ces deux connecteurs dans l’un de ses problèmes résolus.

Désormais, « Rempl » désigne le remplacement des équivalents sous l’une quelconque de ses formes, y compris celles de ce lemme, et peut s’appliquer plusieurs fois de suite, couche par couche, pour atteindre une sous-formule située à n’importe quelle profondeur. Lorsqu’une ligne s’obtient de la ligne $i$ en appliquant une équivalence déjà démontrée, soit à la formule entière, soit, avec Rempl, à l’une de ses parties, elle se justifie par le nom de cette équivalence et le numéro de la ligne : DN$(i)$, « Rempl, DM$(i)$ ». Un changement de nom, qui n’applique aucune équivalence mais réécrit la même chaîne, se justifie de la même manière, par Déf suivi du connecteur que l’on déplie ou que l’on replie : Déf $\wedge$ $(i)$. La proposition de la leçon sur les systèmes déductifs formels garantit que ces lignes sont justifiées, que la ligne $i$ affirme $\Gamma \vdash \varphi$ ou qu’elle affirme une équivalence $\chi \dashv\vdash \varphi$ que l’on prolonge.