Bilan final de Logique mathématique I

Ce que le cours s’est 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. Le cours est donc né d’un but général : construire 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 sans ambiguïté ; un calcul, qui produit des déductions sans prêter attention à la signification des symboles ; une signification, qui attribue à chaque formule sa valeur sous chaque valuation ; et la démonstration que le calcul et la signification coïncident, c’est-à-dire que $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ pour tout ensemble de formules $\Gamma$ et toute formule $\varphi$. La leçon sur le plan d’études a déployé ce but en sept objectifs d’apprentissage globaux, qu’il convient de garder en vue avec la numérotation par laquelle la figure les cite :

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. Formaliser des énoncés et des raisonnements de la langue naturelle, en signalant ce que la formalisation conserve et ce qu’elle perd.
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. Démontrer des métathéorèmes par récurrence sur les entiers, par induction sur la complexité des formules et par récurrence sur la longueur des déductions.
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. Transformer des formules en formes normales et exprimer avec elles des fonctions de vérité et des circuits.
7. Expliquer et appliquer la correction, la complétude et la compacité, et décider l’insatisfaisabilité par résolution.

Chaque leçon du cours a en outre énoncé ses propres objectifs spécifiques. Les leçons ne disent pas à quel objectif global chacun sert ; cette correspondance est une lecture faite de l’extérieur, selon la même méthode que dans les autres cours du site. Chaque objectif spécifique est rattaché à un objectif global principal et, s’il les touche, à d’autres secondaires ; chacun compte entièrement dans son principal et pour moitié dans chaque secondaire, et la leçon est reliée comme principale à l’objectif global qui réunit le plus de poids et comme secondaire aux autres qui en reçoivent. Si deux objectifs sont à égalité, celui de l’unité l’emporte et, si aucun ne l’est, celui qui porte le plus petit numéro ; ainsi, la leçon sur la récurrence et l’induction, dont les quatre objectifs spécifiques sont des démonstrations par récurrence ou par induction, est reliée à l’objectif 4, bien qu’elle appartienne à l’unité du langage. Les introductions suivent la même règle. Les synthèses, en revanche, suivent un critère propre : leur principal est l’objectif de leur unité, parce que leur chaîne déductive, leur évaluation de sortie et la plupart de leurs défis réunissent ce que l’unité a enseigné, et leurs secondaires sont les autres objectifs qu’exercent leurs objectifs spécifiques et leurs six défis. S’il en est ainsi, le cours entier prend la forme d’une colonne vertébrale : la tête est le but général ; la colonne, l’ordre des unités, chacune avec son tronçon ; chaque leçon est un nœud de ce tronçon, relié à son objectif principal, et les sept objectifs flottent autour de la colonne, soutenus par les leçons qui les nourrissent.