David Madore's WebLog: 2025-12

Vous êtes sur le blog de David Madore, qui, comme le reste de ce site web, parle de tout et de n'importe quoi (surtout de n'importe quoi, en fait), des maths à la moto et ma vie quotidienne, en passant par les langues, la politique, la philo de comptoir, la géographie, et beaucoup de râleries sur le fait que les ordinateurs ne marchent pas, ainsi que d'occasionnels rappels du fait que je préfère les garçons, et des petites fictions volontairement fragmentaires que je publie sous le nom collectif de fragments littéraires gratuits. • Ce blog eut été bilingue à ses débuts (certaines entrées étaient en anglais, d'autres en français, et quelques unes traduites dans les deux langues) ; il est maintenant presque exclusivement en français, mais je ne m'interdis pas d'écrire en anglais à l'occasion. • Pour naviguer, sachez que les entrées sont listées par ordre chronologique inverse (i.e., la plus récente est en haut). Cette page-ci rassemble les entrées publiées en décembre 2025 : il y a aussi un tableau par mois à la fin de cette page, et un index de toutes les entrées. Certaines de mes entrées sont rangées dans une ou plusieurs « catégories » (indiqués à la fin de l'entrée elle-même), mais ce système de rangement n'est pas très cohérent. Le permalien de chaque entrée est dans la date, et il est aussi rappelé avant et après le texte de l'entrée elle-même.

You are on David Madore's blog which, like the rest of this web site, is about everything and anything (mostly anything, really), from math to motorcycling and my daily life, but also languages, politics, amateur(ish) philosophy, geography, lots of ranting about the fact that computers don't work, occasional reminders of the fact that I prefer men, and some voluntarily fragmentary fictions that I publish under the collective name of gratuitous literary fragments. • This blog used to be bilingual at its beginning (some entries were in English, others in French, and a few translated in both languages); it is now almost exclusively in French, but I'm not ruling out writing English blog entries in the future. • To navigate, note that the entries are listed in reverse chronological order (i.e., the most recent is on top). This page lists the entries published in December 2025: there is also a table of months at the end of this page, and an index of all entries. Some entries are classified into one or more “categories” (indicated at the end of the entry itself), but this organization isn't very coherent. The permalink of each entry is in its date, and it is also reproduced before and after the text of the entry itself.

[Index of all entries / Index de toutes les entréesLatest entries / Dernières entréesXML (RSS 1.0) • Recent comments / Commentaires récents]

Entries published in December 2025 / Entrées publiées en décembre 2025:

↓Entry #2842 [older| permalink|newer] / ↓Entrée #2842 [précédente| permalien|suivante] ↓

(mercredi)

La longueur des lignes et l'absurdité du style des pages Web

Je vais un peu redire ce que j'ai déjà dit il y a deux ans, mais peu importe.

Ce qui motive cette redite, c'est que mon dernier billet m'a valu le commentaire suivant, évidemment anonyme, qui se plaint de façon fort amène de la longueur des lignes de texte sur ce site :

T'as raison, utilise tous les pixels en largeur, faudrait pas que ça se perde, d'ailleurs tu devrais encore réduire les marges, elles sont encore à deux ou trois pixels.

Toujours agréable d'écrire un texte long comme un roman et de recevoir des réactions sur des points de forme, comme ça, de la part de gens qui n'ont de toute façon visiblement pas la moindre intention de lire le texte. Toujours agréable, aussi, de recevoir des commentaires agressifs et sarcastiques de la part de gens qui n'ont même pas le courage de laisser un nom. (Oui, ça m'arrive moi aussi de faire du sarcasme agressif, mais je le fais en mon nom, et généralement contre des généralités, pas contre des personnes individuelles identifiables à qui je m'adresse.) Et bien sûr, le reproche tombe complètement à plat puisque, précisément, j'ai prévu la possibilité de régler la longueur des lignes en plus de la taille du texte sur ce site (pour faire vite : cherchez le bouton en bas de la page avec l'icône ‘⚙’ et le texte Click for site settings) et qu'en plus, comme je vais le dire, même si je n'avais pas prévu ça, il y avait diverses façons de s'en sortir autrement.

Mais ça vaut la peine de s'attarder un instant sur l'absurdité bien réelle qui sous-tend ce commentaire désagréable, c'est-à-dire la situation du style sur le Web, et notamment sur un point qui ne déclenche pas la stupéfaction consternée qui serait méritée : pourquoi diable le style d'une page Web est-il complètement contrôlé par l'auteur de la page et en rien par le lecteur ?

Note : Pour éviter tout malentendu, je précise que le terme style, dans le contexte du Web et dans ce billet, fait référence à l'apparence : couleurs, polices de caractères, taille des caractères, largeur des lignes, emplacement du texte, ce genre de choses. (Je ne parle donc pas, disons, du style linguistique.) ❧ Par ailleurs, si vous avez besoin d'éclaircissements sur certains termes techniques, je rappelle que j'ai écrit un long billet pour vulgariser le fonctionnement du Web et des technologies comme HTML et compagnie.

Au début du HTML (c'est-à-dire pendant la première moitié des années 1990), il n'y avait pas de style à proprement parler. Le HTML décrivait de l'hypertexte, c'est-à-dire du texte avec des liens, éventuellement quelques éléments supplémentaires comme des titres de section, la possibilité de mettre du gras, de l'italique et du souligné, mais c'était à peu près tout. Pas question de changer de couleur, de police, ou d'autres fioritures du genre.

C'était peut-être un peu limité, mais rappelons-nous qu'avec cette limitation venait un avantage : si ce n'est pas la page Web qui fixe la police ou la taille de caractères, cela laisse la porte ouverte à l'utilisateur pour la choisir — et de fait, vers le milieu des années 1990 des navigateurs offraient cette possibilité (qui existe toujours, au demeurant : il y a un réglage de police par défaut dans mon Firefox ; mais c'est juste que maintenant ça n'a en gros aucun effet puisque chaque page Web trouve absolument indispensable d'imposer son propre look).

Mais simultanément, les navigateurs (les mêmes, c'est-à-dire en gros Netscape Navigator) se sont mis à permettre au HTML de régler la couleur, la police, la taille, ce genre de choses, et ça a abouti au Web de la fin des années 1990, tout clignotant de gifs animés et où tout le monde abusait des balises comme <font>.

Pour essayer de contrôler cette explosion on a inventé le CSS selon un principe vertueux de séparation du fond (confié au HTML) et de la forme (confiée au CSS) : c'est-à-dire que le CSS est un langage dans lequel on décrit le style à appliquer à une page Web, le HTML se bornant à décrire le contenu. Puis le CSS s'est complexifié à un rythme absolument hallucinant depuis le milieu des années 1990, et trouve quand même le moyen de faire toujours presque exactement ce qu'on veut mais à une petite limitation près qui fait qu'on ne peut pas s'en servir, et par ailleurs il est invraisemblablement confusant et plein de bizarreries incompréhensibles (voyez ici ou ou ou pour des exemples divers de limitations connes ou de comportements contre-intuitifs), mais ce n'est pas mon propos ici. Le problème est que, fondamentalement, personne n'a jamais vraiment cru à cette histoire de séparation du fond et de la forme, et les auteurs de pages Web se sont rués sur le CSS comme la vérole sur le bas-clergé breton, remplaçant simplement leurs balises <font> par des attributs style= ou éventuellement des feuilles de style avec des classes ad hoc, et souvent avec une tendance à micromanager le moindre détail ; mais le résultat pour l'utilisateur était et est toujours exactement le même : la personne qui décide essentiellement seule à quoi la page Web va ressembler est l'auteur de cette page.

Évidemment on peut me rétorquer que quand je lis un livre (ou un prospectus publicitaire, parce que beaucoup du Web ressemble plutôt à ça), ce n'est pas moi, le lecteur, qui décide à quoi ça ressemble, donc le problème n'est pas nouveau. (Et de fait, ça arrive que j'achète un livre et que j'aie du mal à le lire parce que je déteste vraiment la police de caractères utilisée, ou — ce qui m'arrive de plus en plus avec l'âge — que je trouve les caractères décidément trop petits.)

Oui mais justement la technologie offrait la possibilité de faire mieux. Et elle n'a pas réalisé cette promesse.

Soyons bien clairs : je ne conteste pas l'idée que l'auteur d'une page Web ait un certain contrôle sur l'apparence de celle-ci (ne serait-ce que le branding : mettre un petit logo quelque part, c'est raisonnable). L'idée de séparer complètement le fond et la forme est, au demeurant, assez illusoire : le HTML n'a pas, par exemple, de concept de paragraphe important ou aparté, donc au mieux ce que je vais pouvoir faire pour mettre en relief un paragraphe important ou au contraire le marquer comme secondaire, c'est lui donner une classe CSS spéciale et ajouter des règles de style qui servent à afficher un bord autour ou diminuer la taille des caractères ; et ensuite, si je dis dans le texte comme je l'ai dit dans le paragraphe encadré ci-dessus ou comme je vais le dire en petits caractères plus loin, je viole le principe de séparation de fond et de forme et je ne vois pas bien comment on peut éviter ça complètement sans limiter sévèrement l'expressivité du Web. Donc il faut bien que l'auteur d'un site Web ait la possibilité de mettre au moins un peu de style.

Mais les technologies Web actuelles ne permettent même pas un partage (souhaitable !) des responsabilités selon lequel, au moins pour un texte qui est généralement assez basique, ce serait l'utilisateur, i.e. le lecteur, qui choisit la police qu'il trouve la plus agréable, la taille de caractères qui convient le mieux à son confort de lecture, la longueur des lignes, les marges, les couleurs, ce genre de choses, et la page Web imposerait le style pour des éléments indispensables à son branding ou bien à la bonne compréhension du texte (encadrés, apartés et notes, légende des images, ce genre de choses).

Je conviens que c'est un peu compliqué de prévoir un style partiellement fixé par l'auteur de la page et partiellement fixé par l'utilisateur : par exemple parce que l'auteur ne peut pas pleinement tester toutes les possibilités (mais bon, il ne peut déjà pas pleinement tester toutes les possibilités de largeur d'écran ou de fenêtre !) et parce que c'est plus difficile de concevoir un style quand on n'a pas tous les éléments. (Le choix des polices pose par exemple la difficulté que toutes n'interagissent pas bien avec tous les caractères Unicode.) Mais le fait est qu'actuellement il n'y a même pas un début d'effort dans cette direction.

Alors oui, bien sûr, quand on conçoit un site Web, on peut prévoir un mécanisme de configurabilité de l'apparence (le JavaScript permet à peu près n'importe quoi). Mais d'abord il faut se fatiguer à l'écrire, ce qui n'est pas du tout évident (surtout quand, comme moi, on n'est pas du tout expert en JavaScript et encore moins en CSS), ça va alourdir tout le site, et potentiellement provoquer des artefacts d'affichage le temps que le JavaScript s'active, et surtout, ce qui rend cette idée absurde, c'est que chaque site Web devrait mettre en place son propre mécanisme de configuration séparé, sans que le navigateur ne joue de rôle de coordinateur, et que l'utilisateur devrait rentrer ses préférences de police, taille, longueur de ligne, etc., une fois séparément pour chaque site qu'il utilise (donc avec un mécanisme différent à chaque fois), au lieu de les saisir une fois pour toutes dans le navigateur. Un site Web n'a même pas de mécanisme pour interroger l'utilisateur et savoir si, par hasard, il aurait une préférence pré-remplie sur certaines variables standardisées. Il n'y a même pas de bonnes pratiques documentées sur la manière de faire. (Et c'est pour ça que, bien que j'aie maintenant un mécanisme pour régler la longueur des lignes sur ce site, les gens ne le voient pas et se plaignent.)

Tout ça est profondément con.

Ce n'est pas mon boulot de décider comment vous lisez mon site Web. C'est vous qui le lisez, ça devrait être à vous de choisir ce qui vous plaît, pas à moi. Moi j'ai juste envie de dire au navigateur fais ce qui est le mieux pour l'utilisateur pour lequel tu travailles : c'est ton boulot de lui demander et de lui permettre de choisir — mais le CSS ne permet rien de tel. Du coup, j'ai fait des choix qui me conviennent, parce que je suis quand même un lecteur important de mon propre site, et si ça ne vous convient pas, ben je suis désolé, mais ce n'est pas moi qui ai conçu le Web.

Alors, ce n'est pas tout à fait vrai qu'on ne peut rien faire, il y a de petits bricolages.

↑Entry #2842 [older| permalink|newer] / ↑Entrée #2842 [précédente| permalien|suivante] ↑

↓Entry #2841 [older| permalink|newer] / ↓Entrée #2841 [précédente| permalien|suivante] ↓

(vendredi)

Introduction aux mathématiques constructives : 4. suites de réels et principes analytiques d'omniscience

Je continue (et termine ?) ma série d'introduction aux mathématiques constructives en parlant maintenant de suites de réels et de principes analytique d'omniscience. Ce billet (partie 4) est la continuation directe de celui d'il y a trois jours, et contrairement à ceux d'avant qui étaient un peu indépendants, celui-ci fait directement suite à la partie 3 puisque, en fait, j'ai coupé un texte extrêmement long en deux. Néanmoins, j'ai quand même ajouté un bref récapitulatif au début avec les choses les plus importantes à retenir de la partie 3.

Table des matières (de toute la série)

Récapitulatif des points essentiels de l'épisode précédent

Pour la commodité du lecteur, je recopie ici les points qui me semblent les plus importants du billet précédent.

‣ Un nombre réel ou coupure de Dedekind est un couple (S,T) de parties de ℚ, vérifiant :

  1. S et T sont habités : ∃r∈ℚ.(rS) et ∃r∈ℚ.(rT) ;
  2. S est un ensemble inférieur et T est un ensemble supérieur : ∀r∈ℚ.∀r′∈ℚ.((r′<rrS) ⇒ r′∈S) et ∀r∈ℚ.∀r′∈ℚ.((r′>rrT) ⇒ r′∈T) ;
  3. S est ouvert vers le haut, et T est ouvert vers le bas : ∀r∈ℚ.(rS ⇒ ∃r′∈ℚ.(r′>rr′∈S)) et ∀r∈ℚ.(rT ⇒ ∃r′∈ℚ.(r′<rr′∈T)) ;
  4. tout élément de S est strictement plus petit que tout élément de T : soit ∀s∈ℚ.∀t∈ℚ.((sStT) ⇒ (s<t)) ;
  5. si un rationnel est strictement plus petit qu'un autre, alors soit le plus petit est dans S, soit le plus grand est dans T : soit ∀s∈ℚ.∀t∈ℚ.((s<t) ⇒ (sStT)).

‣ On définit deux relations binaires sur l'ensemble ℝ des nombres réels, appelées ‘≤’ (l'ordre large) et ‘<’ (l'ordre strict), de la façon suivante :

  • on pose (S,T) ≤ (S′,T′) (ou, de façon synonyme, (S′,T′) ≥ (S,T)) lorsque SS′, ou, ce qui revient au même, TT′ ;
  • on pose (S,T) < (S′,T′) (ou, de façon synonyme, (S′,T′) > (S,T)) lorsqu'il existe d>0 rationnel tel que S+dS′, ou, ce qui revient au même, lorsque TS′ est habité.

Ces relations généralisent celles du même nom sur ℚ. La relation stricte ‘<’ implique la relation large ‘≤’. Les deux relations ‘<’ et ‘≤’ sont transitives ; ‘<’ est irréflexive et strictement antisymétrique, tandis que ‘≤’ est réflexive et antisymétrique au sens large ; on a aussi la transitivité mixte (si x<yz, ou si xy<z, alors on a x<z). Par ailleurs, si x = (x, x) où x := {s∈ℚ : s<x} et x := {t∈ℚ : t>x}.

‣ L'ensemble ℚ est dense et cofinal dans ℝ, c'est-à-dire que si x<x′ sont des réels, il r rationnel tel que x<r<x′, et si si x est un réel, il existe r et r′ rationnels tels que r<x<r′.

‣ L'ordre large est la négation de l'ordre strict de sens contraire, c'est-à-dire que xy équivaut à ¬(x>y). Notamment, x=y équivaut à ¬(xy) où ‘⋕’, défini par xy :⇔ (x<yx>y), s'appelle le discernement standard sur ℝ.

On ne peut pas affirmer que pour tous réels x,y on ait xy ou bien xy. Néanmoins, on a la propriété essentielle suivante :

(❀) : Si x<x′ et y sont des réels, on a soit x<y soit y<x′.

‣ On note xy pour ¬(xy) ou, ce qui est équivalent, xy ∧ ¬(x=y) (cette relation xy est impliquée par x<y, mais on ne peut pas affirmer que ce soit équivalent).

‣ Deux réels x,y ont toujours une borne supérieure xy caractérisée par le fait que xyz si et seulement si xz et yz. Elle vérifie de plus les propriétés que ① xy < z si et seulement si x<z et y<z, et ② z < xy si et seulement si z<x ou bien z<y. (En revanche, on ne peut pas affirmer qu'on ait zxy si et seulement si zx ou bien zy.) Les propriétés duales valent pour la borne inférieure xy.

‣ On définit une addition sur les réels qui prolonge celle de ℚ et fait d'eux un ℚ-espace vectoriel, avec de plus la compatibilité à l'ordre : on a xy si et seulement si yx ≥ 0 et x<y si et seulement si yx > 0 ; si x≥0 et y≥0 alors x+y ≥ 0 ; si x>0 et y>0 (ou même seulement x>0 et y≥0) alors x+y > 0 ; si x>0 alors r·x > 0 pour tout r>0 rationnel, et −x < 0.

‣ On définit aussi une multiplication sur les réels qui prolonge celle de ℚ et fait d'eux une ℚ-algèbre commutative, avec de plus la compatibilité à l'ordre : si x≥0 et y≥0 alors x·y ≥ 0 ; si x>0 et y>0 alors x+y > 0.

‣ La valeur absolue d'un réel se définit par |z| := z⊔(−z). Ainsi, on a toujours |z|≥0. On a |xy| = (xy) − (xy). On a l'inégalité triangulaire habituelle |x+y| ≤ |x| + |y|. On a de plus : |x·y| = |x|·|y|.

La propriété |z|>0 équivaut à z>0 ∨ z<0 (ce qu'on a par ailleurs noté z⋕0). Cela équivaut aussi à l'inversibilité de z pour la multiplication.

Infima et suprema sur les réels

☞ Quelques difficultés

Classiquement, toute partie A⊆ℝ non vide et minorée admet une borne inférieure (une borne inférieure de A est un plus grand minorant, s'il existe, autrement dit, z est une borne inférieure de A signifie d'une part que z minore A, i.e. ∀tA.(zt), et d'autre part que si x minore A alors xz, i.e. ∀x∈ℝ.((∀tA.(xt)) ⇒ xz)). On a vu que, constructivement, toute partie finiment énumérée et habitée {z1,…,zk} (avec k≥1) de ℝ admet une borne inférieure z1⊓⋯⊓zk et une borne supérieure z1⊔⋯⊔zk. Néanmoins, constructivement, on ne peut pas affirmer que toute partie non vide et minorée, ni même toute partie habitée et minorée, possède une borne inférieure. Un contre-exemple brouwérien est vite trouvé :

Contre-exemple brouwérien : Si toute partie habitée et minoré de ℝ possède une borne inférieure, alors pour tout p∈Ω on a ¬p ∨ ¬¬p (la loi faible du tiers exclu).

(Notamment, on ne peut pas affirmer que toute partie habitée et minoré de ℝ possède une borne inférieure, puisqu'on ne peut pas affirmer la loi faible du tiers exclu, cf. ci-dessous)

Démonstration : Si p est une valeur de vérité, considérons la partie A := {0 : p} ∪ {1} de ℝ, c'est-à-dire {t∈ℝ : (t=0 ∧ p) ∨ (t=1)}. Supposons que A ait une borne inférieure z. D'après la proposition (❀) on doit avoir soit z>0 soit z<1. Dans le premier cas (z>0), comme z est un minorant de A, on a ¬(0∈A), c'est-à-dire qu'on a ¬p. Dans le second cas (z<1), 1 n'est pas un minorant de A, donc ¬p est impossible (car ¬p implique que A={1}) : c'est donc que ¬¬p. Bref, on a montré ¬p ∨ ¬¬p. ∎

La loi faible du tiers exclu n'est pas la même chose que la loi du tiers exclu (elle ne l'implique pas), mais c'est néanmoins, comme les différents principes d'omniscience évoqués plus hauts, un « tabou » constructif, et il est donc standard de s'en servir pour des contre-exemples brouwériens.

On remarquera que la démonstration ci-dessus montre même que si toute partie habitée de ℕ possède une borne inférieure, la loi faible du tiers exclu vaut (et j'avais déjà fait remarquer qu'exactement le même contre-exemple montre que si toute partie habitée de ℕ possède un plus petit élément, la loi du tiers exclu vaut).

Pour ce qui est des réels étendus bornés (définis, je le rappelle, par les coupures de MacNeille, c'est-à-dire en affaiblissant (e) en (e⁻)), j'ai déjà expliqué dans la section les concernant que le principe de la borne inférieure vaut pour eux, et d'ailleurs on peut même les définir comme le complété des rationnels — ou, du coup, des réels de Dedekind — pour la propriété de la borne inférieure. Le contre-exemple brouwérien donné ci-dessus montre du coup que l'égalité des coupures de MacNeille et de Dedekind implique la loi faible du tiers exclu, et je l'ai déjà commenté.

Cet exemple montre essentiellement qu'on doit décider de sacrifier soit la propriété de la borne inférieure soit la propriété (❀) (sauf à avoir la loi faible du tiers exclu, ce qui est un tabou) : les coupures de Dedekind font le choix de sacrifier la première (tandis que les coupures de MacNeille font le choix de sacrifier la seconde, mais elles sont beaucoup moins utiles). Maintenant, il est quand même bien pratique de pouvoir prendre des bornes inférieures : je vais chercher à donner une propriété d'une partie A⊆ℝ qui assure son existence.

☞ Borne inférieure (faible) versus infimum (fort)

Mais tout d'abord, il faut revoir la définition, et introduire une distinction :

  • Si A⊆ℝ, on dit que z est la borne inférieure ou inf faible de A lorsque z est le plus grand minorant de A, c'est-à-dire [je recopie la définition ci-dessus] que z minore A, i.e. ∀tA.(zt), et d'autre part que si x minore A alors xz, i.e. ∀x∈ℝ.((∀tA.(xt)) ⇒ xz).

  • Si A⊆ℝ, on dit que z est l'infimum ou inf (fort) de A lorsque z minore A, i.e. ∀tA.(zt), et d'autre part que si x>z alors il existe un élément de A entre les deux, i.e. ∀x∈ℝ.(z<x ⇒ ∃tA.(t<x)).

On fait évidemment les définitions duales de borne supérieure (ou sup faible) et de supremum (ou sup (fort)) en inversant toutes les inégalités.

La terminologie est de moi. En anglais on utilise généralement (mais pas systématiquement) greatest lower bound pour la première notion, et infimum pour la seconde. J'ai essayé de dire quelque chose de cohérent et pas trop idiot.

Classiquement, ces notions sont équivalentes, puisque la première condition (minorer A) est la même, et que la seconde est juste écrite sous forme contraposée.

Constructivement, la borne inférieure, si elle existe, est forcément unique (c'est évident), et d'autre part, l'inf, s'il existe, est la borne inférieure (car la condition (∀tA.(xt)) ⇒ xz est exactement (¬∃tA.(t<x)) ⇒ ¬(z<x), qui est logiquement impliquée par z<x ⇒ ∃tA.(t<x)). Mais on ne peut pas affirmer que la borne inférieure, même si elle existe, est forcément l'inf, à cause de la proposition suivante :

Proposition : Si toute partie de ℝ possédant une borne inférieure possède un infimum (fort !), alors la loi du tiers exclu vaut.

↑Entry #2841 [older| permalink|newer] / ↑Entrée #2841 [précédente| permalien|suivante] ↑

↓Entry #2840 [older| permalink|newer] / ↓Entrée #2840 [précédente| permalien|suivante] ↓

(mardi)

Introduction aux mathématiques constructives : 3. les nombres réels et leur ordre

Je continue ma série d'introduction aux mathématiques constructives en parlant maintenant de nombres réels. Ce billet s'inscrit dans une série dont la table des matières est reproduite ci-dessous (j'y ai rétroactivement intégré ce billet plus ancien comme partie 0) : il n'est pas forcément nécessaire d'avoir complètement lu tous ceux qui précèdent, mais c'est sans doute une bonne idée d'avoir regardé l'avant-propos expliquant de quoi il est question (et/ou la partie sur les motivations et principes de la partie 0).

Table des matières (de toute la série)

Introduction

Méta : Ce billet a une histoire mouvementée (oserais-je dire tourmentée) : je le traîne depuis 2022 environ, où j'avais commencé à écrire un texte super long que j'ai ensuite coupé en parties et dont j'avais déjà publié les deux premières (ici et , cf. la table des matières ci-dessus) sous forme de feuilleton en 2024, mais cette troisième partie (que j'avais déjà annoncée) était plus difficile à publier telle quelle, parce qu'elle était très inachevée (en gros elle s'arrêtait au niveau de la partie sur les bornes inf et sup), donc je ne l'ai pas fait au même moment. Plusieurs fois j'ai voulu m'y remettre, et plusieurs fois j'ai abandonné. Mais je continue à avoir dans un coin de la tête l'idée d'écrire un livre sur les maths constructives (j'en ai récemment reparlé à un ami-et-collègue), dont ces billets pourraient former la trame essentielle ; et aussi, je voulais vraiment mettre en ligne quelque chose sur les principes analytiques d'omniscience pour pouvoir m'y référer. Bref, je m'y suis remis une fois de plus, et cette fois aura été la bonne. Néanmoins, il y a eu toutes sortes de difficultés que je n'attendais pas, qui ont donné naissance à des sortes de digressions dans le présent billet (que j'encourage à ne pas lire dans un premier temps, et que je signale au début des sections correspondantes, mais que j'ai incluses par complétude) : sur les coupures de MacNeille, le principe que je qualifie de WLLPO analytique, et tout ce qui tourne autour du principe de Markov faible ; chacun de ces passages a été beaucoup plus long et fastidieux que prévu. Bref, tout ceci a été plus laborieux que je ne l'attendais. En plus de ça, comme ça devenait vraiment trop long même par rapport à mes standards habituels de billets interminables, j'ai coupé en deux ce qui devait initialement être une seule partie : ce qui suit est donc la partie 3 de ma série, et une partie 4 (sur les suites de réels et principes analytiques d'omniscience) apparaîtra d'ici quelques jours. Aussi, pour ces raisons, les démonstrations ont été très peu relues, donc il est absolument certain qu'il subsiste un certain nombre d'erreurs, que j'espère ne pas être trop graves.

(Je passe maintenant la parole, en gros, au David Madore de 2022.)

Discussion préalable : quels nombres réels ? et ce qui nous attend

☞ Entiers et rationnels ressemblent aux maths classiques

J'ai déjà expliqué (notamment dans un bout d'une entrée précédente sur le sujet) que les entiers naturels en maths constructives ne se comportent « pas très différemment » des maths classiques (l'affirmation technique précise étant que tout énoncé arithmétique Π₂ classiquement démontrable est encore intuitionnistement démontrable, et ceci recouvre en gros « tout ce qu'on peut tester algorithmiquement ») : les propriétés usuelles des opérations algébriques (commutativité, associativité) et de l'ordre, mais aussi des choses comme la division euclidienne, l'existence et l'unicité de la décomposition en facteurs premiers, ce genre de choses est valable en logique intuitionniste sans qu'on ait besoin d'y réfléchir.

Je rappelle notamment que ℕ est discret comme ensemble, c'est-à-dire que pour m et n deux entiers naturels on a (m=n) ∨ ¬(m=n) (deux entiers naturels sont soit égaux soit non égaux), donc il n'y a pas à finasser autour de la notion de discernement, et on peut noter mn (ou bien mn) pour ¬(m=n). De même, on a (m=n) ∨ (m<n) ∨ (m>n) (ces trois cas étant exclusifs, c'est-à-dire qu'exactement un des trois vaut), donc les choses se comportent exactement comme on s'y attend classiquement : ¬(m=n) équivaut à (m<n) ∨ (m>n), et mn équivaut à (m=n) ∨ (m<n) et ainsi de suite.

Les entiers relatifs ℤ et les rationnels ℚ, dont je vais dire un mot ci-dessous, sont construits et se comportent eux aussi en maths constructives comme en maths classiques : par exemple, algébriquement ℤ est un anneau (définition habituelle) et ℚ est un « corps » selon n'importe quelle définition raisonnable qu'on peut écrire d'un corps (p.ex., un anneau dans lequel un élément est nul si et seulement si il n'est pas inversible). Ces deux ensembles sont, de plus, discrets, c'est-à-dire que (x=y) ∨ ¬(x=y) vaut sur les entiers comme sur les rationnels. (Attention, je dis que ℚ est discret en tant qu'ensemble, un concept qui n'a d'intérêt qu'en maths constructives : on peut mettre une topologie sur ℚ et il n'est pas discret en tant qu'espace topologique, mais ce n'est pas ce dont je parle ici.) L'ordre sur les entiers relatifs et les rationnels se comporte aussi comme on s'y attend : on a (x=y) ∨ (x<y) ∨ (x>y) (ces trois cas étant exclusifs, c'est-à-dire qu'exactement un des trois vaut), donc notamment : ¬(x=y) équivaut à (x<y) ∨ (x>y), et xy équivaut à (x=y) ∨ (x<y) et ainsi de suite.

☞ Réels de Dedekind vs. réels de Cauchy

Il en sera bien différemment des réels. Mais avant de discuter de comment les réels se comportent en maths constructives, il faut se demander : quels réels ?

Classiquement, il y a deux constructions standards des nombres réels, et elles sont équivalentes : la construction de Cauchy, et la construction de Dedekind. La construction de Cauchy part des suites de rationnels vérifiant une condition de Cauchy (∀ε>0.∃n∈ℕ.∀pn.∀qn.|upuq|<ε) et quotiente par la relation qui identifie deux suites lorsque leur différence tend vers zéro (uv lorsque ∀ε>0.∃n∈ℕ.∀kn.|ukvk|<ε) : un nombre réel de Cauchy est donc une classe d'équivalence de suites de Cauchy de rationnels. La construction de Dedekind, elle, définit un nombre réel par l'ensemble des rationnels plus petits ou plus grands que lui, ou, de façon plus élégante, les deux à la fois : on dira plus bas les les conditions qui définissent précisément une telle « coupure » de ℚ, mais en gros, un réel va être défini comme une coupure, une coupure étant la donnée de deux ensembles de rationnels (ceux qui sont plus petits que le réel qu'on veut définir et ceux qui sont plus grands).

Ces deux constructions classiquement équivalentes peuvent être définies en maths constructives. Elles sont encore équivalentes à condition qu'on dispose d'un petit peu d'axiome du choix (l'axiome du choix dénombrable suffit largement). Mais en maths constructives sans axiome du choix, on doit distinguer les réels de Cauchy et les réels de Dedekind.

Les réels de Dedekind (dont une définition précise va suivre) sont les plus généraux (i.e., on peut considérer les réels de Cauchy comme un sous-ensemble, et même un sous-« corps », des réels de Dedekind), et ils se comportent plutôt mieux de divers points de vue (par exemple, ils ont les meilleures propriétés de complétude) : de nombreux auteurs sont donc d'accord pour les appeler tout simplement les réels, et c'est ce que je ferai. Autrement dit, pour moi, sauf précision expresse du contraire, un nombre réel, c'est un réel de Dedekind.

Les réels de Cauchy ne sont pas pour autant sans intérêt : par exemple, ils peuvent être préférables à étudier dans un contexte informatique (les réels de Cauchy ont plus de contenu informationnel que les réels de Dedekind) ou dans le cadre d'une théorie des ensembles faible (où se donner une suite de rationnels ne pose pas de problème mais se donner un ensemble de rationnels est plus problématique). Il y a aussi le fait que Bishop, qui travaillait avec l'axiome du choix dénombrable (ce qui rend les réels de Cauchy et de Dedekind égaux), voyait les réels comme des réels de Cauchy, et beaucoup de gens l'ont suivi. Mais il faut faire attention parce que, en maths constructives en l'absence de l'axiome du choix, non seulement il faut distinguer les réels de Cauchy des réels de Dedekind, mais en plus il y a à distinguer différentes sortes de réels de Cauchy, notamment selon qu'on part des suites vérifiant la condition de Cauchy (∀ε>0.∃n∈ℕ.∀pn.∀qn.|upuq|<ε) ou bien une version plus explicite qui impose un module de convergence (du style ∀N∈ℕ.∀pN.∀qN.|upuq|<2N) : certains auteurs utilisent le terme réel de Cauchy dans le premier sens, d'autres dans le second, et le sens n'est pas toujours très clairement explicité ni l'ambiguïté signalée. (Je propose de parler de réels de Cauchy modulés pour ceux qui ont un module de convergence.) En plus de ça, on peut s'interroger sur la pertinence de l'idée de prendre des suites de Cauchy et de quotienter vu que l'ensemble des réels de Cauchy n'est pas forcément Cauchy-complet(!). Bref, les réels de Cauchy sont, selon moi, bien plus bizarres et plus problématiques que les réels de Dedekind : je dirais qu'il faut les considérer comme une tentative de complétion partielle, dont il est intéressant de regarder les limitations, mais qui n'est pas vraiment la bonne notion de nombre réel.

Bref, je vais parler, moi, essentiellement des réels de Dedekind.

Deux intuitions préalables possibles (et un mot sur le regard externe)

☞ Le problème de parler de façon « purement interne »

Le parti-pris global de cette série de billets est de parler de mathématiques constructives de façon purement interne, c'est-à-dire sans référence à un monde mathématique externe classique depuis lequel notre monde constructif serait vu (par exemple, comme un topos, notion que je n'ai pas envie de définir). Autrement dit : on fait directement des maths en logique intuitionniste, sans se demander si nos ensembles sont des objets dans un topos ou quelque chose comme ça. C'est tout à fait possible et tout à fait légitime, et plus simple quand il s'agit d'expliquer les choses, néanmoins, ça n'aide pas forcément à se forger une intuition.

Et quand on parle de nombres réels, je pense que l'absence d'intuition qui peut accompagner cette approche purement interne devient vraiment problématique : j'ai peur que beaucoup de lecteurs, si on leur dit qu'on ne peut pas l'affirmer en maths constructives que tout réel z vérifie z≥0 ou bien z≤0 (ce que j'appellerai plus bas LLPO analytique), se contentent de lever les yeux au ciel en se disant que c'est une forme de masturbation intellectuelle, une sorte de défi consistant à boxer sans ses poings, un exercice quasiment oulipien, parce que nous sommes tellement persuadés que dans le vrai monde réel, un nombre est soit positif soit négatif. Bref, qu'ils abandonnent leur lecture ici. Bon, en fait, j'aurais sans doute mieux fait de m'inquiéter à ce sujet il y a deux ou trois billets, parce que si on est arrivé jusque là, probablement on n'est pas si hostile aux maths constructives. Mais même en étant raisonnablement enclin à en savoir plus, on risque d'être dérouté par le manque d'intuition sur ce que ça peut « vouloir dire ». Or en fait, c'est quelque chose qui peut vraiment intéresser l'analyse numérique où, si on a un nombre réel qu'on est capable d'approcher à n'importe quelle précision voulue, on n'est pas pour autant forcément capable de décider (algorithmiquement en temps fini) si z≥0 ou z≤0. Mais évidemment ceci demande de prendre un point de vue au moins partiellement externe, ou disons de réinterpréter la logique en se disant que l'affirmation interne z≥0 ou z≤0 peut peut-être se comprendre au moins en partie comme je suis capable de dire si z≥0 ou si z≤0.

Donc, même sans développer le point de vue externe qui rendrait les intuitions qui suivent formellement justifiées, je pense qu'il est pertinent que je les mentionne comme une intuition à garder dans le coin de la tête sur ce que « peuvent être » les nombres réels des maths constructives. Voici donc deux intuitions possibles qui peuvent peut-être aider à imaginer de quoi cause toute la suite de ce billet.

☞ Deux intuitions possibles sur les réels constructifs

⚠ Mise en garde : Il est toujours délicat de communiquer une intuition mathématique, et il y a toujours le risque d'embrouiller plus qu'on n'aide. Et ce, d'autant plus fortement que je cherche à les décrire de façon informelle, et que je m'exprime peut-être très mal, donc peut-être que certains lecteurs trouveront ce qui suit absolument sibyllin. On peut les ces deux points de vue précis en parlant de topoï ; mais on peut aussi préférer les ignorer complètement et se contenter de connaître les règles du jeu des maths constructives. Quoi qu'il en soit, ce qui suit vaut ce que ça vaut.

Intuition calculatoire : Dans une première intuition, un nombre réel en maths constructives est (enfin, peut être) un nombre calculé par un certain processus, par exemple algorithmique mais pas forcément, qui est capable de renvoyer des approximations arbitrairement bonnes. Le point crucial qu'on attend de ce processus est que si s,t sont deux rationnels (pour simplifier) tels que s<t, et z le réel que notre processus calcule, alors en calculant suffisamment, on doit être capable d'obtenir la conviction que z<t ou bien que z>s (ces deux cas n'étant pas exclusifs, et en fait on ne peut jamais faire de disjonction exclusive parce qu'il subsiste toujours une certaine incertitude sur notre nombre). C'est exactement cette propriété qui va servir de base ci-dessous à la propriété (e) de la définition des coupures de Dedekind. Par ailleurs, il faut comprendre la disjonction constructive comme forte : pour pouvoir prétendre affirmer PQ il faut être capable d'affirmer l'un des deux termes de la disjonction. Dès lors, il n'est pas surprenant qu'on ne puisse pas affirmer que z≥0 ou bien z≤0, parce que cela reviendrait à être capable de placer z, ne serait-ce qu'au sens large, d'un côté de l'origine, ce qui n'est pas possible en interrogeant le processus pour savoir si z<t ou bien que z>s.

Cette intuition est notamment rendue rigoureuse par le topos effectif (dont j'ai parlé dans ce billet), dans lesquels les nombres réels de Dedekind sont essentiellement les réels calculables (au sens, disons, où on dispose d'un algorithme qui, pour tout n, est capable de calculer une approximation rationnelle à 2n près du réel considéré). Dans le topos effectif ainsi que toutes sortes de variations, le principe de Markov analytique (qui sera défini proprement ci-dessous, mais qui affirme que si z n'est pas nul alors soit z<0 soit z>0) est valable, mais on peut quand même garder une intuition plus générale dans laquelle ¬(z=0) signifie qu'il est impossible que le nombre qu'on cherche à approcher soit nul, mais ce n'est pas pour autant qu'on arrive à trouver moyen de le discerner de zéro (donc de le placer d'un côté ou de l'autre de l'origine).

Intuition topologique : Dans une seconde intuition, un nombre réel en maths constructives est (enfin, peut être) une fonction continue sur un espace de possibilités (imaginez un espace topologique quelconque). Donc une affirmation comme z≥0 vaut dans certains endroits de notre espace des possibles et pas dans d'autres. Mais le point crucial ici est qu'on suppose qu'une affirmation se comprend comme définissant un domaine ouvert de l'espace des possibles, selon le principe qu'on ne peut vraiment affirmer quelque chose en un point que si ce quelque chose est vrai tout autour de ce point (la vérité est locale). Pour quelque chose comme z>0, le domaine en question sera donc bien l'ouvert sur lequel la fonction z est strictement positive, mais pour z≥0 ou bien z=0 ce sera l'intérieur de l'ensemble des points où cette propriété vaut. Dès lors, , il n'est pas surprenant qu'on ne puisse pas affirmer que z≥0 ou bien z≤0, parce que cela demanderait que pour tout point de notre espace de possibles, on ait soit un voisinage sur lequel z≥0 soit un voisinage sur lequel z≤0, et la simple fonction identité sur les réels (classiques !) met cette idée en défaut autour de 0.

Cette intuition est essentiellement rendue rigoureuse par les topos de faisceaux (sur un espace topologique, ou, si on est audacieux, une « locale »), dans lesquels les nombres réels de Dedekind sont le faisceau des fonctions continues à valeurs dans ℝ (les réels classiques).

↑Entry #2840 [older| permalink|newer] / ↑Entrée #2840 [précédente| permalien|suivante] ↑

Continue to older entries. / Continuer à lire les entrées plus anciennes.


Entries by month / Entrées par mois:

2025 Jan 2025 Feb 2025 Mar 2025 Apr 2025 May 2025 Jun 2025 Jul 2025 Aug 2025 Sep 2025 Oct 2025 Nov 2025 Dec 2025
2024 Jan 2024 Feb 2024 Mar 2024 Apr 2024 May 2024 Jun 2024 Jul 2024 Aug 2024 Sep 2024 Oct 2024 Nov 2024 Dec 2024
2023 Jan 2023 Feb 2023 Mar 2023 Apr 2023 May 2023 Jun 2023 Jul 2023 Aug 2023 Sep 2023 Oct 2023 Nov 2023 Dec 2023
2022 Jan 2022 Feb 2022 Mar 2022 Apr 2022 May 2022 Jun 2022 Jul 2022 Aug 2022 Sep 2022 Oct 2022 Nov 2022 Dec 2022
2021 Jan 2021 Feb 2021 Mar 2021 Apr 2021 May 2021 Jun 2021 Jul 2021 Aug 2021 Sep 2021 Oct 2021 Nov 2021 Dec 2021
2020 Jan 2020 Feb 2020 Mar 2020 Apr 2020 May 2020 Jun 2020 Jul 2020 Aug 2020 Sep 2020 Oct 2020 Nov 2020 Dec 2020
2019 Jan 2019 Feb 2019 Mar 2019 Apr 2019 May 2019 Jun 2019 Jul 2019 Aug 2019 Sep 2019 Oct 2019 Nov 2019 Dec 2019
2018 Jan 2018 Feb 2018 Mar 2018 Apr 2018 May 2018 Jun 2018 Jul 2018 Aug 2018 Sep 2018 Oct 2018 Nov 2018 Dec 2018
2017 Jan 2017 Feb 2017 Mar 2017 Apr 2017 May 2017 Jun 2017 Jul 2017 Aug 2017 Sep 2017 Oct 2017 Nov 2017 Dec 2017
2016 Jan 2016 Feb 2016 Mar 2016 Apr 2016 May 2016 Jun 2016 Jul 2016 Aug 2016 Sep 2016 Oct 2016 Nov 2016 Dec 2016
2015 Jan 2015 Feb 2015 Mar 2015 Apr 2015 May 2015 Jun 2015 Jul 2015 Aug 2015 Sep 2015 Oct 2015 Nov 2015 Dec 2015
2014 Jan 2014 Feb 2014 Mar 2014 Apr 2014 May 2014 Jun 2014 Jul 2014 Aug 2014 Sep 2014 Oct 2014 Nov 2014 Dec 2014
2013 Jan 2013 Feb 2013 Mar 2013 Apr 2013 May 2013 Jun 2013 Jul 2013 Aug 2013 Sep 2013 Oct 2013 Nov 2013 Dec 2013
2012 Jan 2012 Feb 2012 Mar 2012 Apr 2012 May 2012 Jun 2012 Jul 2012 Aug 2012 Sep 2012 Oct 2012 Nov 2012 Dec 2012
2011 Jan 2011 Feb 2011 Mar 2011 Apr 2011 May 2011 Jun 2011 Jul 2011 Aug 2011 Sep 2011 Oct 2011 Nov 2011 Dec 2011
2010 Jan 2010 Feb 2010 Mar 2010 Apr 2010 May 2010 Jun 2010 Jul 2010 Aug 2010 Sep 2010 Oct 2010 Nov 2010 Dec 2010
2009 Jan 2009 Feb 2009 Mar 2009 Apr 2009 May 2009 Jun 2009 Jul 2009 Aug 2009 Sep 2009 Oct 2009 Nov 2009 Dec 2009
2008 Jan 2008 Feb 2008 Mar 2008 Apr 2008 May 2008 Jun 2008 Jul 2008 Aug 2008 Sep 2008 Oct 2008 Nov 2008 Dec 2008
2007 Jan 2007 Feb 2007 Mar 2007 Apr 2007 May 2007 Jun 2007 Jul 2007 Aug 2007 Sep 2007 Oct 2007 Nov 2007 Dec 2007
2006 Jan 2006 Feb 2006 Mar 2006 Apr 2006 May 2006 Jun 2006 Jul 2006 Aug 2006 Sep 2006 Oct 2006 Nov 2006 Dec 2006
2005 Jan 2005 Feb 2005 Mar 2005 Apr 2005 May 2005 Jun 2005 Jul 2005 Aug 2005 Sep 2005 Oct 2005 Nov 2005 Dec 2005
2004 Jan 2004 Feb 2004 Mar 2004 Apr 2004 May 2004 Jun 2004 Jul 2004 Aug 2004 Sep 2004 Oct 2004 Nov 2004 Dec 2004
2003 May 2003 Jun 2003 Jul 2003 Aug 2003 Sep 2003 Oct 2003 Nov 2003 Dec 2003

[Index of all entries / Index de toutes les entréesLatest entries / Dernières entréesXML (RSS 1.0) • Recent comments / Commentaires récents]