Plan d’études de Logique mathématique I

Propos

Tous les cours de mathématiques exigent de démontrer, et tous ceux de philosophie exigent d’argumenter ; or aucun d’eux ne fait du raisonnement lui-même son objet, et tous tiennent pour entendu ce que signifie qu’une conclusion suive de prémisses. Ce cours prend cette question pour sujet. Son propos est de construire, pour le langage le plus simple de la logique, la première théorie mathématique complète dont l’objet est le raisonnement, avec ses quatre pièces en vue : un langage, dont les formules se reconnaissent et se lisent sans ambiguïté ; un calcul, qui produit des déductions sans égard à la signification des symboles ; une signification, qui attribue à chaque formule sa valeur de vérité sous chaque valuation de ses variables ; et la démonstration que le calcul et la signification coïncident.

S’il en est ainsi, le cours n’est pas une collection de règles pour manipuler des symboles, mais une théorie dotée d’un résultat central, le théorème de complétude, que tout ce qui précède prépare. Pour un ensemble de formules $\Gamma$ et une formule $\varphi$, la déductibilité $\Gamma \vdash \varphi$ dit qu’il existe une suite finie de formules, construite avec des axiomes et des règles, qui se termine par $\varphi$ ; la conséquence sémantique $\Gamma \models \varphi$ dit que toute valuation qui rend vraies les formules de $\Gamma$ rend vraie $\varphi$. Les deux relations naissent d’idées opposées, l’une syntaxique et existentielle, l’autre sémantique et universelle ; le cours démontre pourtant que $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$. Il s’ensuit que chaque question sur ce qui suit de prémisses peut recevoir une réponse du côté le plus facile : en exhibant une déduction, en parcourant une table ou, comme l’enseigne la dernière leçon de contenu, en réfutant par résolution.

Public et connaissances préalables

Le cours s’adresse à qui commence des études de mathématiques, d’informatique ou de philosophie, et à qui, à n’importe quelle étape de sa formation, veut savoir avec exactitude ce qu’est une démonstration et pourquoi on peut s’y fier : étudiants qui s’initient aux mathématiques universitaires et butent sur les démonstrations, étudiants en informatique qui ont besoin de la logique des circuits, des programmes et des problèmes de satisfaisabilité, et étudiants en philosophie qui veulent passer de la logique des raisonnements à sa théorie.

C’est un cours de niveau 1, sans prérequis et autonome. Il ne suppose ni d’avoir étudié la logique, ni de connaître la théorie des ensembles, ni d’avoir jamais démontré un théorème. Ce qu’il utilise des ensembles (appartenance, inclusion, réunion, ensembles de formules), des fonctions (une valuation est une fonction des variables dans $\{0, 1\}$), des chaînes de symboles et du raisonnement inductif, il l’enseigne là où il en a besoin : les ensembles et les chaînes, dans la leçon de l’unité 1 sur le langage, et la récurrence et l’induction, dans la leçon suivante, avant de s’en servir. Il ne suppose que deux choses : lire avec attention, car dans un langage formel un symbole ajouté ou omis change la chaîne, et l’arithmétique élémentaire des entiers naturels, qui dans ce cours, comme dans le reste du site, commencent à $1$.

Où il mène

De ce qui précède suit la place du cours dans le site. Il n’a pas de prérequis et il est l’aboutissement de trois parcours d’études, Mathématiques, Informatique et Philosophie, parce que dans les trois le raisonnement est à la fois instrument et objet. Il a trois cours complémentaires, qui peuvent se suivre avant, en parallèle ou après, dans n’importe quel ordre. Logique aristotélicienne étudie la logique des termes et le syllogisme, dont la validité dépend de mots comme « tout » et « quelque », que ce cours laisse de côté, et montre de quelle tradition on est parvenu au calcul. Algèbre et géométrie I élève un édifice déductif à partir des axiomes de Peano, et met en pratique, sur les nombres, la méthode axiomatique et l’induction que ce cours étudie comme objet ; son plan recommande d’avoir étudié ce cours auparavant, ou de l’étudier en parallèle. Programmation en C++ I, enfin, met en pratique ce qui est ici théorie : décider si une chaîne est bien formée, parcourir une table de vérité, calculer une forme normale ou chercher une réfutation sont des procédures qui peuvent s’écrire comme des programmes.

Or le cours laisse ouverte une question d’expression : son langage ne peut dire ni « tout » ni « quelque », et la formalisation des raisonnements du français perd, dès l’unité 1, les quantificateurs. Par conséquent, sa suite prévue est la Logique mathématique II, consacrée à la logique des prédicats, qui parcourra le même chemin avec des quantificateurs et des variables qui parcourent des objets : elle conservera la correction, la complétude et la compacité, avec des méthodes que ce cours anticipe, mais en elle la conséquence cessera d’être décidable.

Objectifs d’apprentissage globaux

Les objectifs suivants décrivent ce que doit savoir faire qui achève le cours. Chacun est formulé comme une performance observable, de sorte qu’il puisse se vérifier par une tâche concrète ; chaque leçon de contenu déclare à son tour ses propres objectifs, qui servent un ou plusieurs des objectifs globaux, et la leçon de clôture montre dans quelles unités et leçons chacun est travaillé. Les sept objectifs sont numérotés afin de pouvoir être cités.

1. Objectif 1. Distinguer le langage objet du métalangage, et décider avec les règles de formation si une chaîne est une formule.
2. Objectif 2. Formaliser des énoncés et des raisonnements du langage naturel, en indiquant ce que la formalisation conserve et ce qu’elle perd.
3. Objectif 3. Construire des déductions dans le système du cours (les axiomes de Łukasiewicz, le modus ponens et le remplacement de la double négation), en combinant axiomes, règles primitives et règles dérivées.
4. Objectif 4. Démontrer des métathéorèmes par récurrence sur les entiers naturels et par induction sur la complexité des formules et sur la longueur des déductions.
5. Objectif 5. Décider la validité, la satisfaisabilité, la conséquence et l’équivalence sémantiques, avec des tables de vérité et avec des équivalences.
6. Objectif 6. Transformer des formules en formes normales et exprimer avec elles des fonctions de vérité et des circuits.
7. Objectif 7. Expliquer et appliquer la correction, la complétude et la compacité, et décider l’insatisfaisabilité par résolution.

Les objectifs 3 et 7 ont chacun leur unité, la déduction et la métathéorie ; les objectifs 5 et 6 se partagent l’unité de sémantique, le premier dans sa première moitié, le second dans la seconde. L’objectif 2 a une leçon propre, celle de la formalisation, et s’exerce ensuite chaque fois qu’un problème est posé en mots. Les objectifs 1 et 4, en revanche, sont transversaux : la distinction entre ce qui se dit dans le langage et ce qui se dit sur lui traverse les quatre unités, et le raisonnement inductif est la forme de toutes les démonstrations importantes du cours, de la lecture unique des formules jusqu’à la correction du système et au lemme de Kalmár. Il s’ensuit que leur réussite ne peut être attribuée à une seule leçon, et qu’il convient de les cultiver tout au long du cours.

Le système du cours et ses décisions

Un cours de logique propositionnelle peut se construire de bien des manières, et les textes habituels diffèrent par le langage, par les connecteurs primitifs et par le système déductif. Ce cours prend trois décisions qu’il convient de connaître dès le début, car elles expliquent ce qui, à première vue, peut sembler étrange.

Une langue de cercles et de disques

Le langage du cours a un alphabet de deux symboles seulement, le cercle $\sigO$ et le disque $\sigI$. La $n$-ième variable est la chaîne de $n$ cercles suivis d’un disque, $v_{n} = \sigO^{n}\sigI$, de sorte que $v_{1} = \sigO\sigI$ et $v_{2} = \sigO\sigO\sigI$ ; et il y a une seule règle de formation : si $\varphi$ et $\psi$ sont des formules, $\sigI\varphi\psi$ en est une aussi, qui s’abrège $(\varphi \downarrow \psi)$ et se lit « ni $\varphi$ ni $\psi$ ». La négation conjointe $\downarrow$ est donc l’unique connecteur primitif, et tous les autres sont des abréviations définies une seule fois : $\neg\varphi$ est $(\varphi \downarrow \varphi)$, la disjonction $(\varphi \vee \psi)$ est $\neg(\varphi \downarrow \psi)$, et à partir d’elles se définissent la conjonction, l’implication, la double implication et la disjonction exclusive. Toute autre manière de les écrire est un théorème, qui se démontre, et non une définition.

Le choix a un prix, la lisibilité, que le cours paie dans le métalangage : personne n’écrit au quotidien des chaînes de cercles et de disques, mais leurs noms abrégés, dépliables à tout moment jusqu’à la chaîne qu’ils désignent. Or il rapporte à maintes reprises. Deux symboles suffisent pour une infinité de variables, de sorte que toute formule est une chaîne finie sur un alphabet de deux éléments. Le connecteur s’écrit devant ses arguments, et c’est pourquoi les parenthèses ne sont pas nécessaires : la lecture unique se démontre par un argument de poids, qui attribue $+1$ à chaque variable et $-1$ à chaque disque connecteur. Et comme toute formule composée est une négation conjointe, chaque démonstration par induction sur la complexité n’a qu’un seul cas composé, ce qui abrège toutes celles des unités suivantes. Qu’un seul connecteur suffise pour exprimer n’importe quel autre ne se suppose pas : l’unité de sémantique le démontre.

Une seconde règle primitive

Le système déductif part de celui de Jan Łukasiewicz : trois schémas d’axiomes, écrits avec la négation et l’implication, et le modus ponens comme règle unique. Ces schémas furent formulés pour des langages dont les connecteurs primitifs sont la négation et l’implication ; dans la langue de cercles et de disques, une formule comme $(v_{1} \downarrow v_{2})$ n’est ni l’une ni l’autre, et elle est opaque pour les axiomes. La première leçon de l’unité de déduction démontre, au moyen d’une marque que tous les axiomes possèdent, que le modus ponens conserve et que la formule ne possède pas, que le système de Łukasiewicz ne déduit pas $((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1})$.

S’il en est ainsi, le système doit être complété, et le remède naturel semble être de démontrer la double négation, $\varphi \dashv\vdash \neg\neg\varphi$, que la deuxième leçon déduit des trois schémas. La marque montre que cela ne suffit pas : les théorèmes de la double négation la conservent et, pourtant, même avec eux on n’échange pas $v_{1}$ contre $\neg\neg v_{1}$ à l’intérieur d’une négation conjointe. Par conséquent, après avoir démontré la double négation, la deuxième leçon ajoute une seconde règle primitive, le remplacement de la double négation : d’une formule $\chi$ on infère celle qui résulte d’y remplacer une occurrence d’une sous-formule $\theta$ par $\neg\neg\theta$, ou une occurrence de $\neg\neg\theta$ par $\theta$. Le système du cours se compose donc des trois schémas de Łukasiewicz, du modus ponens et de cette règle.

D’autres systèmes pour la négation conjointe obtiennent le même résultat avec des schémas d’axiomes faits sur mesure. Le cours préfère une règle pour deux raisons : elle est plus simple encore que le modus ponens, car elle prend une seule ligne et change une seule occurrence, et elle n’a rien d’artificiel, car elle exprime ce que la double négation dit déjà, que $\theta$ et $\neg\neg\theta$ sont interchangeables, étendu à tout endroit d’une formule. Elle est en outre correcte, car elle conserve la valeur de vérité de chaque ligne, et elle préserve le théorème de la déduction, avec un cas de plus dans sa démonstration. Qu’elle suffise pour déduire tout ce qui doit être déduit, c’est le théorème de complétude de la dernière unité.

La compacité avant la complétude forte

La complétude admet trois degrés : la faible dit que toute tautologie est un théorème ; la finie, que toute conséquence d’un ensemble fini de prémisses se déduit de lui ; la forte, que la même chose vaut pour un ensemble quelconque, même infini. La méthode du cours, le lemme de Kalmár, travaille avec les variables, en nombre fini, d’une formule et avec des prémisses finies, et c’est pourquoi elle atteint les deux premiers degrés et non le troisième. Pour y parvenir, il suffit que, si $\Gamma \models \varphi$, une partie finie $\Gamma_{0}$ de $\Gamma$ satisfasse déjà $\Gamma_{0} \models \varphi$ ; or c’est précisément ce qu’affirme le théorème de compacité.

Beaucoup de textes démontrent d’abord la complétude forte par une autre méthode et en déduisent la compacité. Dans ce cours, en revanche, la complétude forte est ce que l’on cherche, et obtenir la compacité à partir d’elle serait circulaire. D’où l’ordre s’inverse : la leçon sur la compacité la démontre à l’intérieur de la sémantique, sans mentionner aucune déduction, en fixant une à une les valeurs de $v_{1}, v_{2}, \ldots$, et ce n’est qu’ensuite, en trois lignes, qu’elle obtient la complétude forte, c’est-à-dire $\Gamma \models \varphi \Rightarrow \Gamma \vdash \varphi$ pour tout ensemble $\Gamma$.

Contenus

Le cours s’organise en six unités : cette présentation, quatre unités de contenu et une clôture. Chaque unité de contenu s’ouvre par une leçon d’introduction, qui présente ses leçons, sa place dans le cours, ce qu’elle tient pour connu et le problème qu’elle résout, et qui commence par une évaluation d’entrée ; elle se ferme par une leçon de synthèse, qui reconstruit la chaîne déductive de l’unité, la relie au reste du cours, reprend dans une évaluation de sortie les compétences de celle d’entrée et propose six défis d’une difficulté supérieure à celle des problèmes des leçons.

Unité 0. Présentation du cours

Elle se compose de cette leçon, qui fixe le propos, les objectifs globaux, les décisions, les contenus, la charge de travail et la conception du cours.

Unité 1. Langage

Son objectif est de construire le langage que le cours étudie, de démontrer que chaque formule se lit d’une seule manière et de le relier aux raisonnements du français.

1. Langage : introduction.
2. Qu’est-ce que la logique mathématique : la validité face à la vérité, le contre-exemple, les paradoxes et la distinction entre langage objet et métalangage.
3. Le langage de la logique propositionnelle : ensembles et chaînes, la langue de cercles et de disques, sa règle de formation et ses abréviations.
4. Récurrence sur les entiers et induction sur les formules : récurrence simple et forte, induction structurelle, le lemme du poids, la lecture unique et les définitions par récurrence.
5. Formalisation du langage naturel : le dictionnaire, la traduction d’énoncés et de raisonnements, et ce que perd l’implication matérielle.
6. Langage : synthèse et défis.

Unité 2. Déduction

Son objectif est de donner au langage un calcul, le système du cours, et d’y dériver, une seule fois chacune, les manières de raisonner que les mathématiques utilisent sans les nommer.

1. Déduction : introduction.
2. Systèmes déductifs formels : le système de Łukasiewicz, la déduction avec prémisses, le théorème de la déduction et la marque qui en montre la limite.
3. Quatre techniques de déduction : le syllogisme hypothétique, l’échange des prémisses, la double négation, la contraposition et le remplacement de la double négation.
4. Les symétries des connecteurs : le lemme fondamental de la négation conjointe, le remplacement des équivalents, les formes équivalentes de la disjonction et de la conjonction et leurs cinq symétries.
5. Les techniques de la logique classique : les règles de chaque connecteur, le tiers exclu, la preuve par cas et la réduction à l’absurde, avec prémisses.
6. Lois de De Morgan et de distributivité : leurs démonstrations dans les deux sens et le remplacement des équivalents à l’intérieur d’autres formules.
7. Déduction : synthèse et défis.

Unité 3. Sémantique

Son objectif est de donner aux formules une signification, de décider avec elle la validité et la conséquence, et de réduire toute formule à des formes normales.

1. Sémantique : introduction.
2. Sémantique de la logique propositionnelle : les valuations et leur prolongement par récurrence, le lemme de coïncidence, les tables de vérité, la validité et la satisfaisabilité.
3. Conséquence et équivalence sémantiques : la conséquence à partir d’ensembles, le théorème de la déduction sémantique, le remplacement sémantique et la substitution uniforme.
4. Lois généralisées de De Morgan et de distributivité : conjonctions et disjonctions de $n$ termes et leurs lois, par récurrence.
5. Complétude fonctionnelle : toute fonction de vérité a une formule, la négation conjointe suffit à elle seule, et les systèmes complets de connecteurs.
6. Formes normales : littéraux, clauses, formes disjonctive et conjonctive, leur dualité et leur existence.
7. L’algorithme des formes normales et ses applications : un algorithme correct et qui termine, et la conception et la simplification de circuits d’interrupteurs.
8. Sémantique : synthèse et défis.

Unité 4. Métathéorie

Son objectif est de démontrer que la déduction et la conséquence coïncident, d’abord pour des prémisses finies, puis pour des prémisses quelconques, et d’offrir un troisième moyen de les décider.

1. Métathéorie : introduction.
2. Correction et complétude : la correction par récurrence sur les lignes, la cohérence, le lemme de Kalmár et la complétude faible et finie.
3. Le théorème de compacité : sa démonstration sémantique, ses formes équivalentes, la complétude forte qui en découle et ses applications combinatoires.
4. La méthode de résolution : la forme clausale, la règle de résolution, sa correction et sa complétude pour la réfutation, et son coût.
5. Métathéorie : synthèse et défis.

Unité 5. Clôture du cours

Elle se compose de la leçon Bilan final de Logique mathématique I, qui rappelle les sept objectifs globaux, montre sur une figure dans quelles unités et leçons chacun est travaillé, réunit par objectif la première tentative des évaluations de sortie et indique où se poursuit l’étude.

Charge de travail et crédits

La charge de travail d’un cours ne se mesure pas aux heures d’exposé, qui dans un cours asynchrone n’existent pas, mais au travail total de qui l’étudie : lire, suivre les démonstrations et les déductions, résoudre des problèmes et réviser. L’estimation suit la même méthode dans tous les cours du site : elle compte le temps de lecture du texte de chaque leçon à cent mots par minute, en comptant chaque formule comme un mot, vingt minutes par problème résolu, trente-cinq par problème proposé, quarante-cinq par défi et douze par évaluation d’entrée ou de sortie, et ajoute une marge d’un dixième pour la révision.

Résultats

Les leçons du cours contiennent au total $90$ problèmes résolus, $90$ problèmes proposés et $24$ défis, outre huit évaluations d’unité. La charge de travail estimée par unité, arrondie à l’heure, est la suivante :

• Unité 0, présentation du cours : moins d’$1$ heure.
• Unité 1, langage : $30$ heures.
• Unité 2, déduction : $36$ heures.
• Unité 3, sémantique : $43$ heures.
• Unité 4, métathéorie : $25$ heures.
• Unité 5, clôture du cours : moins d’$1$ heure.

Le total est d’environ $137$ heures de travail. Il convient de lire ce chiffre pour ce qu’il est : une estimation pour qui étudie toutes les démonstrations et résout tous les problèmes et tous les défis. Qui a déjà étudié la logique, ou se limite aux problèmes proposés sans aborder les défis, y consacrera nettement moins ; qui n’a jamais démontré un théorème peut avoir besoin de davantage, surtout dans les unités de déduction et de sémantique, qui sont aussi les plus longues.

Or ce chiffre est nominal : c’est lui qui fixe les crédits du cours, et il suppose une lecture à rythme constant et trois quarts d’heure par défi. Tant qu’il n’aura pas été mesuré auprès d’étudiants réels, il convient de l’accompagner d’une fourchette réaliste. Si la lecture avançait à la moitié du rythme supposé, comme il arrive lorsqu’on recopie chaque déduction avec papier et crayon et qu’on décompose à la main chaque chaîne de cercles et de disques, et si chaque défi exigeait soixante-quinze minutes au lieu de quarante-cinq, la même méthode donnerait environ $174$ heures. Par conséquent, la charge de travail attendue se situe entre environ $137$ et environ $174$ heures. L’extrémité supérieure est une borne prudente, non une mesure ; la fourchette sera corrigée quand on connaîtra le temps qu’y consacrent ceux qui étudient le cours, et d’ici là les crédits se calculent avec le chiffre nominal.

Rythme suggéré

Pour nommer les rythmes, ce plan suit le même critère que les autres plans du site : le temps plein est celui d’une année universitaire de $60$ crédits, environ $1650$ heures réparties sur une quarantaine de semaines, soit environ $40$ heures par semaine, et le temps partiel en est la moitié, environ $20$ heures par semaine. Il s’ensuit un rythme recommandé d’un semestre de seize semaines, avec environ $8$ ou $9$ heures d’étude par semaine, un peu plus du cinquième du temps plein ; avec la fourchette réaliste, de $9$ à $11$ heures par semaine. Ce semestre peut être partagé avec Algèbre et géométrie I, dont les démonstrations se lisent mieux quand la déduction est déjà un objet connu.

Un rythme intensif, d’environ $20$ heures par semaine, c’est-à-dire à temps partiel, achève le cours en sept semaines. Un rythme plus détendu, d’environ $4$ ou $5$ heures par semaine, le porte à deux semestres, qui le partagent presque par moitié : les unités 0 à 2, le langage et la déduction, occupent environ $67$ heures, et les unités 3 à 5, la sémantique, la métathéorie et la clôture, environ $69$.

Équivalence en crédits transférables

Les systèmes de crédits transférables mesurent un cours au travail total qu’il exige de qui le suit, et non aux heures de cours en présentiel, afin que les études faites dans un établissement puissent être reconnues dans un autre. Le Système européen de transfert et d’accumulation de crédits, adopté par les universités européennes à partir de la Déclaration de Bologne, attribue $60$ crédits à une année universitaire à temps plein, et fixe chaque crédit entre $25$ et $30$ heures de travail. Le Système de crédits transférables du Chili, adopté par les universités chiliennes selon une conception analogue, attribue lui aussi $60$ crédits à l’année universitaire et fixe chaque crédit entre $24$ et $31$ heures de travail.

Or, en divisant les $137$ heures estimées par les bornes de chaque intervalle, le cours équivaut à environ $5$ crédits européens (de 4,6 à 5,5), et à entre $4$ et $6$ crédits transférables chiliens (de 4,4 à 5,7). En prenant pour référence la valeur centrale des deux intervalles, 27,5 heures par crédit, on obtient dans les deux systèmes le même nombre, 4,98, qui s’arrondit à 5. Pour les crédits européens, le nombre $C$ de crédits est ainsi borné :

Par conséquent, il est recommandé d’attribuer au cours $5$ crédits européens et $5$ crédits transférables chiliens, c’est-à-dire la douzième partie d’une année universitaire à temps plein, un peu moins qu’un enseignement semestriel courant de six crédits.

Conception du cours

Modalité

Le cours est asynchrone, en ligne et à rythme libre : il n’a ni dates, ni séances en direct, ni échéances, et chaque étudiant avance à la vitesse que lui permettent sa préparation et son temps. Il est offert dans les quatorze langues du site, avec la même logique dans toutes : les formules, les déductions et les pas des démonstrations sont identiques dans chaque version, et seul le texte est traduit. Les leçons indiquent quelles autres leçons il convient d’avoir étudiées auparavant, de sorte que l’ordre recommandé est explicite.

La structure d’une leçon

Toutes les leçons de contenu suivent la même structure. Elles commencent par un résumé et par une liste d’objectifs d’apprentissage propres, formulés comme des performances observables. Viennent ensuite la théorie, avec les définitions, les résultats énoncés avec précision et leurs démonstrations, et les exemples. Les démonstrations se présentent comme des lecteurs pas à pas : chaque pas écrit une ligne, éclaire ce qui change et, lorsqu’il s’appuie sur un résultat antérieur, y renvoie. Les déductions du système s’écrivent avec leurs lignes numérotées et la justification de chacune à droite (un axiome, une prémisse, le modus ponens avec les lignes qu’il utilise, ou une règle dérivée), et en avançant les lignes citées s’éclairent. La leçon se clôt par cinq problèmes résolus, avec leur solution pas à pas, et cinq problèmes proposés, chacun avec une piste repliée puis la réponse finale ; les problèmes proposés de démonstration ajoutent, repliée après la réponse, une solution développée, qu’il convient de n’ouvrir qu’après avoir rédigé la sienne.

Chaque leçon peut en outre s’écouter à voix haute avec le lecteur du site, qui prononce en mots les symboles des formules, y compris le cercle, le disque et les symboles de la déduction et de la conséquence.

Évaluation

Le cours ne note pas : son évaluation est formative et repose sur l’autoévaluation. Les problèmes proposés permettent de vérifier la réussite des objectifs de chaque leçon, et les défis, celle des objectifs de chaque unité. S’y ajoutent les évaluations d’unité : celle d’entrée, au début de l’introduction, mesure le point de départ avec onze à quinze questions, car à celles de l’unité elle en ajoute quelques-unes sur ce que l’unité tient pour connu ; celle de sortie, dans la synthèse et avant les défis, mesure les acquis avec douze questions et se compare avec celle d’entrée. Les deux se corrigent dans le navigateur même, avec une explication pour chaque réponse et un renvoi à la leçon qu’il convient de réviser ; leurs résultats ne sont conservés que dans le navigateur de qui y répond, et le bilan final réunit la première tentative de chaque évaluation de sortie dans un profil par objectif global.

Comment étudier ce cours

Le cours a été pensé pour être étudié dans l’ordre. Chaque unité suppose les précédentes : la déduction s’écrit avec le langage de la première, la sémantique donne une valeur à ses formules, et la métathéorie compare la deuxième avec la troisième ; sauter une leçon oblige, tôt ou tard, à y revenir.

Dans chaque leçon, il convient de lire d’abord le résumé et les objectifs ; d’étudier ensuite la théorie avec papier et crayon, en recopiant les chaînes de cercles et de disques, en séparant leurs variables et leurs disques, et en anticipant chaque ligne d’une déduction avant que le lecteur ne l’écrive ; de tenter les problèmes résolus avant de regarder leur solution, et de résoudre les proposés sans aide, en n’ouvrant la piste que lorsque la tentative est épuisée. Un problème dont on a consulté la réponse avant de le tenter n’a pas été résolu, mais lu.

Enfin, il convient de toujours distinguer de quel niveau est chaque affirmation : si elle dit quelque chose dans le langage, comme une formule, ou quelque chose sur lui, comme $\Gamma \vdash \varphi$ ou $\Gamma \models \varphi$. Cette distinction, qui est le premier des objectifs du cours, est aussi celle qui permet de comprendre son résultat central, lequel ne peut s’énoncer que dans le métalangage.