Les symétries des connecteurs

Ce que l’on utilise et ce qu’il faut démontrer

La leçon sur les systèmes déductifs formels a fixé le système de Łukasiewicz : les axiomes A1, A2 et A3 et le modus ponens. Elle a établi en outre 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 sa réciproque (RTD) et l’équivalence prouvable, $\varphi \dashv\vdash \psi$, qui signifie que $\{\varphi\} \vdash \psi$ et $\{\psi\} \vdash \varphi$ ; et elle a montré, avec un marquage que les axiomes et le modus ponens conservent, que ce système ne déduit pas certaines formules sur la négation conjointe. La leçon sur les quatre techniques de déduction a ajouté le syllogisme hypothétique (SH : $\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)$), l’échange des prémisses (EP), la double négation (DN : $\varphi \dashv\vdash \neg\neg\varphi$, avec ses deux théorèmes $\vdash (\neg\neg\varphi \rightarrow \varphi)$ et $\vdash (\varphi \rightarrow \neg\neg\varphi)$) et la contraposition (CP) sous ses trois formes :

Une fois la double négation démontrée, cette même leçon a 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 d’une sous-formule $\neg\neg\theta$ par $\theta$, alors de $\chi$ on infère $\chi'$. La ligne ainsi obtenue à partir de la ligne $i$ se justifie par RDN$(i)$. À partir de ce point, $\vdash$ se rapporte au système du cours (A1 à A3, le modus ponens et RDN), dans lequel Réfl, Mon, Coupure, TD et RTD restent valables. La règle agit sur la chaîne de la langue de base, de sorte qu’elle atteint aussi les occurrences qu’une abréviation cache, et dans l’un ou l’autre des deux arguments d’une négation conjointe ; parmi ses conséquences immédiates figurent

et, en général, $\chi \dashv\vdash \chi'$ chaque fois que $\chi'$ résulte de $\chi$ par RDN. Une ligne d’équivalence de cette forme se justifie par « RDN », sans numéro de ligne, de la même manière qu’une ligne « DN » ou « CP » cite une équivalence déjà démontrée. Comme là, un théorème déjà démontré peut s’écrire comme ligne d’une déduction, car sa propre déduction peut s’intercaler à cet endroit ; et, par le lemme « du résultat à la règle » de cette leçon, chaque technique s’applique aussi comme règle sous n’importe quel ensemble $\Gamma$ de prémisses, citée avec les numéros des lignes auxquelles elle s’applique, comme CP$(i)$ ou SH$(i, j)$. Dans les déductions sur les déductions, « Prémisse » désigne une hypothèse de la règle que l’on démontre.

Les abréviations officielles, fixées dans la leçon sur le langage de la logique propositionnelle, sont les seules définitions des connecteurs :

Une ligne justifiée par « Déf » ne déduit rien : elle écrit la même formule sous un autre nom, et l’annotation dit quelle abréviation on déplie ou on replie (« Déf $\rightarrow$ », « Déf $\vee$ »). Il convient de rappeler le phénomène observé dans la leçon sur la formalisation du langage naturel : une même formule admet plusieurs noms, de sorte qu’une conjonction est aussi, comme chaîne, une disjonction. Par exemple, en dépliant l’implication avec $\neg\varphi$ au lieu de $\varphi$, on obtient

et la double négation qui apparaît devant $\varphi$, cachée par l’abréviation, est la raison pour laquelle la règle RDN interviendra dans tout ce qui suit.

L’équivalence prouvable comme égalité

Les démonstrations de cette leçon sont, presque toutes, des chaînes d’équivalences : $\varphi_{1} \dashv\vdash \varphi_{2}$, $\varphi_{2} \dashv\vdash \varphi_{3}$, et ainsi de suite. Pour que l’on conclue $\varphi_{1} \dashv\vdash \varphi_{n}$ d’une chaîne, l’équivalence prouvable doit se comporter comme une égalité, et c’est ce qu’a établi la proposition sur les propriétés de l’équivalence prouvable de la leçon sur les systèmes déductifs formels : la relation est réflexive ($\varphi \dashv\vdash \varphi$), symétrique (si $\varphi \dashv\vdash \psi$, alors $\psi \dashv\vdash \varphi$) et transitive (si $\varphi \dashv\vdash \psi$ et $\psi \dashv\vdash \chi$, alors $\varphi \dashv\vdash \chi$), et deux formules prouvablement équivalentes sont interchangeables comme conclusions (si $\Gamma \vdash \varphi$ et $\varphi \dashv\vdash \varphi'$, alors $\Gamma \vdash \varphi'$, pour tout ensemble $\Gamma$ de formules). Il convient de rappeler comment les deux dernières ont été démontrées, car toute la leçon repose sur elles : de $\{\varphi\} \vdash \varphi'$ on passe, par monotonie, à $\Gamma \cup \{\varphi\} \vdash \varphi'$, et de celle-ci et de $\Gamma \vdash \varphi$, par coupure, à $\Gamma \vdash \varphi'$ ; la transitivité résulte de l’application de ce raisonnement avec $\Gamma = \{\varphi\}$ dans un sens et avec $\Gamma = \{\chi\}$ dans l’autre.

Désormais, le pas qui réunit une chaîne d’équivalences en une seule se justifie par « Coupure », qui est l’instrument de cette proposition. Or chaque maillon $\varphi_{i} \dashv\vdash \varphi_{i+1}$ contient les deux déductions, celle de l’aller et celle du retour ; d’où une chaîne d’équivalences démontre à la fois les deux sens de sa conclusion, et rien n’est laissé « en exercice ».