Sémantique : synthèse et défis

Résumé

Cette leçon clôt l’unité consacrée à la sémantique. Elle reconstruit la chaîne déductive qui va de l’extension d’une valuation à toutes les formules et du lemme de coïncidence à la conséquence, à l’équivalence et à leurs deux théorèmes de travail, le remplacement et la substitution uniforme ; de là aux lois pour un nombre quelconque de termes, à la complétude fonctionnelle et aux systèmes de connecteurs, et de là aux formes normales, à leur algorithme et aux circuits, 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 pris aux précédentes, décide de trois manières un argument que le cours porte depuis la première unité et explique pourquoi la question que l’unité laisse ouverte, celle de savoir si ce qui est vrai pour toute valuation coïncide avec ce qui est dérivable, conduit à la métathéorie. Elle reprend dans son évaluation de sortie les compétences de l’évaluation d’entrée et se termine par six défis, plus difficiles que les problèmes des leçons, qui exigent de combiner les outils 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 l’extension récursive, le lemme de coïncidence, le remplacement sémantique et les lois généralisées conduisent à la complétude fonctionnelle, à l’existence des formes normales et à la correction et à la terminaison de leur algorithme.
Distinguer ce que l’unité a démontré de ce qu’elle a pris aux précédentes et de ce qu’elle a laissé à la métathéorie, en particulier la coïncidence de la conséquence sémantique avec la dérivabilité, et la compacité.
Résoudre des problèmes qui combinent le calcul avec des valeurs, la conséquence, la substitution uniforme, les systèmes de connecteurs, les formes normales et les circuits.

Ce que l’unité a accompli

L’unité s’est proposé de donner un sens aux formules du langage construit dans la première unité, sans toucher au système déductif de la deuxième, et de tirer de ce sens des procédés pour décider les questions que la logique pose à leur sujet : si une formule est valide, si elle est satisfaisable, si elle découle d’autres formules, si elle dit la même chose qu’une autre. Le dessein a été rempli avec quelques réserves, chacune déclarée à sa place : la bivalence et la vérifonctionnalité, qui ne se démontrent pas mais se choisissent, et dont la leçon sur la formalisation a montré le prix ; la lecture unique, la définition par récurrence, l’induction et les abréviations officielles, qui ont été démontrées ou fixées dans la première unité et sont utilisées ici ; et les faits indispensables sur les ensembles et les fonctions, qui ont été rappelés là où ils étaient nécessaires. Avec ces réserves, le chemin parcouru peut se lire comme une seule chaîne déductive en six tronçons, un par leçon.

La valeur d’une formule

La leçon sur la sémantique de la logique propositionnelle a défini une valuation comme une fonction des variables dans $\{0, 1\}$ et a démontré, avec le théorème de définition par récurrence sur les formules, qu’elle s’étend de manière unique à toutes les formules avec une seule clause : $v((\varphi \downarrow \psi)) = (1 - v(\varphi))(1 - v(\psi))$ . À partir des abréviations officielles elle a calculé, sans rien stipuler de plus, la valeur de chaque connecteur défini, écrite comme un polynôme en les valeurs des composantes, et avec elle la table de l’implication, qui est ici un théorème. Elle a démontré par induction sur la complexité le lemme de coïncidence, dont il découle que la table de vérité, avec ses $2^{n}$ lignes, contient tout ce que les valuations, en nombre infini, disent d’une formule à $n$ variables ; elle a défini la satisfaction, la validité, la satisfaisabilité, l’antilogie et la contingence, a précisé que $\not\models \varphi$ dit que $\varphi$ n’est pas valide et non qu’elle est une antilogie, a fixé $\top := (v_{1} \rightarrow v_{1})$ et $\bot := \neg\top$ , et a obtenu la décidabilité de la validité et de la satisfaisabilité, à un coût exponentiel que la recherche dirigée d’une valuation qui falsifie réduit sans l’éliminer.

Conséquence et équivalence

La leçon sur la conséquence et l’équivalence sémantiques a défini la conséquence à partir d’un ensemble de prémisses, fini ou infini, et a démontré qu’elle a les propriétés structurelles de la déduction (réflexivité, monotonie, coupure et transitivité), avec des preuves qui passent par les valuations au lieu de manipuler des lignes. Le théorème de déduction sémantique, $\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi)$ , s’est ramené à l’unique ligne fausse de l’implication, et la conséquence s’est ramenée à l’insatisfaisabilité : $\Gamma \models \varphi \Leftrightarrow \Gamma \cup \{\neg\varphi\}$ est insatisfaisable. L’équivalence sémantique, définie comme l’égalité des valeurs, s’est révélée coïncider avec la conséquence mutuelle et avec la validité de la double implication. Ses deux théorèmes de travail ont été démontrés par induction sur la complexité : le remplacement d’une occurrence d’une sous-formule par une autre équivalente, avec le cas de l’occurrence totale, qu’on ne peut pas omettre, et la substitution uniforme de formules quelconques aux variables, qui préserve la validité, l’équivalence et la conséquence. Grâce à eux, les lois du catalogue, vérifiées comme des identités entre polynômes, s’appliquent en tout endroit de n’importe quelle formule et peuvent s’enchaîner.

Lois pour un nombre quelconque de termes

La leçon sur les lois généralisées de De Morgan et de distributivité a défini par récurrence, en associant à gauche, la conjonction et la disjonction de $n$ formules, et a démontré par récurrence sur le nombre de termes le lemme de la valeur, qui dit qu’une conjonction est vraie si et seulement si tous ses termes le sont et une disjonction si et seulement si l’un d’eux l’est. Avec lui et avec la compatibilité des connecteurs avec l’équivalence, elle a obtenu l’associativité généralisée, démontrée par une chaîne d’équivalences afin qu’elle vaille aussi pour l’équivalence prouvable, l’indépendance de l’ordre et des répétitions, les lois de De Morgan généralisées et la distributivité généralisée, dont la récurrence sur deux indices a été organisée pour que l’hypothèse de récurrence couvre toutes les longueurs de la seconde liste ; la loi duale a été obtenue par De Morgan, sans répéter la double récurrence.

Fonctions de vérité

La leçon sur la complétude fonctionnelle a parcouru le chemin inverse, de la table à la formule. Elle a compté les fonctions de vérité à $n$ arguments, $2^{2^{n}}$ , a montré que chaque formule en représente exactement une et que deux formules sont équivalentes si et seulement si elles représentent la même, et a démontré le théorème de complétude fonctionnelle : la conjonction d’une ligne est vraie exactement sur sa ligne, et la disjonction des conjonctions des lignes où la fonction vaut $1$ la représente. Comme cette formule est une chaîne de cercles et de disques, la négation conjointe suffit à elle seule ; avec le critère de la négation conjointe, $\{\neg, \wedge\}$ , $\{\neg, \vee\}$ , $\{\neg, \rightarrow\}$ et la négation alternative suffisent aussi ; et avec le principe de clôture elle a démontré que toutes les formules de $\{\wedge, \vee, \rightarrow, \leftrightarrow\}$ préservent le $1$ , de sorte que ce système n’est pas complet.

Formes normales

La leçon sur les formes normales a choisi, dans chaque classe de formules équivalentes, des représentants de forme fixe. Elle a défini les littéraux, les clauses et les conjonctions élémentaires, et a démontré que la négation d’une forme normale est équivalente à sa duale, qui change chaque conjonction en disjonction et chaque littéral en son opposé. Elle a construit à partir de la table les formes canoniques, uniques une fois les variables fixées, et a démontré l’existence des deux formes normales de deux manières : par la table, comme corollaire de la complétude fonctionnelle, et par induction sur la complexité, avec le seul cas de la négation conjointe, qui équivaut à la conjonction des négations de ses composantes, et avec une hypothèse d’induction qui demande les deux formes à la fois, parce que la négation les échange. Elle a montré, enfin, que la validité d’une forme conjonctive et la satisfaisabilité d’une forme disjonctive se lisent d’un coup d’œil dans leurs paires complémentaires.

L’algorithme et les circuits

La leçon sur l’algorithme des formes normales et ses applications a converti la seconde preuve d’existence en un procédé qui agit sur des écritures : éliminer les connecteurs autres que $\neg$ , $\wedge$ et $\vee$ , faire descendre les négations jusqu’aux variables et distribuer. Elle a démontré sa correction avec le remplacement dans une écriture, qui adapte le théorème de remplacement aux abréviations, et sa terminaison avec trois mesures qui décroissent à chaque pas, dont la dernière lit la conjonction comme un produit ; elle a démontré, en outre, que la forme conjonctive de $\bigvee_{i=1}^{n} (p_i \wedge q_i)$ a nécessairement $2^{n}$ clauses, de sorte que la croissance n’est pas un défaut de l’algorithme. Elle a ensuite obtenu les formes normales d’une boîte noire à partir de sa table, les a raccourcies en fusionnant des lignes voisines et les a converties en circuits d’interrupteurs, dont la conduction est la valeur de leur formule.

La figure suivante réunit les six 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 preuve ; autour d’eux flottent les appuis, c’est-à-dire les principes et les outils 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 (la lecture unique avec la récurrence, l’induction et les abréviations officielles, de la première unité), qui sont dessinés comme des anneaux. Cliquer 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 l’induction et les valeurs des connecteurs sont les appuis les plus fréquentés de l’unité, et que le lemme de la valeur, bien qu’il soit démontré dans la troisième leçon, soutient presque tout ce que les trois dernières disent des conjonctions et des disjonctions.

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'$ ; c’est pourquoi 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. Cela a été démontré dans la première unité. Admis sans démonstration dans cette unité.
BInduction. Simple et forte sur les entiers naturels, et sur la complexité des formules, dont les seuls cas sont les variables et la négation conjointe $(\varphi \downarrow \psi)$ . Cela a été démontré dans la première unité. Admis sans démonstration dans cette unité.
CAbréviations officielles. $\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)$ . Elles ont été fixées dans la première unité. Admis sans démonstration dans cette unité.
DValeurs des connecteurs. Avec $a = v(\varphi)$ et $b = v(\psi)$ : $v(\neg\varphi) = 1 - a$ , $v((\varphi \vee \psi)) = a + b - ab$ , $v((\varphi \wedge \psi)) = ab$ , $v((\varphi \rightarrow \psi)) = 1 - a(1 - b)$ , $v((\varphi \leftrightarrow \psi)) = ab + (1 - a)(1 - b)$ et $v((\varphi \veebar \psi)) = a + b - 2ab$ , où $a^{2} = a$ . Établi dans: 1. Extension d’une valuation.
ELemme de coïncidence. Si deux valuations s’accordent sur les variables de $\varphi$ , elles donnent à $\varphi$ la même valeur ; c’est pourquoi la table à $2^{n}$ lignes dit tout. Établi dans: 2. Lemme de coïncidence et tables.
FRemplacement sémantique. Si $\theta \eqsem \theta'$ et que $\chi'$ résulte du remplacement dans $\chi$ d’une occurrence de $\theta$ par $\theta'$ , alors $\chi \eqsem \chi'$ . Établi dans: 7. Théorème de remplacement sémantique.
GLois d’équivalence. Double négation, idempotence, commutativité, associativité, distributivité, De Morgan, absorption, identité, domination, tiers exclu et non-contradiction, pour des formules quelconques. Établi dans: 9. Lois d’équivalence.
HLemme de la valeur. $v\left( \bigwedge_{i=1}^{n} \varphi_i \right) = 1$ si et seulement si $v(\varphi_i) = 1$ pour tout $i$ ; $v\left( \bigvee_{i=1}^{n} \varphi_i \right) = 1$ si et seulement si $v(\varphi_i) = 1$ pour un certain $i$ . Établi dans: 10. Lemme de la valeur et compatibilité.

Tronçon 1 La valeur d’une formule
- Calculer la valeur d’une formule avec la clause de la négation conjointe et déduire des abréviations celle de chaque connecteur défini.
- Démontrer le lemme de coïncidence et justifier avec lui qu’une table à $2^{n}$ lignes suffit.
- Classer des formules et des ensembles sans confondre $\not\models \varphi$ avec l’antilogie, et décider la validité en cherchant une valuation qui falsifie.
1. Extension d’une valuation. Chaque valuation $v$ s’étend de manière unique à toutes les formules avec la clause $v((\varphi \downarrow \psi)) = (1 - v(\varphi))(1 - v(\psi))$ ; en dépliant les abréviations on calcule la valeur de $\neg$ , $\vee$ , $\wedge$ , $\rightarrow$ , $\leftrightarrow$ et $\veebar$ .
  Repose sur: A (Lecture unique et récurrence), C (Abréviations officielles). Démontré dans: Sémantique de la logique propositionnelle.
2. Lemme de coïncidence et tables. Si $v$ et $v'$ s’accordent sur $V(\varphi)$ , alors $v(\varphi) = v'(\varphi)$ , par induction sur la complexité ; c’est pourquoi les valeurs de $\varphi$ pour toutes les valuations sont exactement celles des $2^{n}$ lignes de sa table.
  Utilise: 1. Extension d’une valuation. Repose sur: B (Induction). Démontré dans: Sémantique de la logique propositionnelle.
3. Classification et décision. Toute formule est exactement l’une de trois choses : valide, contingente ou antilogie ; $\varphi$ est valide si et seulement si $\neg\varphi$ est une antilogie, et c’est une antilogie si et seulement si $\models \neg\varphi$ . $\top$ et le tiers exclu sont valides, $\bot$ est une antilogie, et la validité et la satisfaisabilité se décident en parcourant les lignes.
  Repose sur: D (Valeurs des connecteurs), E (Lemme de coïncidence). Démontré dans: Sémantique de la logique propositionnelle.
Tronçon 2 Conséquence et équivalence
- Décider des conséquences à partir d’ensembles finis ou infinis, en exhibant un contre-modèle ou en démontrant qu’il n’en existe pas.
- Appliquer le théorème de déduction sémantique et la réduction de la conséquence à l’insatisfaisabilité.
- Distinguer le remplacement d’une occurrence de la substitution uniforme, et démontrer l’un et l’autre par induction sur la complexité.
- Établir des équivalences par des chaînes, en nommant correctement chaque loi.
1. La conséquence et ses propriétés. $\Gamma \models \varphi$ si toute valuation qui satisfait $\Gamma$ satisfait $\varphi$ ; $\emptyset \models \varphi$ si et seulement si $\models \varphi$ ; la réflexivité, la monotonie, la coupure et la transitivité sont vérifiées, et un ensemble insatisfaisable a pour conséquence toute formule.
  Utilise: 3. Classification et décision. Démontré dans: Conséquence et équivalence sémantiques.
2. Déduction sémantique et insatisfaisabilité. $\Gamma \cup \{\varphi\} \models \psi \Leftrightarrow \Gamma \models (\varphi \rightarrow \psi)$ , par l’unique ligne fausse de l’implication ; $\{\varphi_1, \ldots, \varphi_n\} \models \psi \Leftrightarrow\; \models (\varphi_1 \rightarrow (\varphi_2 \rightarrow \cdots (\varphi_n \rightarrow \psi) \cdots))$ ; et $\Gamma \models \varphi$ si et seulement si $\Gamma \cup \{\neg\varphi\}$ est insatisfaisable.
  Utilise: 4. La conséquence et ses propriétés. Repose sur: D (Valeurs des connecteurs). Démontré dans: Conséquence et équivalence sémantiques.
3. Équivalence sémantique. $\varphi \eqsem \psi$ si et seulement si $\varphi \models \psi$ et $\psi \models \varphi$ , si et seulement si $\models (\varphi \leftrightarrow \psi)$ ; l’équivalence est réflexive, symétrique et transitive, et deux formules équivalentes sont interchangeables comme prémisses et comme conclusions.
  Utilise: 4. La conséquence et ses propriétés. Repose sur: D (Valeurs des connecteurs). Démontré dans: Conséquence et équivalence sémantiques.
4. Théorème de remplacement sémantique. Si $\theta \eqsem \theta'$ , remplacer dans $\chi$ une occurrence de $\theta$ par $\theta'$ , l’occurrence totale comprise, donne une formule équivalente à $\chi$ ; et de même remplacer toutes les occurrences à la fois.
  Utilise: 1. Extension d’une valuation, 6. Équivalence sémantique. Repose sur: A (Lecture unique et récurrence), B (Induction). Démontré dans: Conséquence et équivalence sémantiques.
5. Substitution uniforme. Si $w(v_n) = v(\sigma(v_n))$ , alors $v(\sigma(\chi)) = w(\chi)$ ; c’est pourquoi, si $\models \chi$ , on a aussi $\models \sigma(\chi)$ , et la substitution préserve l’équivalence et la conséquence, mais non la satisfaisabilité ni la contingence.
  Utilise: 1. Extension d’une valuation, 4. La conséquence et ses propriétés, 6. Équivalence sémantique. Repose sur: A (Lecture unique et récurrence), B (Induction). Démontré dans: Conséquence et équivalence sémantiques.
6. Lois d’équivalence. Les lois du catalogue se vérifient comme des identités entre polynômes avec $a^{2} = a$ ; avec le remplacement et la transitivité, elles s’appliquent aux sous-formules et s’enchaînent.
  Utilise: 3. Classification et décision, 6. Équivalence sémantique. Repose sur: D (Valeurs des connecteurs), F (Remplacement sémantique). Démontré dans: Conséquence et équivalence sémantiques.
Tronçon 3 Lois pour un nombre quelconque de termes
- Déplier des conjonctions et des disjonctions de $n$ termes comme des chaînes associées à gauche et calculer leur valeur.
- Démontrer par récurrence sur le nombre de termes l’associativité généralisée, l’indépendance de l’ordre et les lois de De Morgan généralisées.
- Démontrer la distributivité généralisée par une récurrence sur deux indices, et compter les termes qu’elle produit.
1. Lemme de la valeur et compatibilité. Si $\alpha \eqsem \alpha'$ et $\beta \eqsem \beta'$ , alors $\neg\alpha \eqsem \neg\alpha'$ , $(\alpha \wedge \beta) \eqsem (\alpha' \wedge \beta')$ et $(\alpha \vee \beta) \eqsem (\alpha' \vee \beta')$ ; une conjonction de $n$ termes vaut $1$ si et seulement si tous ses termes valent $1$ , une disjonction si et seulement si l’un d’eux vaut $1$ , et des termes équivalents donnent des conjonctions et des disjonctions équivalentes.
  Utilise: 6. Équivalence sémantique. Repose sur: D (Valeurs des connecteurs), B (Induction). Démontré dans: Lois généralisées de De Morgan et de distributivité.
2. Associativité et ordre. La conjonction des conjonctions de deux listes est équivalente à celle de leur concaténation, et tout regroupement est équivalent au regroupement associé à gauche ; deux listes ayant les mêmes termes donnent des conjonctions et des disjonctions équivalentes, quels que soient l’ordre et les répétitions.
  Repose sur: H (Lemme de la valeur), G (Lois d’équivalence), B (Induction). Démontré dans: Lois généralisées de De Morgan et de distributivité.
3. Lois de De Morgan généralisées. $\neg \bigwedge_{i=1}^{n} \varphi_i \eqsem \bigvee_{i=1}^{n} \neg\varphi_i$ et $\neg \bigvee_{i=1}^{n} \varphi_i \eqsem \bigwedge_{i=1}^{n} \neg\varphi_i$ , en appliquant la loi binaire à la dernière jonction et l’hypothèse de récurrence à ce qui reste à l’intérieur.
  Repose sur: H (Lemme de la valeur), G (Lois d’équivalence), B (Induction). Démontré dans: Lois généralisées de De Morgan et de distributivité.
4. Distributivité généralisée. $\left( \bigvee_{i=1}^{n} \varphi_i \right) \wedge \left( \bigvee_{j=1}^{m} \psi_j \right) \eqsem \bigvee_{i,j} (\varphi_i \wedge \psi_j)$ , avec $nm$ termes dans l’ordre lexicographique ; et sa duale, qui distribue la disjonction de deux conjonctions, par De Morgan.
  Utilise: 11. Associativité et ordre, 12. Lois de De Morgan généralisées. Repose sur: H (Lemme de la valeur), G (Lois d’équivalence), B (Induction). Démontré dans: Lois généralisées de De Morgan et de distributivité.
Tronçon 4 Fonctions de vérité
- Compter les fonctions de vérité et décider l’équivalence en comparant les fonctions que représentent deux formules.
- Construire la formule d’une table et écrire n’importe quelle fonction avec la seule négation conjointe.
- Démontrer qu’un système de connecteurs est complet avec le critère de la négation conjointe, ou qu’il ne l’est pas avec une propriété que ses formules préservent.
1. Fonctions de vérité. Il y a $2^{2^{n}}$ fonctions de vérité à $n$ arguments ; une formule à variables parmi $v_1, \ldots, v_n$ en représente exactement une, $f_\varphi$ , et $\varphi \eqsem \psi \Leftrightarrow f_\varphi = f_\psi$ .
  Utilise: 6. Équivalence sémantique. Repose sur: E (Lemme de coïncidence). Démontré dans: Complétude fonctionnelle.
2. Complétude fonctionnelle. La conjonction d’une ligne vaut $1$ exactement sur sa ligne ; la disjonction des conjonctions des lignes où $f$ vaut $1$ , ou $(v_{1} \wedge \neg v_{1})$ s’il n’y en a aucune, représente $f$ ; et toute formule est équivalente à la formule de sa table.
  Utilise: 14. Fonctions de vérité. Repose sur: H (Lemme de la valeur), D (Valeurs des connecteurs). Démontré dans: Complétude fonctionnelle.
3. Systèmes complets et incomplets. La négation conjointe suffit, parce que les abréviations se déplient ; si les formules de $K$ expriment la valeur $(1 - a)(1 - b)$ , $K$ est un système complet, et $\{\neg, \wedge\}$ , $\{\neg, \vee\}$ , $\{\neg, \rightarrow\}$ et $\{\uparrow\}$ le sont donc aussi ; les formules de $\{\wedge, \vee, \rightarrow, \leftrightarrow\}$ valent $1$ quand toutes les variables valent $1$ , et ce système n’est pas complet.
  Utilise: 15. Complétude fonctionnelle. Repose sur: C (Abréviations officielles), B (Induction), D (Valeurs des connecteurs). Démontré dans: Complétude fonctionnelle.
Tronçon 5 Formes normales
- Reconnaître les littéraux, les clauses et les formes normales, en distinguant la forme de la chaîne de son sens.
- Construire les formes canoniques à partir de la table et démontrer leur unicité.
- Démontrer par induction l’existence des formes normales, avec l’hypothèse d’induction qui demande les deux.
- Décider d’un coup d’œil la validité d’une forme conjonctive et la satisfaisabilité d’une forme disjonctive.
1. Littéraux et dualité. $\neg\ell \eqsem \ell^{*}$ ; une conjonction élémentaire est satisfaisable si et seulement si elle ne contient aucune paire complémentaire, et une clause est valide si et seulement si elle en contient une ; la négation d’une forme normale est équivalente à sa duale, de sorte que la forme conjonctive de $\varphi$ est la duale de la forme disjonctive de $\neg\varphi$ .
  Utilise: 12. Lois de De Morgan généralisées. Repose sur: G (Lois d’équivalence), F (Remplacement sémantique), H (Lemme de la valeur). Démontré dans: Formes normales.
2. Formes canoniques. Si $\varphi$ est satisfaisable, elle est équivalente à sa forme canonique disjonctive, et si elle n’est pas valide, à la conjonctive ; une fois fixées les variables $v_1, \ldots, v_n$ , deux formes canoniques sont équivalentes si et seulement si elles sont la même chaîne, et deux formules satisfaisables sont équivalentes si et seulement si elles ont la même forme canonique disjonctive.
  Utilise: 15. Complétude fonctionnelle, 17. Littéraux et dualité. Repose sur: H (Lemme de la valeur), E (Lemme de coïncidence). Démontré dans: Formes normales.
3. Existence par induction. $(\varphi \downarrow \psi) \eqsem (\neg\varphi \wedge \neg\psi)$ ; les formes normales se conservent par conjonction et par disjonction, la forme disjonctive d’une conjonction et la forme conjonctive d’une disjonction par la distributivité généralisée ; par induction, avec l’hypothèse d’induction pour les deux formes, toute formule a une forme disjonctive et une forme conjonctive.
  Utilise: 17. Littéraux et dualité, 11. Associativité et ordre, 13. Distributivité généralisée. Repose sur: B (Induction), F (Remplacement sémantique). Démontré dans: Formes normales.
4. Ce qui se voit d’un coup d’œil. Une forme conjonctive est valide si et seulement si chaque clause contient une paire complémentaire ; une forme disjonctive est satisfaisable si et seulement si une conjonction élémentaire n’en contient aucune.
  Utilise: 17. Littéraux et dualité. Repose sur: H (Lemme de la valeur). Démontré dans: Formes normales.
Tronçon 6 L’algorithme et les circuits
- Appliquer l’algorithme de réécriture et choisir l’élimination de la double implication qui convient.
- Démontrer sa correction et sa terminaison, et expliquer pourquoi la forme conjonctive peut croître de manière exponentielle.
- Obtenir et simplifier les formes normales d’une boîte noire, et concevoir avec elles des circuits d’interrupteurs.
1. Correction et terminaison de l’algorithme. Remplacer une sous-écriture par une autre équivalente donne une écriture équivalente ; chaque règle est une équivalence, et une écriture irréductible est une forme normale regroupée d’une certaine manière ; les mesures $M_1$ , $M_2$ , avec $M_2(\neg\varphi) = 2^{M_2(\varphi)}$ , et $M_3$ , avec $M_3(\varphi \wedge \psi) = M_3(\varphi)\,M_3(\psi)$ , décroissent à chaque pas.
  Utilise: 19. Existence par induction, 11. Associativité et ordre. Repose sur: G (Lois d’équivalence), D (Valeurs des connecteurs), B (Induction). Démontré dans: L’algorithme des formes normales et ses applications.
2. Croissance exponentielle. $\bigvee_{i=1}^{n} (p_i \wedge q_i)$ est équivalente à une forme conjonctive à $2^{n}$ clauses, et toute forme conjonctive équivalente a au moins $2^{n}$ clauses non valides.
  Utilise: 19. Existence par induction, 17. Littéraux et dualité. Repose sur: H (Lemme de la valeur). Démontré dans: L’algorithme des formes normales et ses applications.
3. Lignes voisines et circuits. $(\kappa \wedge \ell) \vee (\kappa \wedge \ell^{*}) \eqsem \kappa$ et sa duale ; un circuit série-parallèle conduit dans l’état $v$ si et seulement si $v(\varphi_C) = 1$ , et toute fonction de vérité est réalisée par un circuit.
  Utilise: 15. Complétude fonctionnelle, 18. Formes canoniques, 17. Littéraux et dualité, 11. Associativité et ordre. Repose sur: G (Lois d’équivalence), F (Remplacement sémantique), D (Valeurs des connecteurs), B (Induction). Démontré dans: L’algorithme des formes normales et ses applications.

Vers la métathéorie. La chaîne s’arrête là où la sémantique atteint un procédé pour chaque question sur les formules. Il reste à savoir si ce qui est vrai pour toute valuation est exactement ce qui se déduit dans le système : la prochaine unité comparera les deux notions.