Quatre techniques de déduction

Les outils de départ

Dans la leçon sur les systèmes déductifs formels, on a fixé le système de Łukasiewicz. Son langage est la langue des cercles et des disques, écrite avec les abréviations officielles de la leçon sur le langage de la logique propositionnelle ; ses axiomes sont toutes les instances des trois schémas suivants, où $\varphi$, $\psi$ et $\chi$ sont des formules quelconques, et sa seule règle est le modus ponens.

• A1 : $(\varphi \rightarrow (\psi \rightarrow \varphi))$.
• A2 : $((\varphi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \chi)))$.
• A3 : $((\neg\psi \rightarrow \neg\varphi) \rightarrow (\varphi \rightarrow \psi))$.
• MP : de $\varphi$ et de $(\varphi \rightarrow \psi)$ on déduit $\psi$.

Une déduction de $\varphi$ à partir d’un ensemble $\Gamma$ de formules est une suite finie de formules qui se termine par $\varphi$ et dans laquelle chaque formule est un axiome, un élément de $\Gamma$ ou le résultat de l’application du modus ponens à deux formules antérieures ; si elle existe, on écrit $\Gamma \vdash \varphi$, et si $\Gamma$ est vide, $\vdash \varphi$, et l’on dit que $\varphi$ est un théorème. Dans cette même leçon ont été démontrés les métathéorèmes que nous utiliserons ici : 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$), le modus ponens entre déductions (si $\Gamma \vdash \varphi$ et $\Gamma \vdash (\varphi \rightarrow \psi)$, alors $\Gamma \vdash \psi$), la coupure (Coupure : si $\Gamma \vdash \varphi_{i}$ pour chaque $i$ de $1$ à $n$ et $\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{n}\} \vdash \psi$, alors $\Gamma \vdash \psi$), la finitude (si $\Gamma \vdash \varphi$, un sous-ensemble fini de $\Gamma$ suffit), 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), et le théorème $\vdash (\varphi \rightarrow \varphi)$, que nous abrégerons Id dans les justifications. Enfin, $\varphi \dashv\vdash \psi$ (équivalence prouvable) signifie que $\{\varphi\} \vdash \psi$ et $\{\psi\} \vdash \varphi$.

Il convient de rappeler que $\neg$ et $\rightarrow$ ne sont pas des symboles de la langue de base, mais des abréviations : $\neg\varphi$ est la chaîne $(\varphi \downarrow \varphi)$, et $(\varphi \rightarrow \psi)$ est $(\neg\varphi \vee \psi)$, c’est-à-dire $\neg(\neg\varphi \downarrow \psi)$. Les trois axiomes ne parlent que de négations et d’implications, et la même leçon a montré, à l’aide d’un marquage à valeurs $0$ et $1$ qu’ils conservent, ainsi que le modus ponens, la limite qui s’ensuit : dans le système de Łukasiewicz, de $(v_{1} \downarrow v_{2})$ on ne déduit pas $(\neg\neg v_{1} \downarrow v_{2})$, et la négation conjointe reste en partie hors de sa portée. Cette leçon procède donc en deux temps. Jusqu’à la double négation incluse, $\vdash$ se rapporte au système de Łukasiewicz, et rien de ce que l’on démontre ne dépend du dépliage des abréviations. Une fois la double négation démontrée, on ajoute au système une seconde règle primitive, le remplacement de la double négation, qui agit sur la chaîne dépliée ; à partir de ce point, $\vdash$ se rapporte au système du cours, celui de Łukasiewicz augmenté de cette règle. Comme toute déduction du premier est aussi une déduction du second, rien de ce qui a été démontré auparavant ne se perd.

Deux styles de déduction

Il y a deux manières d’écrire une déduction, et l’on utilisera les deux. La première est la déduction proprement dite, une suite de formules dans laquelle chaque ligne est un axiome, une prémisse ou le résultat du modus ponens ; chaque ligne se justifie par A1, A2, A3, Prémisse ou MP$(i, j)$, où la ligne $i$ est l’antécédent et la ligne $j$ est l’implication dont l’antécédent est exactement la ligne $i$ (et, dès que la nouvelle règle aura été introduite, RDN$(i)$). La seconde est la déduction sur les déductions, dont les lignes ne sont pas des formules, mais des affirmations de la forme $\Gamma \vdash \varphi$ ; chacune se justifie par un métathéorème déjà démontré, et la suite entière est un raisonnement du métalangage qui garantit qu’il existe une déduction du premier style, bien qu’il ne l’écrive pas. Les justifications de ce second style se lisent comme suit.

• Réfl : la formule de droite appartient à l’ensemble de gauche.
• A1, A2, A3 : la formule de droite est une instance du schéma ; une instance d’un axiome se déduit de n’importe quel $\Gamma$ par une déduction d’une seule ligne.
• MP$(i, j)$ : le modus ponens entre déductions, appliqué à la ligne $i$, $\Gamma \vdash \varphi$, et à la ligne $j$, $\Gamma \vdash (\varphi \rightarrow \psi)$, avec le même $\Gamma$.
• TD$(i)$ et RTD$(i)$ : le théorème de déduction ou sa réciproque, appliqué à la ligne $i$.
• Le nom d’un théorème déjà démontré, comme Id ou DN : la formule de droite est une instance de ce théorème, et elle se déduit de n’importe quel $\Gamma$ par monotonie, car l’ensemble vide est inclus dans $\Gamma$.
• Prémisse, dans une déduction sur les déductions : la ligne est l’une des hypothèses de la règle que l’on est en train de démontrer.

Tout résultat de cette leçon est énoncé avec des métavariables et vaut donc pour des formules quelconques : sa démonstration est un schéma, et en y substituant une formule à chaque métavariable on obtient une autre démonstration, car les instances d’un schéma d’axiome le restent et chaque modus ponens le reste aussi (il en ira de même pour chaque application de la nouvelle règle). Ainsi, de $\vdash (\varphi \rightarrow \varphi)$ découle $\vdash (\neg\psi \rightarrow \neg\psi)$, avec $\neg\psi$ au lieu de $\varphi$. Ce procédé, appliquer un résultat à une formule plus complexe que celle de l’énoncé, est celui qui rapporte le plus dans la suite.

Du résultat à la règle

Les techniques de cette leçon se démontrent à partir de prémisses fixes, comme $\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)$ ; mais on les utilise au milieu de déductions qui ont d’autres prémisses, où $(\varphi \rightarrow \psi)$ et $(\psi \rightarrow \chi)$ ne sont pas des prémisses, mais des formules déjà déduites. Le lemme suivant, conséquence directe de la monotonie et de la coupure, autorise cet usage une fois pour toutes.

Il s’ensuit que chaque technique démontrée à partir de prémisses a trois présentations : le résultat lui-même, le théorème que l’on obtient en déchargeant ses prémisses et la règle qui s’applique sous n’importe quel $\Gamma$. Dans une déduction sur les déductions, la règle s’invoque par le nom de la technique et les numéros des lignes auxquelles elle s’applique, comme SH$(3, 4)$, et le lemme garantit que le pas est légitime.