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)
Partie 0 (histoire, motivations et principes) :
Partie 1 (un peu de théorie des ensembles) :
- Avant-propos
- Rappel du contexte et quelques notations
- Ensembles vides et habités, singletons, sous-terminaux, valeurs de vérité
- Produits, fonctions, injections, surjections, bijections
- L'ensemble Ω des valeurs de vérité
- Quelques notions constructives sans intérêt en maths classiques
- L'axiome du choix (ne sera pas admis)
Partie 2 (entiers naturels et principes d'omniscience) :
Partie 3 (les nombres réels et leur ordre) :
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 là, 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 m≠n (ou bien m⋕n) 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 m≤n é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 x≤y é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∈ℕ.∀p≥n.∀q≥n.|up−uq|<ε) et quotiente par la relation qui identifie deux suites lorsque leur différence tend vers zéro (u∼v lorsque ∀ε>0.∃n∈ℕ.∀k≥n.|uk−vk|<ε) : 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∈ℕ.∀p≥n.∀q≥n.|up−uq|<ε)
ou bien une version plus explicite qui impose un module de convergence
(du style
∀N∈ℕ.∀p≥N.∀q≥N.|up−uq|<2−N) :
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 P∨Q 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 à 2−n 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).