Déduction : synthèse et défis

Résumé

Cette leçon clôt l’unité consacrée à la déduction. Elle reconstruit la chaîne déductive qui va de la définition du système de Łukasiewicz (trois schémas d’axiomes et le modus ponens) au théorème de déduction et à la limite de ce système dans la langue de la négation conjointe ; de là aux quatre techniques de base et à la règle de remplacement de la double négation, qui complète le système du cours ; du lemme fondamental de la négation conjointe au remplacement des équivalents et aux symétries, et de là aux règles de la logique classique et aux lois de De Morgan et de distributivité, en indiquant à chaque maillon quels résultats il utilise et dans quelle leçon il est démontré. Elle distingue ce que l’unité a démontré de ce qu’elle a admis, situe l’acquis par rapport au plan du cours et explique pourquoi la question que l’unité laisse ouverte, celle de savoir si le déductible coïncide avec le vrai, conduit à l’unité de sémantique. Elle reprend dans son évaluation de sortie les compétences de l’évaluation d’entrée et se termine par six défis, d’une difficulté supérieure à celle des problèmes des leçons, qui exigent de combiner les instruments de plusieurs d’entre elles.

Objectifs d’apprentissage

Reconstruire l’ordre logique des résultats de l’unité, en identifiant les résultats antérieurs sur lesquels chacun s’appuie et la leçon où il est démontré.
Expliquer comment s’enchaînent le théorème de déduction, la double négation, la règle de remplacement de la double négation, la contraposition, le lemme fondamental et le remplacement des équivalents, et pourquoi les règles classiques et les lois de De Morgan et de distributivité en dépendent.
Distinguer ce que l’unité a démontré de ce qu’elle a admis (les schémas d’axiomes, les deux règles primitives, la récurrence forte, l’induction structurelle et la lecture unique) et de ce qu’elle a laissé aux unités suivantes, en particulier la relation entre déduction et vérité.
Résoudre des problèmes qui combinent les marquages, la règle de remplacement de la double négation, le théorème de déduction, le raisonnement par disjonction des cas, le raisonnement par l’absurde, le remplacement des équivalents et les lois de De Morgan et de distributivité.

L’acquis de l’unité

L’unité s’était proposé de doter le langage de l’unité précédente d’un système déductif, c’est-à-dire d’une manière purement syntaxique d’obtenir des formules à partir d’autres, et de démontrer avec ce système, ligne par ligne, les techniques avec lesquelles raisonnent les mathématiques. Le but a été atteint avec quelques réserves, chacune déclarée en son lieu : les trois schémas d’axiomes et les deux règles primitives, qui ne se démontrent pas mais se choisissent, et dont le bon choix est une question que l’unité pose sans y répondre entièrement ; la récurrence forte et l’induction structurelle, la lecture unique et la définition par récurrence, qui ont été démontrées dans l’unité précédente et sont utilisées ici ; et l’indispensable de la théorie des ensembles (sous-ensembles, réunions et ensembles finis), rappelé là où il était nécessaire. Avec ces réserves, le chemin parcouru peut se lire comme une seule chaîne déductive en quatre tronçons.

Le système de Łukasiewicz et sa limite

La leçon sur les systèmes déductifs formels a défini un système comme un langage, des axiomes et des règles, tous vérifiables en ne regardant que les chaînes, et a fixé la première étape du système du cours, le système de Łukasiewicz : les schémas A1, A2 et A3 et le modus ponens comme règle unique, que la lecture unique rend applicable sans ambiguïté. Elle a défini la déduction à partir d’un ensemble $\Gamma$ de prémisses et la relation $\Gamma \vdash \varphi$ , a déduit $\vdash (\varphi \rightarrow \varphi)$ en cinq lignes et a démontré les propriétés structurelles : réflexivité, monotonie, modus ponens entre déductions, coupure et finitude. Avec elles et avec la récurrence forte sur le nombre de lignes, elle a démontré le théorème de déduction, dont le deuxième cas exige d’avoir déduit auparavant $(\varphi \rightarrow \varphi)$ , et sa réciproque ; elle en a tiré l’équivalence prouvable, réflexive, symétrique et transitive. Enfin, elle a établi la limite de ce système : un marquage à valeurs $0$ et $1$ , défini par récurrence sur la forme primitive $(\alpha \downarrow \beta)$ , traite la négation et l’implication comme d’habitude, est conservé par A1, A2, A3 et le modus ponens, et laisse libre la valeur de formules comme $(v_{1} \downarrow v_{2})$ . Il en découle que $((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1})$ n’est pas un théorème du système de Łukasiewicz, et que de $(v_{1} \downarrow v_{2})$ on ne déduit pas $(\neg\neg v_{1} \downarrow v_{2})$ , ni l’inverse. Comme tout marquage donne la même valeur à $\theta$ et à $\neg\neg\theta$ , la leçon a en outre fait observer que même la double négation, une fois démontrée, ne remédierait pas à cette limite.

Les quatre techniques et la règle nouvelle

La leçon sur les quatre techniques de déduction a d’abord démontré le lemme « du résultat à la règle » : si $\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta$ , la même conclusion s’obtient à partir de n’importe quel $\Gamma$ qui déduit les $\alpha_{i}$ , et de plus $\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots))$ . C’est ce lemme qui permet d’utiliser chaque technique sous trois présentations (à partir de prémisses, comme théorème et comme règle), et les leçons sur les symétries et sur De Morgan, qui assemblent des chaînes d’équivalences avec la coupure, s’appuient pour cela sur les propriétés de l’équivalence prouvable de la première leçon, qui sont la même idée appliquée à une seule prémisse ; dans la chaîne, chaque résultat ne figure qu’une fois, là où il est démontré. Avec lui, la leçon a déduit le syllogisme hypothétique à partir de A1 et de A2 en sept lignes, l’échange des prémisses avec le théorème de déduction, la double négation (dont le premier sens applique A3 deux fois à une implication fabriquée avec A1, et dont le second applique le premier à $\neg\varphi$ et A3) et la contraposition sous ses trois formes, qui répartissent de trois manières les négations d’une implication ; les quatre valent déjà dans le système de Łukasiewicz.

Une fois la double négation démontrée, la leçon a complété le système du cours par une seconde règle primitive, le remplacement de la double négation (RDN) : de $\chi$ on infère $\chi'$ lorsque $\chi'$ résulte du remplacement, dans $\chi$ , d’une occurrence d’une sous-formule $\theta$ par $\neg\neg\theta$ , ou d’une occurrence de $\neg\neg\theta$ par $\theta$ . La règle doit être postulée, car le marquage $m_{1}$ donne $1$ aux théorèmes de la double négation et sépare pourtant $(v_{1} \downarrow v_{2})$ de $(\neg\neg v_{1} \downarrow v_{2})$ ; RDN ne conserve pas $m_{1}$ , et c’est pourquoi elle élargit le déductible, mais elle conserve le marquage honnête, et c’est pourquoi elle ne l’élargit pas trop. La règle agit sur la chaîne de la langue de base, où une négation duplique son argument : $(\varphi \rightarrow \psi)$ contient deux fois la sous-formule $\neg\varphi$ , et placer une double négation devant son antécédent exige deux applications. Cette même observation soutient l’extension du théorème de déduction : si une ligne s’obtient par la règle, l’hypothèse de récurrence donne l’implication dont le conséquent est la ligne précédente, et deux applications de la règle, une dans chaque copie de ce conséquent, donnent l’implication cherchée ; les autres propriétés structurelles valent avec la même démonstration. Les premières conséquences sont qu’une formule équivaut à toute formule qui en résulte par la règle, en particulier $(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi)$ et $(\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi)$ , et que les implications correspondantes, que d’autres systèmes prennent pour axiomes, sont ici des théorèmes.

Connecteurs et remplacement

La leçon sur les symétries des connecteurs a affronté la difficulté propre à la langue des cercles et des disques : les axiomes de Łukasiewicz ne parlent que de négations et d’implications, et presque aucune négation conjointe n’est l’une ou l’autre. Le lemme fondamental, $(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi)$ , jette le pont : comme $\neg(\neg\varphi \rightarrow \psi)$ est $\neg\neg(\neg\neg\varphi \downarrow \psi)$ , la règle RDN place la double négation intérieure et la double négation, l’extérieure ; en sens inverse, la double négation et la règle les retirent. Avec lui, le remplacement des équivalents, démontré d’abord sous la négation et des deux côtés de l’implication avec la contraposition et le syllogisme hypothétique, a été étendu aux deux arguments de la négation conjointe et, de là, à la disjonction et à la conjonction. La règle et le remplacement ne se rendent pas superflus l’un l’autre : la règle échange seulement $\theta$ et $\neg\neg\theta$ , tandis que le remplacement admet des équivalents quelconques ; et le remplacement, démontré avec le lemme fondamental, repose à son tour sur la règle. La leçon a démontré ensuite que les formes que d’autres textes prennent pour des définitions sont des équivalences : $(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi)$ , qui exige deux applications de la règle, une dans chaque copie que crée la négation extérieure, et $(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi)$ , qui exige la double négation ; en revanche, $(\varphi \wedge \psi)$ et $\neg(\varphi \rightarrow \neg\psi)$ sont la même chaîne. Enfin, elle a démontré les cinq symétries dans l’ordre qu’imposent les définitions : celle de la négation conjointe avec le lemme fondamental et la contraposition, et chacune des autres avec la précédente, transportée par le remplacement sous la négation quand il le faut.

Les règles classiques et les lois

La leçon sur les techniques de la logique classique a démontré, toutes avec un ensemble $\Gamma$ de prémisses qui se transmet de ligne en ligne, l’introduction et l’élimination de la disjonction et de la conjonction, le tiers exclu et la non-contradiction, l’explosion, le raisonnement par l’absurde sous ses deux formes et le raisonnement par disjonction des cas, avec une formule et sa négation et avec une disjonction quelconque. L’ordre des dépendances est strict : l’explosion repose sur les règles de la disjonction ; le raisonnement par l’absurde classique, sur l’explosion et sur A3 ; le raisonnement par disjonction des cas, sur la contraposition et sur le raisonnement par l’absurde. Aucune de ces démonstrations n’invoque directement la règle RDN : la règle agit à travers les formes équivalentes et le remplacement des équivalents. La leçon sur les lois de De Morgan et de distributivité a fait travailler ces règles ensemble : la première loi de De Morgan résulte de la définition de la conjonction et de la double négation ; la seconde exige d’entrer dans la négation conjointe, où la règle RDN intervient deux fois, une dans chaque argument et sans qu’il faille la symétrie, et il en découle que $(\varphi \downarrow \psi)$ équivaut à $(\neg\varphi \wedge \neg\psi)$ , la lecture « ni $\varphi$ ni $\psi$ » que l’unité précédente avait stipulée ; les variantes comprennent $\neg(\varphi \rightarrow \psi) \dashv\vdash (\varphi \wedge \neg\psi)$ . Les deux lois de distributivité ont été démontrées dans leurs deux sens par disjonction des cas, en choisissant dans chacun la forme du raisonnement par disjonction des cas qui convient.

La figure suivante réunit les quatre tronçons en une seule chaîne. Chaque nœud de la colonne est une définition ou un résultat, numéroté selon l’ordre logique et relié par un arc aux maillons antérieurs qu’utilise sa démonstration ; autour flottent les appuis, c’est-à-dire les principes et les instruments auxquels la chaîne recourt sans cesse, chacun relié par un trait plein aux maillons qui s’appuient sur lui et par un trait pointillé au maillon où il est établi, sauf ceux que cette chaîne ne démontre pas (les schémas d’axiomes, qui sont admis, et les instruments de l’unité précédente), qui sont dessinés comme des anneaux. La règle de remplacement de la double négation, bien qu’elle soit elle aussi admise sans démonstration, figure reliée au maillon qui l’introduit, parce que c’est là qu’on explique pourquoi elle doit être postulée. Un clic sur un appui met en évidence tous les maillons qui l’utilisent, et chaque maillon renvoie à la leçon où il est démontré. On remarquera que le théorème de déduction et la double négation sont, après les axiomes, les appuis les plus visités de l’unité, et que la règle nouvelle soutient tout ce que l’unité dit de la négation conjointe : le théorème de déduction étendu, le lemme fondamental, les formes équivalentes et la seconde loi de De Morgan.

Appuis de la chaîne

ALecture unique et récurrence. Si $\sigI\varphi\psi = \sigI\varphi'\psi'$ , les quatre chaînes étant des formules, alors $\varphi = \varphi'$ et $\psi = \psi'$ ; d’où une règle qui calcule la valeur de $\sigI\varphi\psi$ à partir de $\varphi$ , de $\psi$ et de leurs valeurs définit une seule fonction sur les formules. Elle a été démontrée dans l’unité précédente. Admis sans démonstration dans cette unité.
BRécurrence forte. Si une propriété vaut pour un entier naturel chaque fois qu’elle vaut pour tous les entiers plus petits, elle vaut pour tous les entiers naturels. Elle a été déduite de la récurrence simple dans l’unité précédente, et elle s’applique ici au nombre de lignes d’une déduction. Admis sans démonstration dans cette unité.
CAxiomes de Łukasiewicz. Les schémas A1, $(\varphi \rightarrow (\psi \rightarrow \varphi))$ ; A2, $((\varphi \rightarrow (\psi \rightarrow \chi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \chi)))$ ; et A3, $((\neg\psi \rightarrow \neg\varphi) \rightarrow (\varphi \rightarrow \psi))$ . Ils sont admis. Admis sans démonstration dans cette unité.
DRemplacement de la double négation. Seconde règle primitive du système du cours : de $\chi$ on infère $\chi'$ 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$ . Elle est postulée après la démonstration de la double négation. Établi dans: 8. Remplacement de la double négation.
EThéorème de déduction. $\Gamma \cup \{\varphi\} \vdash \psi$ si et seulement si $\Gamma \vdash (\varphi \rightarrow \psi)$ ; il se démontre dans le système de Łukasiewicz et vaut, avec un cas de plus, dans le système du cours. Établi dans: 3. Théorème de déduction et équivalence prouvable.
FDu résultat à la règle. Si $\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta$ et $\Gamma \vdash \alpha_{i}$ pour chaque $i$ , alors $\Gamma \vdash \beta$ : toute technique démontrée à partir de prémisses s’applique sous n’importe quel ensemble de prémisses. Établi dans: 5. Du résultat à la règle.
GDouble négation. $\varphi \dashv\vdash \neg\neg\varphi$ , avec les théorèmes $\vdash (\neg\neg\varphi \rightarrow \varphi)$ et $\vdash (\varphi \rightarrow \neg\neg\varphi)$ . Établi dans: 7. Double négation.
HRemplacement des équivalents. Si $\varphi \dashv\vdash \varphi'$ , on peut mettre $\varphi'$ à la place de $\varphi$ sous une négation, des deux côtés d’une implication, d’une négation conjointe, d’une disjonction et d’une conjonction, sans altérer l’équivalence. Établi dans: 12. Remplacement des équivalents.

Tronçon 1 Le système de Łukasiewicz et sa limite
- Reconnaître les instances des schémas et décider si une suite de formules est une déduction à partir d’un ensemble de prémisses.
- Démontrer les propriétés structurelles de la déduction et le théorème de déduction par récurrence forte sur le nombre de lignes.
- Construire des déductions sur les déductions avec la réflexivité, la monotonie, la coupure, le théorème de déduction et sa réciproque.
- Démontrer qu’une formule ne se déduit pas au moyen d’un marquage que les axiomes et le modus ponens conservent, et expliquer avec lui la limite du système de Łukasiewicz.
1. Système, déduction et identité. Les axiomes du système de Łukasiewicz sont les instances uniformes de A1 à A3, et sa règle unique est le modus ponens. $\Gamma \vdash \varphi$ s’il existe une suite finie de formules qui se termine par $\varphi$ , dont chacune est un axiome, un élément de $\Gamma$ ou obtenue par modus ponens de deux précédentes. Le premier théorème, $\vdash (\varphi \rightarrow \varphi)$ , se déduit en cinq lignes avec A1 et A2.
  Repose sur: A (Lecture unique et récurrence), C (Axiomes de Łukasiewicz). Démontré dans: Systèmes déductifs formels.
2. Propriétés structurelles. Si $\varphi \in \Gamma$ , $\Gamma \vdash \varphi$ ; si $\Gamma \subseteq \Delta$ et $\Gamma \vdash \varphi$ , $\Delta \vdash \varphi$ ; de $\Gamma \vdash \varphi$ et $\Gamma \vdash (\varphi \rightarrow \psi)$ découle $\Gamma \vdash \psi$ ; si $\Gamma \vdash \varphi_{i}$ pour chaque $i$ et $\Gamma \cup \{\varphi_{1}, \ldots, \varphi_{r}\} \vdash \psi$ , $\Gamma \vdash \psi$ ; et si $\Gamma \vdash \varphi$ , une partie finie de $\Gamma$ suffit.
  Utilise: 1. Système, déduction et identité. Démontré dans: Systèmes déductifs formels.
3. Théorème de déduction et équivalence prouvable. $\Gamma \cup \{\varphi\} \vdash \psi$ si et seulement si $\Gamma \vdash (\varphi \rightarrow \psi)$ , par récurrence forte sur le nombre de lignes, avec A1, A2 et l’identité. Il en découle que l’équivalence prouvable, $\varphi \dashv\vdash \psi$ , est réflexive, symétrique et transitive, et que deux formules équivalentes se déduisent des mêmes ensembles.
  Utilise: 1. Système, déduction et identité, 2. Propriétés structurelles. Repose sur: B (Récurrence forte), C (Axiomes de Łukasiewicz). Démontré dans: Systèmes déductifs formels.
4. Limite du système de Łukasiewicz. Un marquage à valeurs $0$ et $1$ défini par récurrence satisfait $m(\neg\varphi) = 1 - m(\varphi)$ et $m((\varphi \rightarrow \psi)) = 1 - m(\varphi) \left( 1 - m(\psi) \right)$ , et A1, A2, A3 et le modus ponens conservent le marquage $1$ ; d’où $((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1})$ n’est pas un théorème du système de Łukasiewicz, et $\{(v_{1} \downarrow v_{2})\} \nvdash (\neg\neg v_{1} \downarrow v_{2})$ , ni l’inverse. Comme tout marquage donne $1$ à la double négation, le remplacement doit être postulé.
  Utilise: 1. Système, déduction et identité. Repose sur: A (Lecture unique et récurrence), B (Récurrence forte), C (Axiomes de Łukasiewicz). Démontré dans: Systèmes déductifs formels.
Tronçon 2 Les quatre techniques et la règle nouvelle
- Convertir un résultat à partir de prémisses en un théorème et en une règle applicable sous n’importe quel ensemble de prémisses.
- Enchaîner des implications, réordonner des antécédents, placer et retirer des doubles négations et choisir la forme de la contraposition qui correspond à chaque implication.
- Appliquer la règle de remplacement de la double négation, en repérant les occurrences que cachent les abréviations et en la répétant dans chaque copie que crée une négation.
- Expliquer avec le marquage pourquoi la règle est postulée, et démontrer que le théorème de déduction vaut avec elle.
1. Du résultat à la règle. Si $\{\alpha_{1}, \ldots, \alpha_{n}\} \vdash \beta$ , alors de $\Gamma \vdash \alpha_{1}$ , $\ldots$ , $\Gamma \vdash \alpha_{n}$ découle $\Gamma \vdash \beta$ , et $\vdash (\alpha_{1} \rightarrow (\alpha_{2} \rightarrow \cdots (\alpha_{n} \rightarrow \beta) \cdots))$ ; en particulier, si $\alpha \dashv\vdash \alpha'$ , $\Gamma \vdash \alpha$ si et seulement si $\Gamma \vdash \alpha'$ .
  Utilise: 2. Propriétés structurelles. Repose sur: E (Théorème de déduction). Démontré dans: Quatre techniques de déduction.
2. Syllogisme hypothétique et échange. $\{(\varphi \rightarrow \psi), (\psi \rightarrow \chi)\} \vdash (\varphi \rightarrow \chi)$ , avec une déduction de sept lignes à partir de A1 et de A2 ; et $\{(\varphi \rightarrow (\psi \rightarrow \chi))\} \vdash (\psi \rightarrow (\varphi \rightarrow \chi))$ .
  Utilise: 1. Système, déduction et identité. Repose sur: C (Axiomes de Łukasiewicz), E (Théorème de déduction), F (Du résultat à la règle). Démontré dans: Quatre techniques de déduction.
3. Double négation. $\vdash (\neg\neg\varphi \rightarrow \varphi)$ , en appliquant A3 deux fois à une implication que A1 fabrique à partir de $\neg\neg\varphi$ ; $\vdash (\varphi \rightarrow \neg\neg\varphi)$ , en appliquant ce qui précède à $\neg\varphi$ et A3 ; d’où $\varphi \dashv\vdash \neg\neg\varphi$ , déjà dans le système de Łukasiewicz.
  Repose sur: C (Axiomes de Łukasiewicz), E (Théorème de déduction). Démontré dans: Quatre techniques de déduction.
4. Remplacement de la double négation. On postule la règle RDN, car le marquage donne $1$ à la double négation et non au remplacement à l’intérieur d’une négation conjointe. Si $\chi'$ résulte de $\chi$ par la règle, $\chi \dashv\vdash \chi'$ ; en particulier, $(\varphi \downarrow \psi) \dashv\vdash (\neg\neg\varphi \downarrow \psi)$ et $(\varphi \downarrow \psi) \dashv\vdash (\varphi \downarrow \neg\neg\psi)$ .
  Utilise: 3. Théorème de déduction et équivalence prouvable, 4. Limite du système de Łukasiewicz. Repose sur: G (Double négation). Démontré dans: Quatre techniques de déduction.
5. Théorème de déduction dans le système du cours. Réflexivité, monotonie, coupure et finitude valent avec la règle nouvelle, et aussi $\Gamma \cup \{\varphi\} \vdash \psi$ si et seulement si $\Gamma \vdash (\varphi \rightarrow \psi)$ : dans le cas nouveau, comme $(\varphi \rightarrow \chi)$ est $((\neg\varphi \downarrow \chi) \downarrow (\neg\varphi \downarrow \chi))$ , la règle s’applique deux fois, une dans chaque copie de $\chi$ . Il en découle que $\vdash ((\varphi \downarrow \psi) \rightarrow (\neg\neg\varphi \downarrow \psi))$ et sa réciproque sont des théorèmes.
  Utilise: 2. Propriétés structurelles, 3. Théorème de déduction et équivalence prouvable. Repose sur: B (Récurrence forte), D (Remplacement de la double négation). Démontré dans: Quatre techniques de déduction.
6. Contraposition. $(\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \neg\varphi)$ , $(\neg\varphi \rightarrow \psi) \dashv\vdash (\neg\psi \rightarrow \varphi)$ et $(\varphi \rightarrow \neg\psi) \dashv\vdash (\psi \rightarrow \neg\varphi)$ : les membres changent de côté, et chacun change de signe en passant.
  Utilise: 6. Syllogisme hypothétique et échange. Repose sur: C (Axiomes de Łukasiewicz), E (Théorème de déduction), G (Double négation), F (Du résultat à la règle). Démontré dans: Quatre techniques de déduction.
Tronçon 3 Connecteurs et remplacement
- Déplier les abréviations pour décider si deux expressions désignent la même chaîne ou des formules dont l’équivalence exige une déduction.
- Traduire la négation conjointe en négation et implication avec le lemme fondamental.
- Transporter une équivalence à l’intérieur d’une formule avec le remplacement des équivalents, le distinguer de la règle de remplacement de la double négation et enchaîner des équivalences.
- Démontrer les cinq symétries dans l’ordre qu’imposent les définitions.
1. Lemme fondamental. $(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi)$ : comme $\neg(\neg\varphi \rightarrow \psi)$ est $\neg\neg(\neg\neg\varphi \downarrow \psi)$ , la règle RDN place la double négation intérieure et la double négation, l’extérieure ; en sens inverse, la double négation et la règle les retirent.
  Repose sur: D (Remplacement de la double négation), G (Double négation). Démontré dans: Les symétries des connecteurs.
2. Remplacement des équivalents. Si $\varphi \dashv\vdash \varphi'$ , alors $\neg\varphi \dashv\vdash \neg\varphi'$ , $(\varphi \rightarrow \psi) \dashv\vdash (\varphi' \rightarrow \psi)$ et $(\psi \rightarrow \varphi) \dashv\vdash (\psi \rightarrow \varphi')$ ; avec le lemme fondamental, de même des deux côtés de la négation conjointe, et de là, de la disjonction et de la conjonction. À la différence de la règle RDN, il admet des équivalents quelconques.
  Utilise: 6. Syllogisme hypothétique et échange, 10. Contraposition, 11. Lemme fondamental. Repose sur: E (Théorème de déduction). Démontré dans: Les symétries des connecteurs.
3. Formes équivalentes. $(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi)$ , avec deux applications de la règle RDN, une dans chaque copie que crée la négation extérieure ; $(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi)$ , par la double négation ; et $(\varphi \wedge \psi)$ est la même chaîne que $\neg(\varphi \rightarrow \neg\psi)$ .
  Repose sur: D (Remplacement de la double négation), G (Double négation). Démontré dans: Les symétries des connecteurs.
4. Les cinq symétries. $(\varphi \downarrow \psi) \dashv\vdash (\psi \downarrow \varphi)$ , par le lemme fondamental et la contraposition ; de celle-ci, successivement, les symétries de $\vee$ , $\wedge$ , $\leftrightarrow$ et $\veebar$ , chacune avec la précédente, transportée par le remplacement sous la négation quand il le faut.
  Utilise: 11. Lemme fondamental, 10. Contraposition. Repose sur: H (Remplacement des équivalents). Démontré dans: Les symétries des connecteurs.
Tronçon 4 Les règles classiques et les lois
- Démontrer avec des prémisses l’introduction et l’élimination de la disjonction et de la conjonction, le tiers exclu et la non-contradiction.
- Démontrer l’explosion, le raisonnement par l’absurde et le raisonnement par disjonction des cas avec des prémisses, et expliquer pourquoi ils ne suffisent pas sans elles.
- Démontrer par déduction les lois de De Morgan, leurs variantes et les lois de distributivité dans leurs deux sens.
- Transformer des formules en formes normales simples au moyen de chaînes d’équivalences justifiées.
1. Règles des connecteurs. Avec n’importe quel $\Gamma$ : de $\varphi$ découle $(\varphi \vee \psi)$ ; de $(\varphi \vee \psi)$ et $\neg\varphi$ , $\psi$ ; de $\varphi$ et $\psi$ , $(\varphi \wedge \psi)$ ; de $(\varphi \wedge \psi)$ , $\varphi$ et $\psi$ ; en outre, $\vdash (\varphi \vee \neg\varphi)$ et $\vdash \neg(\varphi \wedge \neg\varphi)$ .
  Utilise: 1. Système, déduction et identité, 2. Propriétés structurelles, 6. Syllogisme hypothétique et échange, 10. Contraposition, 13. Formes équivalentes, 14. Les cinq symétries. Repose sur: C (Axiomes de Łukasiewicz), E (Théorème de déduction), F (Du résultat à la règle), G (Double négation). Démontré dans: Les techniques de la logique classique.
2. Explosion et raisonnement par l’absurde. Si $\Gamma \vdash \varphi$ et $\Gamma \vdash \neg\varphi$ , alors $\Gamma \vdash \psi$ pour toute $\psi$ ; si $\Gamma \cup \{\neg\varphi\}$ déduit $\psi$ et $\neg\psi$ , alors $\Gamma \vdash \varphi$ ; et si $\Gamma \cup \{\varphi\}$ les déduit, $\Gamma \vdash \neg\varphi$ .
  Utilise: 1. Système, déduction et identité, 2. Propriétés structurelles, 15. Règles des connecteurs. Repose sur: C (Axiomes de Łukasiewicz), E (Théorème de déduction), G (Double négation). Démontré dans: Les techniques de la logique classique.
3. Raisonnement par disjonction des cas. Si $\Gamma \cup \{\varphi\} \vdash \psi$ et $\Gamma \cup \{\neg\varphi\} \vdash \psi$ , alors $\Gamma \vdash \psi$ ; et si $\Gamma \cup \{\varphi\} \vdash \chi$ , $\Gamma \cup \{\psi\} \vdash \chi$ et $\Gamma \vdash (\varphi \vee \psi)$ , alors $\Gamma \vdash \chi$ .
  Utilise: 2. Propriétés structurelles, 10. Contraposition, 15. Règles des connecteurs, 16. Explosion et raisonnement par l’absurde. Repose sur: E (Théorème de déduction). Démontré dans: Les techniques de la logique classique.
4. Lois de De Morgan. $\neg(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \vee \neg\psi)$ , par la définition et la double négation ; $\neg(\varphi \vee \psi) \dashv\vdash (\neg\varphi \wedge \neg\psi)$ , avec une application de la règle RDN dans chaque argument de la négation conjointe ; d’où $(\varphi \downarrow \psi) \dashv\vdash (\neg\varphi \wedge \neg\psi)$ et $\neg(\varphi \rightarrow \psi) \dashv\vdash (\varphi \wedge \neg\psi)$ .
  Repose sur: D (Remplacement de la double négation), G (Double négation), H (Remplacement des équivalents). Démontré dans: Lois de De Morgan et de distributivité.
5. Lois de distributivité. $(\varphi \wedge (\psi \vee \chi)) \dashv\vdash ((\varphi \wedge \psi) \vee (\varphi \wedge \chi))$ et $(\varphi \vee (\psi \wedge \chi)) \dashv\vdash ((\varphi \vee \psi) \wedge (\varphi \vee \chi))$ , chacune dans ses deux sens par disjonction des cas ; avec les symétries, aussi à droite.
  Utilise: 14. Les cinq symétries, 15. Règles des connecteurs, 17. Raisonnement par disjonction des cas. Repose sur: H (Remplacement des équivalents). Démontré dans: Lois de De Morgan et de distributivité.

Vers la sémantique. La chaîne s’arrête là où la déduction atteint toutes les techniques avec lesquelles raisonnent les mathématiques. Il reste à savoir si ce qui se déduit est exactement ce qui est vrai pour toute valuation : l’unité suivante définira la vérité, et la dernière comparera les deux notions.

Les abréviations des justifications

Les déductions de l’unité justifient chaque ligne par une abréviation, la même dans toutes les leçons. Elles sont réunies ici, ordonnées selon la leçon qui les introduit. « Prémisse » désigne une hypothèse de l’énoncé et, dans les déductions sur les déductions, une hypothèse de la règle que l’on démontre. Les nombres entre parenthèses citent les lignes auxquelles s’applique la règle ; une équivalence déjà démontrée se cite sans numéro quand on l’écrit comme ligne, et avec le numéro de la ligne qu’elle transforme quand on l’applique à cette ligne, y compris à l’une de ses parties avec « Rempl ».

Première leçon : A1, A2 et A3 (les schémas d’axiomes) ; MP $(i, j)$ (modus ponens) ; Déf (dépliage ou repliage d’une abréviation, avec le connecteur que l’on déplie : « Déf $\vee$ », « Déf $\dashv\vdash$ ») ; Id (identité, le théorème $\vdash (\varphi \rightarrow \varphi)$ ) ; Réfl (réflexivité : si $\varphi \in \Gamma$ , alors $\Gamma \vdash \varphi$ ) ; Mon (monotonie) ; Coupure (ce qui a été déduit peut servir de prémisse) ; Fin (finitude) ; TD (théorème de déduction) et RTD (sa réciproque).
Deuxième leçon : SH (syllogisme hypothétique) ; EP (échange des prémisses) ; DN (double négation) ; RDN $(i)$ (remplacement de la double négation dans la ligne $i$ ; RDN sans numéro cite l’équivalence entre une formule et celle qui en résulte par la règle) ; CP (contraposition, sous l’une quelconque de ses trois formes) ; « Résolu $n$ » (un résultat du problème résolu $n$ de la même leçon, écrit comme ligne).
Troisième leçon : LF (lemme fondamental, $(\varphi \downarrow \psi) \dashv\vdash \neg(\neg\varphi \rightarrow \psi)$ ) ; Rempl (remplacement des équivalents, sous l’une quelconque de ses formes, suivi de l’équivalence appliquée : « Rempl, DM $(i)$ ») ; Éq (formes équivalentes de la disjonction et de la conjonction, $(\varphi \vee \psi) \dashv\vdash (\neg\varphi \rightarrow \psi)$ et $(\varphi \wedge \psi) \dashv\vdash (\neg\varphi \downarrow \neg\psi)$ ) ; Sym (symétrie d’un connecteur).
Quatrième leçon : $\vee$ I et $\vee$ E (introduction et élimination de la disjonction) ; $\wedge$ I et $\wedge$ E (introduction et élimination de la conjonction) ; TE (tiers exclu) ; NC (non-contradiction ; l’abréviation nomme le théorème, mais ne justifie aucune ligne de l’unité) ; Exp (explosion) ; Cas $(i, j)$ et Cas $(i, j, k)$ (raisonnement par disjonction des cas, avec une formule et sa négation ou avec une disjonction) ; « Cas sans prémisses » (la disjonction des cas sans ensemble $\Gamma$ , qui n’apparaît que dans un problème) ; RA (raisonnement par l’absurde, sous ses deux formes).
Cinquième leçon : DM (lois de De Morgan) ; Dist (distributivité) ; Assoc (associativité de la disjonction) ; Instance $(i)$ (la ligne $i$ , qui vaut pour des formules quelconques, réécrite avec d’autres formules à la place de ses métavariables ; on indique la substitution).
Défis de cette leçon : M3 (le schéma que le troisième défi met à la place de A3).