Langage objet, métalangage et démonstration

Objectifs

À l'issue de ce module, le lecteur saura :

• distinguer, dans une phrase mathématique, ce qui relève du langage objet et ce qui relève du métalangage, et corriger les phrases qui confondent les deux niveaux ;
• décrire un dispositif syntaxique comme un système de règles sur un univers, et exhiber une dérivation dans un tel système ;
• démontrer que la définition d'un ensemble par le bas, au moyen de dérivations, et sa définition par le haut, comme plus petite partie close, coïncident ;
• justifier une preuve par induction sur un ensemble inductivement défini en invoquant ce théorème, et repérer les hypothèses sans lesquelles il tombe ;
• démontrer les propriétés structurelles de la dérivabilité — réflexivité, monotonie, finitude, transitivité — et reconnaître laquelle d'entre elles la sémantique ne fournit pas gratuitement ;
• démontrer qu'un objet n'est pas dérivable dans un système donné, en exhibant un invariant préservé par toutes les règles.

Prérequis supposés acquis

Les notions suivantes, introduites au module 1, sont mobilisées sans être redéfinies :

• l'appartenance, l'inclusion et la compréhension restreinte : définition 1.6 et notation 1.7 (module 1, « Ensembles, fonctions et cardinalité ») ;
• les opérations booléennes et l'intersection indexée, définition 1.8 (module 1), dont l'usage exige un ensemble d'indices non vide ;
• l'ensemble des parties, définition 1.10 (module 1) ;
• le couple, le produit cartésien, les $n$-uplets, l'ensemble $E^{*}$ des suites finies et le mot vide $\varepsilon$ : définition 1.12 (module 1) ;
• la notion de fonction totale, d'injection et de bijection : définitions 1.19 et 1.21 (module 1) ;
• la subpotence $\preccurlyeq$, notation 1.28 (module 1), et ses propriétés de préordre, proposition 1.29 (module 1) ;
• la finitude, la dénombrabilité et le caractère au plus dénombrable, définition 1.40 (module 1) ;
• la caractérisation $E \preccurlyeq \mathbb{N}$ du caractère au plus dénombrable, corollaire 1.42 (module 1), et le fait que $E^{*}$ est au plus dénombrable dès que $E$ l'est, proposition 1.47 (module 1).

Sont supposées acquises, en outre, les connaissances mathématiques générales suivantes, extérieures au parcours et non redémontrées. Les trois premières sont exactement celles déjà admises au module 1, rappelées ici sous la numérotation propre à ce module ; la quatrième est un emprunt nouveau, signalé comme tel.

1. Le raisonnement par récurrence sur $\mathbb{N}$, sous sa forme simple et sous sa forme forte, ainsi que le principe du bon ordre : toute partie non vide de $\mathbb{N}$ possède un plus petit élément, noté $\min$. Ce prérequis est identique au prérequis 1 du module 1.
2. La définition de suites par récurrence sur $\mathbb{N}$ : étant donnés une valeur initiale et une loi de passage de l'étape $n$ à l'étape $n+1$, il existe une unique suite les vérifiant. Ce prérequis est identique au prérequis 2 du module 1 ; il sera démontré dans le cadre général du théorème de définition par induction structurelle (module 3) et du théorème de récursion transfinie (module 16).
3. Les propriétés élémentaires des ensembles finis : toute partie d'un ensemble fini est finie ; la réunion de deux ensembles finis est finie ; le principe de choix fini, à savoir qu'un nombre fini de sélections successives dans des ensembles non vides se justifie par récurrence sur le nombre de sélections. Ce prérequis reprend le prérequis 4 du module 1 et l'étend à la réunion et au choix fini, deux points admis ici sans démonstration.
4. La divisibilité élémentaire dans $\mathbb{N}$, sous la seule forme suivante : pour tout $k \in \mathbb{N}$, si $3$ divise $2k$, alors $3$ divise $k$. Cet emprunt est nouveau ; il n'est utilisé que dans la preuve du théorème 2.36.

Aucune axiomatique n'est supposée : comme au module 1, le raisonnement se mène dans la théorie naïve des ensembles, dont le statut est précisément l'un des objets de ce module.

Corps du cours

Le partage des niveaux

Un texte de logique parle de langages, de formules, de dérivations. Il en parle dans un langage, qui n'est pas celui dont il parle. Tout le module tient dans cette phrase, et la difficulté est qu'elle est facile à admettre et difficile à respecter : les fautes de niveau ne produisent pas d'erreur visible, elles produisent des énoncés qui semblent avoir un sens et n'en ont pas.

Dans tout le parcours, le métalangage est le français augmenté de la théorie naïve des ensembles du module 1, et les langages objets sont ceux que les modules 3, 6 et 16 construiront. Cette dissymétrie est délibérée : le langage objet est entièrement décrit, symbole par symbole, tandis que le métalangage est employé sans être décrit.

La première est $\mathcal{M} \models \varphi \to \mathcal{M} \models \psi$. Le signe $\to$ est un connecteur du langage objet : il ne relie que des formules de ce langage. Or $\mathcal{M} \models \varphi$ n'est pas une formule du langage objet, c'est une assertion du métalangage. L'écriture correcte est : si $\mathcal{M} \models \varphi$, alors $\mathcal{M} \models \psi$, ou, dans une chaîne alignée, $\mathcal{M} \models \varphi \Longrightarrow \mathcal{M} \models \psi$ (Charte § 4.1).

La seconde est « l'énoncé $\Gamma \vdash \varphi$ est dérivable ». Le signe $\vdash$ appartient au métalangage : $\Gamma \vdash \varphi$ affirme l'existence d'une dérivation, et une telle affirmation ne se dérive pas, elle se démontre. L'écriture correcte est : on démontre que $\Gamma \vdash \varphi$ (Charte § 4.2).

Alphabets, mots et expressions

Avant tout système, il faut des objets sur lesquels les règles opèrent. Ces objets sont des suites finies de symboles, et rien d'autre : c'est le degré zéro de la syntaxe, celui qui rend la notion de règle purement mécanique.

1. $(uv)w = u(vw)$, et $\varepsilon u = u\varepsilon = u$ ;
2. $\mathrm{lg}(uv) = \mathrm{lg}(u) + \mathrm{lg}(v)$ ;
3. $\#_{s}(uv) = \#_{s}(u) + \#_{s}(v)$.

Systèmes de règles et définitions inductives

Tous les objets syntaxiques du parcours — formules, dérivations, théories closes par déduction — sont engendrés de la même façon : on part de quelques objets donnés et l'on applique un nombre fini de fois des règles à un nombre fini de prémisses. Il vaut la peine de traiter cette situation une fois pour toutes, en général, plutôt que de la refaire à chaque module.

La famille $\mathcal{C}$ est un ensemble par compréhension restreinte à $\mathcal{P}(U)$ (notation 1.7 et définition 1.10, module 1) ; elle est non vide, car $U$ lui-même est clos, ce qui légitime l'intersection indexée au sens de la définition 1.8 (module 1). Par construction, $\mathrm{Ind}(\mathsf{S})$ est contenu dans toute partie close ; qu'il soit lui-même clos n'a rien d'immédiat et résultera du théorème 2.21.

Pour $i = 1$, l'ensemble $\{ x_1, \dots, x_{i-1} \}$ est vide : la première ligne d'une dérivation est donc nécessairement un axiome. Une dérivation est un objet fini, et la vérification qu'une suite donnée en est une ne porte que sur des faits finis, ligne par ligne : c'est là tout l'intérêt de la notion, et l'on y reviendra à la remarque 2.42.

Le second point de la proposition 2.24 est trivial ; le premier ne l'est pas, et c'est lui qui servira. Il dit qu'un système de règles sur un univers au plus dénombrable ne dispose que d'au plus dénombrablement de dérivations, quel que soit le nombre de ses règles. Aucune énumération de dérivations ne pourra donc jamais atteindre un ensemble non dénombrable d'objets : c'est la première apparition, encore muette, de l'écart entre ce qu'un système démontre et ce qu'il vise, écart que le théorème de Löwenheim–Skolem descendant (module 9) et le paradoxe de Skolem (module 9) rendront spectaculaire.

Dérivabilité sous hypothèses

Un système de règles engendre un ensemble d'objets à partir de ses seuls axiomes. La pratique demande davantage : on veut dériver à partir d'hypothèses supplémentaires, provisoirement adoptées. Le procédé est uniforme, et les propriétés qui en résultent sont exactement celles que tous les systèmes de déduction du parcours exhiberont.

1. Réflexivité. Si $x \in \Gamma$, alors $\Gamma \vdash_{\mathsf{S}} x$.
2. Monotonie. Si $\Gamma \subseteq \Delta$ et $\Gamma \vdash_{\mathsf{S}} x$, alors $\Delta \vdash_{\mathsf{S}} x$.
3. Finitude. Si $\Gamma \vdash_{\mathsf{S}} x$, il existe une partie finie $\Gamma_{0} \subseteq \Gamma$ telle que $\Gamma_{0} \vdash_{\mathsf{S}} x$.
4. Transitivité. Si $\Gamma \vdash_{\mathsf{S}} y$ pour tout $y \in \Delta$, et si $\Delta \vdash_{\mathsf{S}} x$, alors $\Gamma \vdash_{\mathsf{S}} x$.

Un système jouet et une démonstration à son sujet

Les définitions qui précèdent restent vides tant qu'on n'a pas vu, sur un cas complet, ce qu'est une dérivation et ce qu'est une démonstration portant sur les dérivations. Le système suivant n'a aucune signification ; c'est délibéré. Ses règles sont des manipulations de symboles, et la question qu'on lui pose — un certain mot est-il dérivable ? — se tranche par un raisonnement qui ne se mène pas dans le système.

Les trois dernières familles sont infinies : chacune de R1, R2, R3 n'est pas une règle mais un schéma de règles, une règle étant obtenue par le choix des mots $u$, $v$, $w$. Il en ira de même du schéma de séparation de $\mathrm{ZF}$ (module 16) et du schéma de récurrence de $\mathrm{PA}$ (module 13) : un système à ensemble infini de règles reste parfaitement légitime au sens de la définition 2.17, seule la finitude de chaque ensemble de prémisses étant requise.

La seconde dérive $\varepsilon$ de l'hypothèse $\mathtt{abbb}$, au sens de la définition 2.28 ; la ligne $1$ est un axiome du système enrichi $\mathsf{D}[\{ \mathtt{abbb} \}]$, et son numéro reste porté par la colonne des dépendances jusqu'à la conclusion, aucune règle de $\mathsf{D}$ ne déchargeant d'hypothèse.

Ainsi $\{ \mathtt{abbb} \} \vdash_{\mathsf{D}} \varepsilon$. Le théorème 2.36 montrera que $\varnothing \vdash_{\mathsf{D}} \varepsilon$ est faux : la conclusion tient à l'hypothèse, et non aux seules règles.

Démonstration et dérivation

Il reste à nommer précisément ce que fait ce texte lui-même, et à mesurer ce que la formalisation déplace.

Cette définition ne fait que fixer un vocabulaire, conformément à la Charte § 4.2 et § 7 : elle ne définit pas la démonstration comme un objet mathématique, et ne le peut pas ici. Une démonstration n'a pas de forme prescrite ; elle est reconnue correcte par un lecteur compétent, non vérifiée par un automate. Toute la logique mathématique tient dans le refus de se satisfaire de cette situation, sans pour autant pouvoir en sortir.

Résumé des résultats

Glossaire du module

Pièges fréquents

Employer un connecteur du langage objet comme articulation du raisonnement. C'est la faute décrite au contre-exemple 2.4, et elle est d'autant plus tenace qu'elle ne produit jamais d'erreur de résultat : les phrases fautives sont en général celles qu'on aurait écrites correctement en français. Le critère est mécanique : $\neg$, $\wedge$, $\vee$, $\to$, $\leftrightarrow$, $\forall$, $\exists$, $\bot$, $\top$, $=$ ne peuvent apparaître qu'à l'intérieur d'une formule mentionnée ; dès qu'un de ces signes relie deux assertions de la rédaction, la phrase est mal formée.

Confondre « non dérivable » et « faux ». La non-dérivabilité est une propriété d'un objet relativement à un système, établie dans la métathéorie, généralement par un invariant (théorème 2.36) ; la fausseté est une propriété relative à une structure (Charte § 7). Rien, à ce stade, ne relie les deux, et le programme des modules 5, 8 et 9 consiste précisément à établir ce lien pour des systèmes déterminés. Croire le lien acquis d'avance rend inintelligibles les théorèmes d'incomplétude, dont tout le contenu est que le lien se rompt (module 14).

Attendre d'une dérivation qu'elle établisse une impossibilité. Une dérivation ne fait qu'accroître la liste des objets dérivables ; aucune ne peut avoir pour conclusion « tel objet n'est pas dérivable ». C'est pourquoi les résultats négatifs du parcours sont tous des théorèmes de la métathéorie, et pourquoi la remarque 2.38 mérite d'être relue avant chaque preuve d'indépendance.

Confondre une règle et un schéma de règles. R1, R2 et R3 de la définition 2.34, comme le schéma de séparation ou le schéma de récurrence, désignent chacun une infinité de règles. Un système à ensemble infini de règles reste licite ; ce qui ne l'est pas, c'est une règle à ensemble infini de prémisses, et l'exercice 2.26 montre que la confusion entre les deux fait s'effondrer le théorème 2.21.

Croire le métalangage plus sûr que le langage objet. Le métalangage de ce parcours est le français et la théorie naïve des ensembles, dont le module 1 a montré qu'elle est contradictoire sous sa forme non restreinte (théorème 1.2, module 1). Il n'est ni plus formel, ni mieux fondé que les systèmes qu'il étudie : il est seulement celui dans lequel on se tient. La remarque 2.5 rappelle que les rôles peuvent s'échanger, et le second théorème d'incomplétude de Gödel (module 15) dira ce qu'il en coûte de vouloir refermer la boucle.

Lire $\mathrm{Ind}(\mathsf{S})$ comme « l'ensemble des objets vrais ». Un système de règles engendre ce que ses règles engendrent, ni plus ni moins ; la définition 2.19 le construit sans qu'aucune notion de vérité intervienne. Le seul énoncé qui traverse la définition est celui du corollaire 2.22, et il ne dit rien de plus que ceci : ce qui est préservé par les règles vaut pour tout ce qu'elles engendrent.

Écrire « démontrable dans $T$ » pour « dérivable dans $T$ ». La Charte § 7 réserve « démontrer » au métalangage et « dériver » au système formel, avec la seule exception lexicale du prédicat de prouvabilité (module 15). La définition 2.41 fixe cet usage ; l'inobservation rend indiscernables les deux énoncés qui, au module 14, doivent absolument le rester : « $\mathfrak{N} \models \sigma$ » et « $T \vdash \sigma$ ».

Prendre l'ordre des lignes d'une dérivation pour une donnée essentielle. La définition 2.20 n'impose qu'une condition d'antériorité des prémisses ; un même élément admet en général une infinité de dérivations, différant par leur ordre, par des lignes inutiles ou par les règles employées. Ce n'est pas une imprécision : la preuve du théorème 2.21 exploite cette latitude en concaténant des dérivations, et le module 19 étudiera précisément les formes normales que l'on peut imposer aux dérivations sans changer ce qu'elles concluent.

Notations introduites

Les notations suivantes sont introduites ou fixées dans ce module. Celles qui ne figurent pas dans la Charte sont signalées par une mention explicite dans la dernière colonne, conformément à la Charte § 1 ; elles sont reprises dans l'encadré de tête.

Checklist d'auto-vérification

• Unicité des notations — chaque concept est noté d'une seule façon dans tout le module, conformément à la § 6 ; aucune notation concurrente n'a été introduite en cours de route.
• Notations hors Charte — toute notation absente de la Charte est signalée dans l'encadré de tête et reprise dans la section « Notations introduites ».
• Séparation objet / méta — $\neg, \wedge, \vee, \to, \leftrightarrow, \forall, \exists, \bot, \top, =$ n'apparaissent qu'à l'intérieur de formules du langage objet, c'est-à-dire, dans ce module, uniquement au contre-exemple 2.4 et aux exercices 2.6 et 2.7, où ils sont mentionnés ; $\Longrightarrow, \Longleftrightarrow, :=$ et les quantifications en français n'apparaissent que dans le métalangage ; aucune phrase de preuve n'utilise un connecteur objet comme articulation logique.
• Démonstration vs dérivation — le vocabulaire distingue partout démonstration (métathéorie) et dérivation (système formel) ; c'est l'objet même de la définition 2.41.
• Format des environnements — en-têtes en gras conformes au modèle **Théorème 9.4 (Complétude).**, aucun environnement hors de la liste admise.
• LaTeX systématique — aucun symbole mathématique en Unicode brut ; aucun | littéral dans une cellule de tableau ; aucune formule $$...$$ dans un tableau.
• Numérotation — compteur unique, continu et croissant sur tout le module, de $2.1$ à $2.45$, préfixé par le numéro du module.
• Renvois — tous les renvois sont numérotés et au format de la § 2.4 ; les renvois externes mentionnent le module, le premier d'entre eux rappelant le titre abrégé ; aucun renvoi vague.
• Preuves complètes — toutes les hypothèses utilisées sont nommées, tous les cas d'induction sont traités, la méthode est annoncée en italique, la preuve se clôt par $\blacksquare$ ; la preuve emboîtée du théorème 2.21 se clôt par $\square$ ; toute étape déléguée renvoie à un exercice numéroté existant.
• Dérivations formelles — format linéaire à quatre colonnes de la § 5.1, dépendances explicites, à l'exemple 2.35. (La colonne « Formule » y est intitulée « Mot », l'univers du système $\mathsf{D}$ étant un ensemble de mots et non de formules ; aucune décharge ni condition de variable propre n'est à signaler, le système $\mathsf{D}$ ne comportant ni règle de décharge ni variable.)
• Résultats nommés — la § 8 n'assigne aucun résultat canonique au module 2 ; aucun nom canonique n'est donc employé, et les résultats des autres modules cités le sont sous leur nom canonique exact.
• Glossaire — les termes ambigus de la § 7 sont employés dans le sens retenu ; la section « Glossaire du module » couvre tous les termes nouveaux introduits en gras.
• Gabarit — les sept sections de la § 3 sont présentes, dans l'ordre, avec leurs titres exacts.