Mathématiques et logique : synthèse et défis

Résumé

Cette leçon clôt la quatrième unité du cours, consacrée aux mathématiques et à la logique. Elle reconstruit la chaîne de principes et de mécanismes qui va du mode mathématique aux arbres de déduction, en indiquant à chaque maillon quel principe est employé et dans quelle leçon il est établi ; elle situe l’acquis par rapport au plan du cours et précise quelles questions, à peine esquissées, restent pour les unités suivantes ; elle reprend dans son évaluation de sortie les compétences de l’évaluation d’entrée ; et elle se termine par six défis, d’une difficulté supérieure à celle des problèmes des leçons, qui exigent d’en combiner plusieurs pour composer des notes de cours avec énoncés, démonstration et renvois, diagnostiquer des documents qui compilent avec des défauts que rien ne signale, transposer une notation logique d’une tradition à une autre, construire et déboguer une déduction à plusieurs branches, prévoir la numérotation et les grandeurs d’un rapport de physique, et réunir deux préambules incompatibles.

Objectifs d’apprentissage

Reconstruire l’ordre des mécanismes de l’unité, en identifiant le principe sur lequel chacun s’appuie.
Expliquer pourquoi tant de défauts de l’écriture mathématique compilent sans avertissement, et où chercher leur trace dans le résultat ou dans le journal.
Distinguer ce que l’unité a établi de ce qu’elle a seulement esquissé et que les unités suivantes développeront.
Prévoir les numéros, les renvois et les grandeurs que produit un source contenant des équations, des énoncés et des unités, et le corriger.
Concevoir un préambule qui fixe la notation, les énoncés et l’ordre de chargement des extensions d’un travail, et qui permette de changer de convention sans toucher au corps du texte.

L’acquis de l’unité

L’unité se proposait que chaque signe d’une formule soit composé selon ce qu’il signifie, et que la notation d’un travail soit la même sur toutes ses pages. Ce but a été atteint en s’appuyant sur ce que l’introduction a tenu pour acquis des unités précédentes : les renvois, qui dépendent de ce qu’enregistre une étiquette ; les commandes personnelles, qui concentrent les décisions de forme dans le préambule ; et la lecture du journal. Dès lors, le chemin parcouru peut se lire comme une seule chaîne en cinq tronçons.

Formules en ligne et hors texte

La leçon sur les formules en ligne et hors texte a établi le principe dont dépendent presque tous les autres : en mode mathématique, les espaces du source ne comptent pas, et le moteur sépare chaque signe selon sa classe, ordinaire, opérateur binaire, relation, ponctuation, ouvrant ou fermant. Elle en a déduit pourquoi une variable ne s’écrit pas avec \textit, pourquoi $3,5$ donne « 3, 5 » et pourquoi la ponctuation de la phrase se place hors de la formule en ligne. Elle a montré que, dans LuaLaTeX, une lettre grecque hors de son mode ne produit pas d’erreur, mais disparaît ou apparaît de façon incontrôlée, avec une seule ligne « Missing character » dans le journal ; elle a ponctué la formule hors texte comme une partie de la phrase, sans ligne vide et sans $$ ; elle a numéroté avec equation, \eqref, \numberwithin et \tag ; elle a distingué \text de \mathrm ; et elle a étudié la virgule décimale, que babel en français ne produit pas (à la différence de babel en espagnol) et qui s’écrit entre accolades, l’extension icomma, et siunitx, qui demande sa propre déclaration du séparateur, locale = FR.

Symboles et notation

La leçon sur les symboles et la notation est partie d’une règle de groupement : ^ et _ agissent sur un seul élément ou sur un groupe entre accolades. Elle a parcouru les fractions, les racines, les lettres grecques et les alphabets, parmi lesquels les combinaisons qui se perdent sans erreur avec fontspec, comme \mathbf{\Gamma} ; les opérateurs nommés, que babel en français laisse intacts (seules les fonctions hyperboliques ch, sh et th se déclarent soi-même), avec ce que change babel en espagnol, le cas le plus net (\lim accentué, \sen nouveau, \sin intact), et ce que supprime es-minimal ; les grands opérateurs, les délimiteurs et leurs tailles ; la recherche d’un symbole inconnu ; et unicode-math, avec ses quatre précautions. Elle s’est terminée en portant la notation dans le préambule, dans des commandes personnelles que l’on décide une fois.

Équations sur plusieurs lignes

La leçon sur les équations sur plusieurs lignes a remplacé les formules empilées et eqnarray par align, avec le & avant la relation, et a établi qu’un environnement d’alignement est un tableau : une ligne par \\ et une cellule par tronçon entre deux &. Elle en a déduit ses défauts silencieux (le =&, le & en trop, la double barre finale qui numérote une ligne vide, l’étiquette sur une ligne portant \notag) et ses erreurs bruyantes ; elle a choisi entre gather, multline, split, aligned et gathered selon le numéro que doit porter l’ensemble ; elle a composé des définitions par cas avec cases et dcases, du texte avec \intertext, des matrices et des matrices augmentées ; elle a numéroté des groupes avec subequations et permis la coupure de page.

Théorèmes et démonstrations

La leçon sur les théorèmes et les démonstrations a porté jusqu’à l’énoncé l’idée de déclarer au lieu d’imiter : avec amsthm, \newtheorem fixe l’en-tête, le numéro et le style de chaque sorte d’énoncé. Elle a déduit quand conviennent le compteur partagé et les compteurs séparés, quand la numérotation par section ou par chapitre, et quel style correspond à ce qu’on affirme, à ce qu’on stipule et à ce qui accompagne. Elle a composé les démonstrations avec proof, dont l’en-tête vient de babel, et corrigé avec \qedhere le carré orphelin ; elle a renvoyé avec cleveref, chargé après amsthm, avec un \crefname par environnement, et découvert qu’avec le compteur partagé de \newtheorem cleveref appelle « théorème » tout énoncé, défaut que thmtools corrige.

Logique et déductions

La leçon sur la logique et les déductions a séparé le langage objet du métalangage, avec \to face à \Rightarrow et les signes \vdash, \models et \equiv ; elle a appliqué le principe de la classe du signe au tilde de la négation, à la barre des ensembles et aux deux-points des fonctions ; elle a proposé une commande par connecteur, sans arguments pour changer de signes et avec arguments pour changer de syntaxe ; elle a réuni les extensions des signes modaux ; elle a composé des tables de vérité avec array ; et elle a construit des arbres de déduction naturelle avec bussproofs, dont la logique de pile explique les deux erreurs, ainsi que les boîtes de Fitch et les arguments en forme standard.

La figure suivante réunit les cinq tronçons en une seule chaîne. Chaque nœud de la colonne est un mécanisme ou une règle, numéroté selon l’ordre dans lequel ils s’appuient les uns sur les autres et relié par un arc aux maillons antérieurs qu’il utilise ; autour flottent les appuis, c’est-à-dire les principes 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 qui ont été établis dans des unités précédentes, qui sont dessinés comme des anneaux. Un clic sur un appui met en évidence tous les maillons qui l’utilisent, et chaque maillon renvoie à la leçon où il est étudié.

Appuis de la chaîne

ACe qu’enregistre une étiquette. Une étiquette enregistre le dernier numéro attribué avant elle, dans son environnement, sans savoir à quoi elle est attachée. Établi dans l’unité précédente. Admis sans démonstration dans cette unité.
BCommandes personnelles. Une commande personnelle nomme une fonction, et sa définition, écrite une fois dans le préambule, en fixe la forme ; la changer change tout le document. Établi dans l’unité précédente. Admis sans démonstration dans cette unité.
COrdre de chargement. Les extensions se chargent dans l’ordre où elles sont lues, et une extension postérieure ajuste, conserve ou défait ce qu’avait fait une extension antérieure. Établi dans l’unité précédente. Admis sans démonstration dans cette unité.
DLa classe du signe. En mode mathématique, le moteur sépare chaque signe selon sa classe (ordinaire, opérateur binaire, relation, ponctuation, ouvrant, fermant) et ignore les espaces du source. Établi dans: 1. Deux modes.
ECe qui disparaît sans erreur. Dans LuaLaTeX, un signe que la fonte en usage ne contient pas n’arrête pas la compilation : il disparaît, et ne laisse dans le journal qu’une ligne « Missing character ». Établi dans: 2. Signes dans le mauvais mode.
FUn élément ou un groupe. Les indices, les exposants et les arguments agissent sur l’élément qui suit ou sur un groupe entre accolades, lesquelles ne s’impriment pas. Établi dans: 6. Indices et exposants.
GUn alignement est un tableau. Un environnement d’alignement construit une ligne par \\ et une cellule par tronçon entre deux &, même si la ligne reste vide. Établi dans: 11. Aligner avec align.
HLa pile d’arbres. Une inférence à n prémisses prend les n derniers arbres de la pile et en rend un ; la preuve s’imprime s’il en reste exactement un à la fin. Établi dans: 23. Arbres de déduction.

Tronçon 1 Formules en ligne et hors texte
- Prévoir le résultat d’un signe, d’une variable ou d’un mot écrit dans le mauvais mode.
- Ponctuer les formules en ligne et hors texte comme des parties de la phrase.
- Numéroter les formules hors texte et y renvoyer.
- Écrire les décimaux et les grandeurs selon l’usage français, avec ou sans siunitx.
1. Deux modes. En mode mathématique, les lettres sont des variables, les espaces du source ne comptent pas, l’espacement dépend de la classe de chaque signe et une ligne vide n’est pas admise.
  Repose sur: D (La classe du signe). Démontré dans: Formules en ligne et hors texte.
2. Signes dans le mauvais mode. Un _ dans le texte donne « Missing $ inserted » ; \alpha hors formule disparaît ou apparaît collé ; un mot dans la formule est un produit de variables et va dans \text ou dans \mathrm, qui ne sont pas interchangeables.
  Utilise: 1. Deux modes. Repose sur: E (Ce qui disparaît sans erreur). Démontré dans: Formules en ligne et hors texte.
3. La formule dans la phrase. La formule en ligne limite sa hauteur et laisse dehors la ponctuation de la phrase ; la formule hors texte se ponctue à l’intérieur, sans ligne vide, avec \[…\] ou equation et jamais avec $$.
  Utilise: 1. Deux modes. Repose sur: D (La classe du signe). Démontré dans: Formules en ligne et hors texte.
4. Numéroter et renvoyer. equation numérote et son étiquette se place à l’intérieur ; \eqref ajoute les parenthèses ; \numberwithin numérote par section ; \tag pose une marque sans consommer de numéro.
  Utilise: 3. La formule dans la phrase. Repose sur: A (Ce qu’enregistre une étiquette). Démontré dans: Formules en ligne et hors texte.
5. Virgule décimale. La virgule d’une formule est une ponctuation ; babel en français ne convertit pas le point (babel en espagnol, si) ; {,} vaut toujours, et siunitx demande locale = FR ou output-decimal-marker.
  Utilise: 1. Deux modes. Repose sur: D (La classe du signe). Démontré dans: Formules en ligne et hors texte.
Tronçon 2 Symboles et notation
- Grouper indices et exposants et prévoir ce qui manque sans accolades.
- Choisir alphabet, variante et opérateur selon la convention de la discipline.
- Prévoir ce que babel change dans les opérateurs : rien en français, beaucoup en espagnol.
- Fixer la notation du document dans son préambule.
1. Indices et exposants. x^10 n’élève que le 1 ; x^{10} élève le groupe ; deux indices de même sorte à la suite donnent « Double subscript » ou « Double superscript ».
  Utilise: 1. Deux modes. Repose sur: F (Un élément ou un groupe). Démontré dans: Symboles et notation.
2. Lettres et alphabets. Chaque alphabet dit quelle sorte d’objet on nomme ; avec fontspec, \mathbf{\Gamma} disparaît et \mathbf{\alpha} ne sort pas en gras, et le gras d’un symbole est \boldsymbol.
  Utilise: 6. Indices et exposants. Repose sur: E (Ce qui disparaît sans erreur). Démontré dans: Symboles et notation.
3. Opérateurs nommés. Les opérateurs vont en romain avec leur espace ; babel en français ne change rien, tandis que babel en espagnol accentue \lim, \max, \min et \inf, définit \sen et ne touche pas \sin, et es-minimal supprime tout cela.
  Utilise: 6. Indices et exposants. Repose sur: D (La classe du signe). Démontré dans: Symboles et notation.
4. Délimiteurs. \left et \right mesurent ce qu’ils encadrent et vont par paires ; les tailles manuelles donnent un contrôle fin ; mathtools définit des paires comme \abs.
  Utilise: 6. Indices et exposants. Repose sur: D (La classe du signe), F (Un élément ou un groupe). Démontré dans: Symboles et notation.
5. La notation dans le préambule. \R, \vect, \dd ou \abs se définissent une fois ; unicode-math vient après amsmath, sans amssymb derrière, et demande \symbf pour le gras.
  Utilise: 7. Lettres et alphabets, 8. Opérateurs nommés, 9. Délimiteurs. Repose sur: B (Commandes personnelles), C (Ordre de chargement), E (Ce qui disparaît sans erreur). Démontré dans: Symboles et notation.
Tronçon 3 Équations sur plusieurs lignes
- Aligner des chaînes et des systèmes avec align, avec le & avant la relation.
- Décider quelles lignes sont numérotées et prévoir les numéros.
- Choisir l’environnement selon la structure et le numéro de l’ensemble.
- Composer des définitions par cas, des matrices et du texte intercalé.
1. Aligner avec align. Le & se place avant la relation et \\ ouvre une ligne ; =& et un & en trop changent le résultat sans avertissement, et une ligne vide arrête la compilation.
  Utilise: 3. La formule dans la phrase. Repose sur: G (Un alignement est un tableau), D (La classe du signe). Démontré dans: Équations sur plusieurs lignes.
2. Quelles lignes sont numérotées. align numérote chaque ligne, y compris la ligne vide que laisse un \\ final ; \notag ôte le numéro sans le consommer, et une étiquette sur cette ligne enregistre celui de la ligne numérotée suivante.
  Utilise: 11. Aligner avec align, 4. Numéroter et renvoyer. Repose sur: G (Un alignement est un tableau), A (Ce qu’enregistre une étiquette). Démontré dans: Équations sur plusieurs lignes.
3. Un numéro pour l’ensemble. split dans equation donne un numéro à la chaîne ; aligned et gathered sont des blocs sans numéro ; subequations donne des lettres à un groupe qui consomme un seul numéro.
  Utilise: 11. Aligner avec align, 12. Quelles lignes sont numérotées. Repose sur: A (Ce qu’enregistre une étiquette). Démontré dans: Équations sur plusieurs lignes.
4. Cas, matrices et texte. cases a deux colonnes et convertit un & en trop en fin de ligne ; dcases compose en taille hors texte ; les matrices admettent dix colonnes ; array trace des barres ; \intertext ne rompt pas l’alignement.
  Utilise: 11. Aligner avec align. Repose sur: G (Un alignement est un tableau). Démontré dans: Équations sur plusieurs lignes.
Tronçon 4 Théorèmes et démonstrations
- Déclarer les énoncés avec leur style et leur compteur.
- Prévoir la numérotation d’une série partagée ou séparée.
- Clore les démonstrations avec le symbole à sa place.
- Renvoyer aux énoncés avec leur nom.
1. Énoncés déclarés. \newtheorem d’amsthm, dans le préambule, fixe en-tête, numéro et aspect ; l’en-tête est écrit par l’auteur, et la forme étoilée ne numérote pas.
  Repose sur: B (Commandes personnelles). Démontré dans: Théorèmes et démonstrations.
2. Compteurs et styles. [theoreme] fait une seule série, dont le numéro indique la place ; [section] ou [chapter] numérote par division ; plain, definition et remark répondent à ce qu’on affirme, stipule ou qui accompagne.
  Utilise: 15. Énoncés déclarés. Repose sur: B (Commandes personnelles). Démontré dans: Théorèmes et démonstrations.
3. Démonstrations. proof prend son en-tête de babel et pose le carré à la fin du dernier paragraphe ; si elle se termine par une formule ou une liste, \qedhere le met à sa place, sauf à côté d’un numéro.
  Utilise: 15. Énoncés déclarés, 11. Aligner avec align. Démontré dans: Théorèmes et démonstrations.
4. Renvoyer aux énoncés. L’étiquette se place dans l’environnement ; amsthm se charge avant cleveref, avec un \crefname par environnement ; avec le compteur partagé de \newtheorem tout s’appelle « théorème », et thmtools le corrige.
  Utilise: 16. Compteurs et styles, 4. Numéroter et renvoyer. Repose sur: A (Ce qu’enregistre une étiquette), C (Ordre de chargement). Démontré dans: Théorèmes et démonstrations.
Tronçon 5 Logique et déductions
- Distinguer dans la notation le langage objet du métalangage.
- Corriger l’espacement du tilde, de la barre, des deux-points et des quantificateurs.
- Changer de tradition depuis le préambule.
- Construire et déboguer des arbres de déduction, des tables de vérité et des arguments.
1. Deux niveaux de langage. \to est le connecteur du langage objet et \Rightarrow la flèche du métalangage ; \vdash affirme la déduction et \models la conséquence sémantique.
  Utilise: 8. Opérateurs nommés. Démontré dans: Logique et déductions.
2. L’espacement logique. \sim est une relation et se met entre accolades ; la barre du clavier est ordinaire et \mid une relation ; : est une relation et \colon une ponctuation ; la portée d’un quantificateur est décidée par une parenthèse.
  Utilise: 19. Deux niveaux de langage, 5. Virgule décimale. Repose sur: D (La classe du signe). Démontré dans: Logique et déductions.
3. Une commande par connecteur. Sans arguments, la commande change le signe d’une tradition à l’autre ; avec arguments, la définition décide en outre de l’ordre et des parenthèses, et permet la notation polonaise.
  Utilise: 20. L’espacement logique, 10. La notation dans le préambule. Repose sur: B (Commandes personnelles), F (Un élément ou un groupe). Démontré dans: Logique et déductions.
4. Signes modaux et tables de vérité. \Box, \Diamond et \vDash exigent amssymb, et latexsym chargé avant change le losange ; la table de vérité est un array avec V et F en romain.
  Utilise: 19. Deux niveaux de langage, 14. Cas, matrices et texte. Repose sur: C (Ordre de chargement), G (Un alignement est un tableau). Démontré dans: Logique et déductions.
5. Arbres de déduction. Dans bussproofs, \AxiomC pose une feuille et les inférences prennent les derniers arbres ; s’il en manque, « Hypotheses missing! » ; s’il y en a trop, « Proof tree badly specified. » à l’impression.
  Utilise: 19. Deux niveaux de langage. Repose sur: H (La pile d’arbres). Démontré dans: Logique et déductions.
6. Boîtes et forme standard. logicproof compose les boîtes de Fitch comme un tableau avec subproof ; un argument en forme standard numérote les prémisses et sépare la conclusion par un filet et \therefore.
  Utilise: 23. Arbres de déduction, 22. Signes modaux et tables de vérité. Repose sur: G (Un alignement est un tableau). Démontré dans: Logique et déductions.

Vers les tableaux et les figures. La chaîne s’arrête là où les formules, les énoncés et les déductions sont complets et numérotés : le tableau, qui n’a servi ici qu’aux matrices, aux tables de vérité et aux preuves, s’étend dans l’unité suivante jusqu’aux tableaux et aux figures du document, avec leurs légendes, leurs numéros et leur place dans la page.