David Madore's WebLog: Introduction aux mathématiques constructives : 3. les nombres réels et leur ordre

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.|u_p−u_q|<ε) et quotiente par la relation qui identifie deux suites lorsque leur différence tend vers zéro (u∼v lorsque ∀ε>0.∃n∈ℕ.∀k≥n.|u_k−v_k|<ε) : 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.|u_p−u_q|<ε) ou bien une version plus explicite qui impose un module de convergence (du style ∀N∈ℕ.∀p≥N.∀q≥N.|u_p−u_q|<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 rendre 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⁻ⁿ 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).

Coupures de Dedekind

☞ Qu'est-ce qu'un réel ?

Qu'est-ce qu'un réel ? Classiquement, il y a deux approches pour les définir : les coupures de Dedekind ou les suites de Cauchy, qui donnent le même résultat. Constructivement, ce n'est plus le cas : on va pouvoir définir des réels de Dedekind et des réels de Cauchy (même deux sortes différentes de réels de Cauchy, si on veut) ; lorsqu'on dispose soit de la loi du tiers exclu (i.e., si on travaille en logique classique) soit de l'axiome du choix dénombrable, alors les réels de Dedekind et de Cauchy coïncident, mais en général (et donc dans le cadre dans lequel je me place ici) on ne peut pas l'affirmer. Les réels de Dedekind sont les plus généraux (les réels de Cauchy sont un sous-ensemble des réels de Dedekind, ce sont simplement ceux qui sont limites d'une suite de rationnels). Comme je l'ai dit dans l'avant-propos, il ne fait aucun doute dans mon esprit que les « bons » réels sont ceux de Dedekind (par exemple parce qu'ils correspondent à une notion de complétion raisonnable, ou parce que dans un topos spatial ils sont représentés par les fonctions réelles continues ; mais aussi simplement parce que les réels de Cauchy ne se comportent pas très bien, même vis-à-vis des suites). Bref, je vais définir les réels par les coupures de Dedekind, et je signale simplement que certains appellent ça les réels de Dedekind mais pour moi ce sont simplement les réels, quitte à dire plus loin un mot sur les réels de Cauchy.

Digression : Bon, il faut peut-être dire un mot du fait qu'il y a encore une autre sorte de réels, plus généraux que les réels de Dedekind, qui sont peut-être encore « meilleurs », ce sont les réels formels ; mais les réels formels ne sont pas un ensemble, ce sont une « locale », c'est-à-dire en gros un ensemble 𝒪(ℝ_form) d'« ouverts » qui se comportent comme les ouverts d'un espace topologique (en fait, un ensemble partiellement ordonné admettant des bornes supérieures quelconques et des bornes inférieures finies, et dans lequel les bornes inférieures finies se distribuent sur les bornes supérieures quelconques) mais sans qu'il ait d'ensemble sous-jacent. (L'ensemble 𝒪(ℝ_form) des ouverts des réels formels sont d'ailleurs assez faciles à définir : ce sont les réunions formelles d'intervalles ]p,q[ avec p<q∈ℚ sujettes aux relations sur l'intersection qu'on attend des intervalles rationnels c'est-à-dire ]p₁,q₁[ ∩ ]p₂,q₂[ = ]max(p₁,p₂),min(q₁,q₂)[ si max(p₁,p₂)<min(q₁,q₂) ou ∅ sinon, et aux relations sur la réunion que ]p₁,q₁[ ∪ ]p₂,q₂[ = ]p₁,q₂[ si p₁≤p₂<q₁≤q₂ et ⋃{]p′,q′[ : p<p′<q′<q} = ]p,q[ et ⋃{]p,q[ : p<q} = ℝ_form.) L('ensemble d)es réels de Dedekind, définis ci-dessous, sont alors précisément les « points » de la locale des réels formels, c'est-à-dire les applications ξ : 𝒪(ℝ_form) → Ω préservant les bornes supérieures quelconques et des bornes inférieures finies (donc concrètement, une application qui à deux rationnels p<q associe une valeur de vérité ξ(]p,q[) vérifiant les relations écrites dans la parenthèse de la phrase précédente ; le lien avec la définition qui va suivre est que la coupure (S,T) correspond à la fonction ξ qui associe à p<q la valeur de vérité de p∈S ∧ q∈T). Peut-être que c'est là la « bonne » façon de définir les réels de Dedekind, en fait (de dire que ℝ est la partie spatiale de la locale définie par 𝒪(ℝ_form)). Mais je vais quand même procéder de façon plus classique avec les coupures.

☞ Coupures de Dedekind

Un réel, donc, ou coupure de Dedekind est un couple (S,T) de parties de ℚ, où S est appelée la coupure inférieure et T la coupure supérieure (en fait, chacune des deux détermine l'autre, donc on pourrait formuler la définition avec une seule des deux, mais c'est moins symétrique), qui vérifient les cinq propriétés ci-dessous ; pour se faire une intuition sur ces propriétés, il faut imaginer que S sera l'ensemble des rationnels strictement plus petits que le réel qu'on définit et T l'ensemble des rationnels strictement plus grands ; on demande :

1. S et T sont habités : ∃r∈ℚ.(r∈S) et ∃r∈ℚ.(r∈T) ;
2. S est un ensemble inférieur (c'est-à-dire qu'il contient tout rationnel plus petit qu'un de ses éléments) et T est un ensemble supérieur (c'est-à-dire qu'il contient tout rationnel plus grand qu'un de ses éléments) : ∀r∈ℚ.∀r′∈ℚ.((r′<r ∧ r∈S) ⇒ r′∈S) et ∀r∈ℚ.∀r′∈ℚ.((r′>r ∧ r∈T) ⇒ r′∈T) ;
3. S est ouvert au sens où il contient un élément plus grand que n'importe quel élément donné, et T est ouvert au sens où il contient un un élément plus petit que n'importe quel élément donné : ∀r∈ℚ.(r∈S ⇒ ∃r′∈ℚ.(r′>r ∧ r′∈S)) et ∀r∈ℚ.(r∈T ⇒ ∃r′∈ℚ.(r′<r ∧ r′∈T)) ;
4. tout élément de S est strictement plus petit que tout élément de T : soit ∀s∈ℚ.∀t∈ℚ.((s∈S ∧ t∈T) ⇒ (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) ⇒ (s∈S ∨ t∈T)).

Il y a bien sûr toutes sortes de façon de reformuler ces conditions. Les conditions (b) et (c), par exemple, peuvent se formuler ensemble en disant qu'un rationnel est dans S si et seulement si il existe un rationnel strictement plus grand qui soit dans S, et symétriquement pour T. Grâce à (b) et (c) (et au fait que l'ordre sur les rationnels est total), la condition (d) peut se reformuler en disant simplement que S∩T=∅, ce qui est peut-être plus simple, mais j'aime la symétrie entre (d) et (e), ce qui explique mon choix rédactionnel.

La condition (e) est la plus significative (pas que les autres puissent être dispensée, mais il n'y a pas trop de doute sur ce qu'on veut à leur sujet, alors que (e) est plus sujette à débat), parce qu'elle permet de montrer une disjonction, quelque chose qui, constructivement, est fort : c'est cette propriété (e) qui va assurer la proposition (❀) plus bas (et, à travers elle, fait qu'on a un discernement sur les réels). On utilise souvent le terme de coupure localisée pour exprimer cette propriété (e) avec insistance.

On peut aussi s'intéresser à différents affaiblissements de ces conditions. Notamment la condition (e⁻) suivante, plus faible que (e), quoique classiquement équivalente : si s<t sont deux rationnels alors (¬(t∈T))⇒(s∈S) et (¬(s∈S))⇒(t∈T) (c'est-à-dire : tout rationnel plus petit qu'un rationnel qui n'est pas dans T est dans S, et tout rationnel plus grand qu'un rationnel qui n'est pas dans S est dans T ; ou avec des symboles : ∀s∈ℚ.∀t∈ℚ.((s<t ∧ ¬(t∈T)) ⇒ s∈S) et ∀s∈ℚ.∀t∈ℚ.((s<t ∧ ¬(s∈S)) ⇒ t∈T). Les coupures plus générales définies par les conditions (a), (b), (c), (d) et (e⁻) s'appellent les réels étendus bornés ou coupures de MacNeille. (Les coupures de Dedekind sont donc un cas particulier des coupures de MacNeille, c'est-à-dire que les réels sont un sous-ensemble des réels étendus bornés.) Je reviendrai plus bas sur les coupures de MacNeille et leurs propriétés, dans une section optionnelle qu'on sera invité à sauter si on ne veut pas se laisser distraire. (Par contre, je ne dirai rien sur les réels étendus généraux — aussi appelés réels classiques —, qui sont encore plus généraux que les réels étendus bornés, et qu'on obtient en affaiblissant aussi la propriété (a) pour juste dire que S et T ne sont pas vides.)

Si (S,T) est une coupure de Dedekind, d'après (d) et (e), l'ensemble T est l'ensemble des rationnels strictement plus grands qu'un rationnel qui n'est pas dans S, et l'ensemble S est l'ensemble des rationnels strictement plus petits qu'un rationnel qui n'est pas dans T (c'est essentiellement la conjonction de (d) et de la condition (e⁻) mentionnée en petits caractères ci-dessus). En particulier, ceci nous permet de dire que T est complètement déterminé par S, et que S est complètement déterminé par T : connaître une seule des deux composantes de la coupure permet de retrouver l'autre (et on peut tout à fait construire le réels avec uniquement, disons, l'ensemble S, c'est juste que la définition sera moins agréable et moins symétrique).

J'appelle ℝ l'ensemble des coupures de Dedekind, c'est-à-dire des couples (S,T) de parties de ℚ vérifiant (a)–(e). Il n'y a pas de quotient à faire ici : deux réels (S,T) et (S′,T′) sont égaux lorsque S=S′ et T=T′ (en fait, une seule de ces deux conditions suffit, puisque S et T se déterminent mutuellement comme je l'ai expliqué au paragraphe précédent).

Chaque rationnel r∈ℚ détermine une coupure ({s∈ℚ : s<r}, {t∈ℚ : t>r}) (il est à peu près trivial que c'est bien une coupure de Dedekind). Ceci détermine une injection ℚ→ℝ, et on identifie ℚ à son image dans ℝ, c'est-à-dire chaque r∈ℚ à la coupure qu'on vient de dire.

❇

☞ Un lemme sur les coupures entières

Le lemme technique suivant va s'avérer important pour la suite (on pourra notamment l'appliquer à (S∩ℤ, T∩ℤ) lorsque (S,T) est une coupure de Dedekind), et il est par ailleurs assez instructif dans l'utilisation des coupures (façon de dire que j'ai eu un mal de chien à trouver comment le rédiger proprement) :

Lemme sur les coupures entières : Soient M,N deux parties de ℤ vérifiant les propriétés suivantes :

1. M et N sont habités : ∃k∈ℤ.(k∈M) et ∃k∈ℤ.(k∈N) ;
2. M est un ensemble inférieur (c'est-à-dire qu'il contient tout rationnel plus petit qu'un de ses éléments) et N est un ensemble supérieur (c'est-à-dire qu'il contient tout rationnel plus grand qu'un de ses éléments) : ∀k∈ℤ.∀k′∈ℤ.((k′<k ∧ k∈M) ⇒ k′∈M) et ∀k∈ℤ.∀k′∈ℤ.((k′>k ∧ k∈N) ⇒ k′∈N) ;
3. ⊤ (i.e., il n'y a pas d'hypothèse (c), mais je garde quand même cet item pour le parallélisme avec les coupures de Dedekind) ;
4. tout élément de M est strictement plus petit que tout élément de N : soit ∀m∈ℤ.∀n∈ℤ.((m∈M ∧ n∈N) ⇒ (m<n)) ;
5. si un entier est strictement plus petit qu'un autre, alors soit le plus petit est dans M, soit le plus grand est dans N : soit ∀m∈ℤ.∀n∈ℤ.((m<n) ⇒ (m∈M ∨ n∈N)).

Alors il existe un k∈ℤ tel que tout entier m<k soit dans M et que tout entier n>k soit dans N.

Démonstration : Commençons par la remarque triviale que, dans la propriété (b), on peut remplacer l'ordre strict dans l'hypothèse par un ordre large (sur les entiers — comme d'ailleurs sur les rationnels — k′≤k est équivalent à k′<k ou bien k′=k et dans le second cas notre propriété est évidente).

Maintenant, on va démontrer par récurrence sur ℓ que s'il existe m∈M et n∈N avec n−m ≤ ℓ alors la conclusion souhaitée vaut. (Pour être parfaitement clair : les parties M,N étant fixées, on démontre par récurrence sur ℓ l'affirmation s'il existe m∈M et n∈N avec n−m ≤ ℓ, alors il existe un k∈ℤ tel que tout entier i<k soit dans M et que tout entier j>k soit dans N.)

Pour ℓ=0, l'affirmation est claire (s'il existe m∈M et n∈N avec n≤m, la propriété (d) montre une absurdité, et ex falso quodlibet).

Supposons donc notre affirmation connue pour un certain ℓ et prouvons-la pour ℓ+1. Supposons donc qu'on ait m∈M et n∈N avec n−m ≤ ℓ+1, et on veut montrer l'existence de k tel qu'expliqué. D'après la propriété (e), soit (m+1)∈M, soit (m+2)∈N. Dans le premier cas, comme (m+1)∈M et n∈N avec n−(m+1) ≤ ℓ, notre hypothèse de récurrence donne la conclusion voulue. Dans le second cas, k = m+1 convient pour la conclusion car d'une part m∈M donc tout élément <m+1 (c'est-à-dire ≤m) est dans M par la propriété (b) et d'autre part (m+2)∈N donc tout élément >m+1 (c'est-à-dire ≥m+2) est dans N aussi par la propriété (b). On a donc bien prouvé la conclusion voulue, et ceci conclut notre récurrence.

Bref, on a démontré que pour tout ℓ, s'il existe m∈M et n∈N avec n−m ≤ ℓ alors la conclusion souhaitée vaut. Comme il existe effectivement m∈M et n∈N (par la propriété (a)), on peut simplement poser ℓ = n−m et conclure. ∎

L'ordre sur les réels

☞ Deux propositions préalables

Pour introduire l'ordre sur les réels (i.e., les coupures de Dedekind), on va commencer par prouver deux propositions faciles, mais qui sont assez typiques de la manière dont on raisonne sur les coupures. La première servira à définir l'ordre large :

Proposition : Pour (S,T) et (S′,T′) deux coupures de Dedekind (ou même de MacNeille si on a lu ce que c'est), on a S⊆S′, si et seulement si T⊇T′.

Démonstration : Toute la situation étant symétrique, il suffit de prouver que S⊆S′ implique T⊇T′. En supposant S⊆S′, considérons r∈T′ : on veut montrer r∈T. D'après la propriété (c) de la coupure (S′,T′), il existe r′<r tel que r′∈T′. Maintenant, remarquons que r′∈S impliquerait r′∈S′ (par l'inclusion supposée), ce qui contredit r′∈T′ (propriété (d)) : on a donc prouvé ¬(r′∈S). D'après la propriété (e) de la coupure (S,T) (et ici, si on a lu ce que c'est, la version faible (e⁻) suffit), appliquée à r′<r, on en déduit r∈T, ce qu'on voulait. (Le raisonnement qu'on vient de tenir vaut pour les coupures de Dedekind mais aussi celles de MacNeille puisqu'on n'a utilisé que la version faible (e⁻).) ∎

La seconde servira à définir l'ordre strict et/ou la densité de ℚ dans ℝ :

Proposition : Pour (S,T) et (S′,T′) deux coupures de Dedekind, l'ensemble T∩S′ est habité si et seulement si il existe d>0 rationnel tel que S+d ⊆ S′, où S+d := {s+d : s∈S} = {s′∈ℚ : s′−d∈S} est le translaté de S par d. (De plus, si on a lu ce que c'est, le seulement si vaut même pour les coupures de MacNeille.)

Démonstration : Montrons d'abord que si T∩S′ est habité alors il existe d>0 rationnel tel que S+d ⊆ S′. Pour cela, soit r∈T∩S′. D'après la propriété (c) de la coupure (S′,T′), il existe r′>r qui est toujours dans S′, et d'après la propriété (b) de la coupure (S,T), il est bien sûr aussi toujours dans T. Posons d := r′−r qui est >0 puisque r′>r, et on va montrer S+d ⊆ S′. Si s∈S, alors on a s<r puisque r∈T (et par la propriété (d) de la coupure (S,T)), donc s+d < r+d = r′, et comme r′∈S′, par la propriété (b) de la coupure (S′,T′), on a s+d∈S′. On a donc bien montré S+d ⊆ S′. (Le raisonnement qu'on vient de tenir vaut pour les coupures de Dedekind mais aussi celles de MacNeille puisqu'on n'a pas utilisé la propriété (e).)

Montrons la réciproque. Supposons donc S+d ⊆ S′ pour un certain d>0 rationnel. Pour montrer que T∩S′ est habité, il suffit de prouver que T∩(S+d) l'est, et on peut maintenant oublier la coupure (S′,T′), et se contenter de prouver que, si (S,T) est une coupure de Dedekind et d>0 rationnel quelconque, alors T∩(S+d) est habité.

Soit M := {i∈ℤ : ½·i·d ∈ S} et N := {i∈ℤ : ½·i·d ∈ T}. Toutes les propriétés supposées dans le lemme sur les coupures entières (ci-dessus) sont vérifiées : la seule qui ne soit pas totalement évidente est (a), mais par la propriété parallèle (a) sur (S,T), on sait qu'il existe r∈S, et on peut trouver un entier tel que ½·i·d < r (par exemple en prenant i < 2r/d, ce qui ne pose pas de difficulté) auquel cas on a bien i∈M, et le cas de N est symétrique. Le lemme sur les coupures entières nous assure alors qu'il existe k tel que ½·i·d ∈ S si i<k et que ½·i·d ∈ T si i>k. En particulier, ½·(k−1)·d ∈ S et ½·(k+1)·d ∈ T. Mais ceci montre que ½·(k+1)·d est à la fois dans T est dans S+d, et achève la démonstration. ∎

Il faut aussi que je fasse quelque part la remarque à peu près triviale que si (S,T) est une coupure de Dedekind, alors (S+d, T+d) en est aussi une quel que soit le rationnel d.

☞ Définition des ordres large et strict

On définit deux relations binaires sur ℝ, 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 S⊆S′, ou, ce qui revient au même d'après ce qui a été dit, T⊇T′ ;
• on pose (S,T) < (S′,T′) (ou, de façon synonyme, (S′,T′) > (S,T)) lorsqu'il existe d>0 rationnel tel que S+d ⊆ S′, ou, ce qui revient au même d'après ce qui a été dit, lorsque T∩S′ est habité.

Comme on s'y attend, x<y se lit x est strictement inférieur à y (ou bien sûr : y est strictement supérieur à x) ; pour x≤y, on prendra garde à le lire x est inférieur au sens large à y (ou bien sûr : y est supérieur au sens large à x) et pas inférieur ou égal, car comme je vais l'expliquer plus bas, on ne peut pas affirmer que c'est la même chose (par contre, on pourra lire pas strictement supérieur pour la raison que je vais expliquer plus bas, ou bien au plus égal qui ne semble pas problématique). Pour z>0 et z≥0, on lira strictement positif et positif au sens large respectivement (je préfère éviter d'utiliser positif tout seul, ainsi que supérieur).

Si on s'intéresse aux coupures de MacNeille, la définition de l'ordre large est le même, mais pour l'ordre strict, les deux propriétés données cessent d'être équivalentes en général : on définira l'ordre strict (S,T) < (S′,T′) sur les coupures de MacNeille par ∃d∈ℚ.(d>0 ∧ S+d ⊆ S′) ; on peut aussi utiliser un symbole (S,T) ⊲ (S′,T′) pour dire que T∩S′ est habité, ce qui est plus fort, mais cette dernière relation d'ordre se comporte très mal. Je vais y revenir dans une section consacrée aux coupures de MacNeille plus loin. Pour l'instant, oublions-les.

Manifestement, ces relations généralisent les relations du même nom sur ℚ, donc il n'y a pas de conflit à utiliser les mêmes notations. La relation stricte ‘<’ implique la relation large ‘≤’. Il est facile de voir que les deux relations ‘<’ et ‘≤’ sont transitives ; ‘<’ est irréflexive (on n'a jamais x<x) et (donc) strictement antisymétrique (on n'a jamais simultanément x<y et y<x) tandis que ‘≤’ est réflexive (on a toujours x≤x) et antisymétrique au sens large c'est-à-dire que si x≤y et y≤x alors x=y. On a aussi la transitivité mixte : si x<y≤z, ou si x≤y<z, alors on a x<z.

De plus, si x=(S,T) est un réel, on voit qu'on a S = {s∈ℚ : s<x} (d'après les propriétés (b)&(c) des coupures) et T = {t∈ℚ : t>x} comme on s'y attend. On pourra d'ailleurs éventuellement noter x^← := {s∈ℚ : s<x} et x^→ := {t∈ℚ : t>x} pour les coupure gauche et droite définissant le réel x (si bien que x = (x^←, x^→)).

☞ Densité des rationnels

Les remarques ci-dessous sont très faciles, mais sont absolument essentielles, alors je vais les faire noir sur blanc :

Remarques : ℚ est dense dans ℝ au sens où si x<x′ sont des réels, il existe un rationnel r tel que x<r<x′ ; de plus, ℚ est cofinal dans ℝ au sens où si x est un réel, il existe des rationnels r et r′ tels que r<x<r′.

Démonstration : En se rappelant que pour un rationnel r et un réel x=(S,T) dire r<x signifie exactement r∈S et dire r>x signifie exactement r∈T, la première affirmation découle du fait qu'on a vu que x<x′ équivaut à T∩S′ habité, et la seconde est exactement la propriété (a) des coupures. ∎

⚠ Avertissement : Cette densité de ℚ dans ℝ me permettra notamment de dire, une fois définies l'addition et la valeur absolue sur les réels, que pour tout réel x et tout entier m il existe un rationnel r tel que |x−r| < 2^−m, une propriété dont on a l'habitude en maths classiques, et qui sert énormément. Classiquement, dire ça permet évidemment de construire une suite (r_m) de rationnels telle que |x−r_m| < 2^−m (et qui converge donc vers x) ; mais comme je travaille en maths constructives sans l'axiome du choix, on ne peut pas l'affirmer ici, faute de pouvoir choisir r_m pour chaque m. Je deviendrai sur ces difficultés quand je parlerai de réels de Cauchy (qui sont justement ceux qui sont limite d'une suite de rationnels, encore qu'il faudra distinguer selon que la limite est modulée).

❇

☞ Le rapport entre ordres strict et large

Classiquement, se donner un ordre strict sur un ensemble ou se donner un ordre large dessus est exactement équivalent, puisque chacun détermine l'autre de façon évidente. En maths constructives, les choses sont plus délicates, et je vais tâcher des les éclaircir. Mais disons tout de suite qu'il faut considérer, au moins sur les réels, que l'ordre strict est l'objet fondamental et que l'ordre large en dérive. En effet :

Proposition : Pour x et y deux réels, on a x≤y si et seulement si ¬(x>y). Autrement dit, ‘≤’ est la négation logique de ‘>’.

(Un moyen mnémotechnique peut être de se dire que les anglophones ont finalement raison d'utiliser le terme nonnegative, i.e., ¬(z<0) pour dire z≥0.) Ce n'est pas difficile à démontrer :

Démonstration de l'équivalence entre x≤y et ¬(x>y) pour x,y deux réels :

Mettons x=(S,T) et y=(U,V) (les deux coupures de Dedekind définissant les réels considérés).

Dans un premier temps, supposons x≤y et on veut montrer ¬(x>y). Autrement dit, on suppose S⊆U, et on veut prouver que S∩V n'est pas habité (i.e., est vide). Supposons donc r ∈ S∩V, et on veut aboutir à une absurdité. Mais comme S⊆U, on a r ∈ U∩V, ce qui est absurde car U et V sont disjoints.

Réciproquement, supposons ¬(x>y), et on veut prouver x≤y. Autrement dit, on suppose S∩V = ∅, et on veut prouver S⊆U. Soit r∈S : on veut montrer r∈U. D'après la propriété (c) de la coupure (S,T), on peut trouver r′>r avec r′∈S. Comme S∩V = ∅, on a ¬(r′∈V). Comme r<r′, d'après la propriété (e) de la coupure (U,V), on a soit r∈U soit r′∈V ; or on vient d'exclure le second : c'est donc que r∈U comme annoncé. ∎

Corollaire : Pour x et y deux réels, x=y est la négation de x<y ou bien x>y (ce qu'on notera plus bas comme x⋕y). ❧ Par conséquent, ¬¬(x=y) équivaut à x=y : on rappelle que ceci exprime le fait que l'ensemble des réels est (¬¬)-séparé ; et de même, ¬¬(x≤y) équivaut à x≤y. ❧ Notamment, si x et y sont deux réels et p une affirmation quelconque, et si on suppose que p implique x=y et que ¬p implique aussi x=y, alors on a x=y inconditionnellement (et la même chose vaut en remplaçant x=y par x≤y).

Démonstration : Pour ce qui est de la première affirmation, x=y équivaut à x≥y ∧ x≤y, qui équivaut à ¬(x<y) ∧ ¬(x>y), qui équivaut à ¬(x<y ∨ x>y) par pure logique.

Pour ce qui est de la seconde affirmation, on rappelle que par pure logique, ¬¬¬r équivaut à ¬r : en appliquant ceci à l'affirmation x<y ∨ x>y pour r, ce qui vient d'être dit montre que ¬¬(x=y) équivaut à x=y.

Pour ce qui est de la troisième affirmation, on l'a déjà expliquée dans le premier billet de cette série (pour un ensemble (¬¬)-séparé), mais je rappelle l'argument : par pure logique, si p⇒q et ¬p⇒q, on peut conclure (p∨¬p) ⇒ q, donc ¬¬(p∨¬p) ⇒ ¬¬q par pure logique, donc en fait ¬¬q (car ¬¬(p∨¬p) est valable). Et on applique ça ici à q valant x=y (ou bien x≤y) pour lequel on vient de voir que ¬¬q entraîne q. ∎

Bref, pour prouver x≤y, même en maths constructives, on peut supposer x>y et chercher à arriver à une absurdité ; et pour prouver x=y on peut chercher à arriver à une absurdité depuis x<y ou x>y.

⚠ En revanche, je n'affirme pas que x≤y équivaille à x<y ∨ x=y, ni non plus que x<y équivaille à x≤y ∧ ¬(x=y) ou à ¬(x≥y) (ces deux dernières sont équivalents et on va noter ça x⋖y ci-dessous).

Digression : La faillite de ces équivalences classiquement évidentes est sans doute une des choses les plus déstabilisantes des maths constructives. Non seulement c'est déstabilisant, mais il peut aussi être difficile à mémoriser ce qu'on a le droit d'affirmer et ce qu'on n'a pas le droit d'affirmer sur les réels constructifs. On peut se dire que x<y signifie que je sais trouver un rationnel entre les deux (cf. plus bas ; c'est donc une relation très forte), mais je ne sais pas si ça aide tant que ça à comprendre que x≤y équivaut à ¬(x>y) comme je vais le dire ci-dessous. Une autre façon de retenir ce qui est marche peut être de penser aux fonctions réelles continues sur un espace topologique. C'est pour ça que je me permets de digresser pour évoquer rapidement l'interprétation des réels constructifs comme des fonctions continues sur un espace topologique (ici juste comme moyen mnémotechnique ou pour aider l'intuition : une explication plus correcte devrait faire l'objet d'un billet de blog séparé sur les topos de faisceaux). Bref, imaginez que x,y soient non pas des réels (constructifs) mais des fonctions continues à valeurs réelles (en maths classiques pour simplifier) sur un espace topologique X (on peut imaginer X=ℝ ici si on veut) ; et imaginez que x<y et x<y désignent les relations habituellement désignées par ces symboles entre les fonctions en question, mais surtout que la valeur de vérité de ces choses est le plus grand ouvert sur lequel l'inégalité vaut (i.e., l'intérieur de l'ensemble des points où l'inégalité vaut), le ou logique et le et logique s'interprétant comme réunion et intersection des ouverts correspondants, et le non logique s'interprétant comme le plus grand ouvert disjoint (i.e., classiquement, le complémentaire de l'adhérence). Il est alors clair que x≤y (comprendre : le plus grand ouvert sur lequel x(ξ)≤y(ξ)) n'est en général pas pareil que x<y ∨ x=y (comprendre : la réunion de l'ouvert sur lequel x(ξ)<y(ξ) et du plus grand ouvert sur lequel x(ξ)=y(ξ)), et que x<y (comprendre : l'ouvert sur lequel x(ξ)<y(ξ)) n'est en général pas pareil que ¬(x≥y) (comprendre : le plus grand ouvert disjoint du plus grand ouvert sur lequel x(ξ)≥y(ξ)) ; par exemple, si z est la fonction valeur absolue sur ℝ, elle vérifie ¬(0≥z) car le plus grand ouvert sur lequel elle est négative est vide, mais elle ne vérifie pas 0<z. En revanche, l'équivalence entre x≤y et ¬(x>y) va bien fonctionner, car les deux se comprennent comme le plus grand ouvert sur lequel on n'a pas x(ξ)>y(ξ).

☞ Une proposition cruciale sur la localisation des réels

⚠ J'insiste sur le fait qu'on ne peut pas affirmer que pour deux réels x,y on ait soit x<y soit x=y soit x>y (la trichotomie classique) ; on ne peut même pas affirmer qu'on ait soit x≤y soit x≥y (la dichotomie classique) ; ces affirmations vont s'appeler LPO analytique et LLPO analytique plus loin. Cela peut sembler tellement rédhibitoire de ne pas disposer d'un ordre total sur les réels qu'on peut se dire qu'il est désespéré de faire de l'analyse dans ces conditions. Voici cependant un résultat qui permet souvent d'en tenir lieu, et qui va énormément servir dans les raisonnements sur les réels de Dedekind, en gros dès qu'on veut produire une disjonction :

Proposition (❀) : Si x<x′ et y sont des réels, on a soit x<y soit y<x′ (autrement dit, donnés un réel strictement plus petit qu'un autre, n'importe quel troisième réel est soit strictement plus grand que le plus petit des deux, soit strictement plus petit que le plus grand des deux ; le soit … soit est, bien sûr, ici, un « ou inclusif ») : ∀x∈ℝ.∀x′∈ℝ.∀y∈ℝ.((x<x′) ⇒ (x<y ∨ y<x′)).

Ou, si on préfère : si x<x′, alors ℝ est la réunion de la demi-droite ]x,→[ := {y∈ℝ : x<y} et de la demi-droite ]←,x′[ := {y∈ℝ : y<x′}.

Démonstration : Mettons x=(S,T) et x′=(S′,T′) et y=(U,V) (les trois coupures de Dedekind définissant les réels considérés). L'hypothèse x<x′ se traduit par le fait que T∩S′ est habité. Soit donc r ∈ T∩S′. D'après la propriété (c) de la coupure (S′,T′), on peut trouver r′>r avec r′∈S′, et d'après la propriété (b) de (S,T) on a encore r′∈T, bref r′ ∈ T∩S′. Comme r<r′, d'après la propriété (e) de la coupure (U,V), on a soit r∈U soit r′∈V. Dans le premier cas, r ∈ T∩U, donc T∩U est habité, c'est-à-dire x<y ; dans le second cas, r′ ∈ S′∩V, donc S′∩V est habité, c'est-à-dire y<x′. ∎

(C'est l'échec de cette propriété fondamentale qui rend les coupures de MacNeille presque inutilisables.)

Comme je l'ai dit plus haut, cette proposition va être cruciale pour produire des disjonctions (chose qui est, en maths constructives, généralement difficile). Il faut néanmoins prendre garde au fait que la disjonction qu'elle produit n'est jamais exclusive, et c'est ce qui va faire qu'on aura souvent envie de pouvoir faire appel à l'axiome du choix dénombrable dans le contexte de l'utilisation de cette proposition (dès qu'on veut l'invoquer sur une suite de quelque chose) : ça va revenir nous embêter plus loin.

❇

☞ Encore une relation d'ordre !

Comme on a vu plus haut que x≤y équivaut à ¬(x>y), on peut aussi vouloir s'intéresser à la négation de ‘≥’ : on note parfois x⋖y (ou, bien sûr, y⋗x) pour ¬(x≥y). Cette relation x⋖y équivaut à x≤y ∧ ¬(x=y). (Démonstration : comme x>y implique x≥y, on voit que ¬(x≥y) implique ¬(x>y), c'est-à-dire que x⋖y implique x≤y, et il est par ailleurs évident qu'il implique ¬(x=y) ; réciproquement, comme x≤y et x≥y entraînent x=y, c'est que x≤y et ¬(x=y) entraînent ¬(x≥y), c'est-à-dire x⋖y, comme on le voulait. ∎) La relation x⋖y peut par exemple se lire en disant que x est presque strictement inférieur à y (ou sinon inférieur mais pas égal). Il est clair d'après ce que je viens de dire que ‘⋖’ est irréflexive et transitive. La négation de ‘⋖’ est simplement ‘≥’ car trois négations valent une.

La structure de treillis sur ℝ

☞ Construction des bornes inf et sup binaires

Comme je l'ai dit plus haut, on ne peut pas affirmer qu'on ait soit x≤y soit x≥y. Là aussi, ça peut sembler rédhibitoire : dans ces conditions, comment va-t-on pouvoir définir ne serait-ce que la valeur absolue ? Ce qui va nous sauver est la structure de treillis : il est extrêmement important de savoir que deux réels x,y ont toujours une borne inférieure et une borne supérieure, qu'on notera x⊓y et x⊔y respectivement :

Proposition : Si x,y sont deux réels, disons x=(S,T) et y=(U,V), alors (S∪U, T∩V) est un nombre réel z : ce z est la borne supérieure de x et y au sens où pour tout réel t on a t≥z si et seulement si t≥x et t≥y (et ceci caractérise z) ; on notera z = x⊔y. Le cas de la borne inférieure, notée x⊓y, se traite de façon analogue, et c'est (S∩U, T∪V).

Démonstration : La vérification des propriétés (a)–(e) pour (S∪U, T∩V) est facile. (Par exemple, pour vérifier que T∩V est habité, on utilise le fait que T et V le sont, et on prend le plus grand des deux rationnels exhibant ces faits, qui sera à la fois dans T et V d'après la propriété (b). Pour la propriété (e), si s<t sont rationnels, on remarquera qu'on passe par une distinction des cas s∈S ou t∈T et des cas s∈U ou t∈V pour obtenir t ∈ T∩V dans un cas et s ∈ S∪U dans tous les autres.)

Dire qu'un réel est supérieur au sens large à x et à y signifie que sa coupure inférieure contient S et U respectivement, ce qui revient exactement à dire qu'elle contient S∪U, ce qui revient à dire qu'il est supérieur au sens large à z := (S∪U, T∩V) : ceci montre que ce z est bien la borne supérieure de {x,y}. (Et l'unicité de la borne supérieure découle du fait que si z et z′ vérifient tous les deux la même propriété, on a z≥z′ car z≥x et z≥y et de même z≤z′, donc z=z′.) ∎

L'idée est que x⊓y et x⊔y vont pouvoir servir dans plein d'endroits où, classiquement, on utiliserait min(x,y) et max(x,y).

⚠ Avertissement : Il y a des gens qui notent carrément min(x,y) et max(x,y) ce que j'ai noté x⊓y et x⊔y respectivement (on trouve ça par exemple dans le livre Homotopy Type Theory — que je déconseille très vivement au passage). Cette notation est une erreur : en effet, le maximum d'un ensemble S est (par définition, classiquement comme constructivement) un élément appartenant à S qui est supérieur au sens large à tout élément de S ; l'existence de max{x,y} est donc équivalente à x≤y ∨ x≥y (selon que ce maximum vaut y ou x). La raison pour laquelle les gens insistent pour utiliser cette notation pourtant erronée est que Bishop l'a utilisée (parce que Bishop poursuivait le but de rendre les maths constructives aussi semblables que possible aux maths classiques). Ou alors ils ergotent sur le fait qu'ils notent max(x,y) et pas max{x,y} (dans ce cas ce n'est pas une erreur c'est juste une notation épouvantablement pourrie). On peut en revanche parler de max(r,s) pour deux rationnels, ou pour deux réels qui s'avèrent être comparables pour l'ordre large, mais en général c'est une erreur de l'écrire. On peut cependant valablement noter inf(x,y) et sup(x,y) pour x⊓y et x⊔y si on veut (ce n'est pas un problème, et on va voir plus bas qu'ils sont bien un inf et un sup au sens fort).

☞ Bornes inf et sup binaires et inégalités strictes

Le fait suivant, qui permet de contrôler les inégalités strictes, s'avérera utile dans la suite (notamment pour voir que la borne supérieure qu'on a définie n'est pas juste une borne supérieure mais un supremum (fort)) :

Proposition : Pour x,y,z trois réels, on a : ① x⊔y < z si et seulement si x<z et y<z ; et par ailleurs : ② z < x⊔y si et seulement si z<x ou bien z<y.

Démonstration : Pour alléger les notations, on notera t^← resp. t^→ les coupure gauche {r∈ℚ : r<t} resp. droite {r∈ℚ : r>t} définissant le réel t. Montrons le ① : dire que x⊔y < z signifie que (x⊔y)^→ ∩ z^← est habité, c'est-à-dire, par construction de ‘⊔’, que x^→ ∩ y^→ ∩ z^← est habité. Ceci entraîne manifestement que x^→ ∩ z^← et y^→ ∩ z^← sont habités, c'est-à-dire x<z et y<z. Dans l'autre sens, si x<z et y<z, c'est-à-dire que x^→ ∩ z^← et y^→ ∩ z^← sont habités, disons que r ∈ x^→ ∩ z^← et s ∈ y^→ ∩ z^←, considérons max(r,s) : il est dans z^← car il est égal à l'un de r ou s et que les deux sont dans z^←, et il est dans x^→ car il est supérieur au sens large à r qui est dedans, et de même il est dans y^→ : bref, max(r,s) est dans x^→ ∩ y^→ ∩ z^←, c'est-à-dire x⊔y < z.

Montrons le ② : dire z < x⊔y signifie que z^→ ∩ (x⊔y)^← est habité, c'est-à-dire, par construction de ‘⊔’, que z^→ ∩ (x^← ∪ y^←) est habité, qui n'est autre que (z^→ ∩ x^←) ∪ (z^→ ∩ y^←) ; or une union est habitée si et seulement si l'un des termes de l'union l'est, c'est donc équivalent à dire que z^→ ∩ x^← ou bien z^→ ∩ y^← est habité, ce qui équivaut à z<x ou bien z<y. ∎

Dualement, bien sûr, on a x⊓y < z si et seulement si x<z ou bien y<z, et z < x⊓y si et seulement si z<x et z<y.

En passant à la négation du ② de la proposition ci-dessus, on retrouve le fait que x⊔y ≤ z si et seulement si x≤z et y≤z, (et dualement z ≤ x⊓y si et seulement si z≤x et z≤y). En revanche, la négation du ① ne donne pas grand-chose d'intéressant : z ≤ x⊔y vaut si et seulement si x<z et y<z ne sont pas tous les deux vrais ; mais on ne peut pas affirmer que cela équivaille à z≤x ou bien z≤y (cette équivalence sera une formulation possible du principe LLPO analytique plus bas).

[Optionnel] Les coupures de MacNeille et leurs ordres

☡ Guide de lecture : Hic sunt dracones ! Cette section est moralement en petits caractères (je ne la mets pas en petits caractères parce que c'est déplaisant d'avoir des passages trop longs en petits caractères, surtout que j'aurai envie de mettre des passages en encore plus petits caractères, mais considérez que c'est comme si). Elle n'est là que pour les gens qui veulent en savoir plus sur les coupures de MacNeille, également appelées réels étendus bornés. Il est recommandé de la sauter si on ne trouve pas cette idée fascinante : en tout cas, sa lecture n'est pas nécessaire pour la compréhension de la suite de ce billet.

☞ Retour sur les coupures de MacNeille

Je rappelle que les coupures de MacNeille (ou réels étendus bornés) sont définies en remplaçant la propriété (e) (∀s∈ℚ.∀t∈ℚ.((s<t) ⇒ (s∈S ∨ t∈T))) qui définissait les réels (= coupures de Dedekind) par la propriété (e⁻) plus faible suivante : ∀s∈ℚ.∀t∈ℚ.((s<t ∧ ¬(t∈T)) ⇒ s∈S) et ∀s∈ℚ.∀t∈ℚ.((s<t ∧ ¬(s∈S)) ⇒ t∈T), les autres propriétés (a)–(d) restant inchangées. Je noterai ℝ_MN l'ensemble des coupures de MacNeille.

Digression : Si on a une idée de ce que sont les topos de faisceaux, ou même si on veut simplement se faire une intuition de ce dont il s'agit, je précise que tandis que les réels de Dedekind sont représentés par les fonctions réelles continues sur un espace topologique, les coupures de MacNeille sont représentées par fonctions semicontinues normales, ou plus précisément les couples (f_♭, f_♯) de fonctions réelles telles que f_♭(x) = lim.inf_x(f_♯) et f_♯(x) = lim.sup_x(f_♭), où lim.inf_x(g) désigne sup_V∋x(inf_y∈V(g(y))), le sup étant pris sur les voisinages V de x et l'inf sur les éléments de ce voisinage — et symétriquement lim.sup_x(g) = inf_V∋x(sup_y∈V(g(y))) — si bien que chacune de f_♭ et f_♯ détermine l'autre, et on les appelle fonction semicontinue inférieurement normale et fonction semicontinue supérieurement normale. Voir ici si vous voulez plus d'explications à ce sujet.

☞ Ordres fort, strict et large

Sur les coupures de MacNeille, on a trois relations d'ordre assez naturelles à définir (je prends le soin de l'écrire, parce que ça m'a causé énormément de confusion et que l'Elephant de Johnstone est complètement bidonné sur le sujet) :

• on pose (S,T) ⊲ (S′,T′) (ou, de façon synonyme, (S′,T′) ⊳ (S,T)) lorsque T∩S′ est habité ;
• on pose (S,T) < (S′,T′) (ou, de façon synonyme, (S′,T′) > (S,T)) lorsqu'il existe d>0 rationnel tel que (S+d) ⊆ S′ (ou, ce qui revient au même, (T+d)⊇T), où S+d := {s+d : s∈S} = {s′∈ℚ : s′−d∈S} est le translaté de S par d ;
• on pose (S,T) ≤ (S′,T′) (ou, de façon synonyme, (S′,T′) ≥ (S,T)) lorsque S⊆S′ ou, ce qui revient au même, T⊇T.

Je vais les appeler respectivement l'ordre fort, l'ordre strict et l'ordre large sur les coupures de MacNeille. (Sur les coupures de Dedekind, les deux premiers sont équivalents, comme on l'a vu ; mais pour les coupures de MacNeille, c'est quand même ‘<’ qui est le moins désagréable à utiliser.)

Proposition : (S,T) ⊲ (S′,T′) implique (S,T) < (S′,T′) qui à son tour implique la négation de (S,T) ≥ (S′,T′), qui implique (S,T) ≤ (S′,T′). Par ailleurs, (S,T) ≥ (S′,T′) équivaut à la négation de (S,T) ⊲ (S′,T′) et aussi à la négation de (S,T) < (S′,T′).

Démonstration : On a déjà prouvé que (S,T) ⊲ (S′,T′) implique (S,T) < (S′,T′) : j'ai fait attention, dans la preuve que j'en ai donnée sur les réels de Dedekind, à ce qu'elle vaille encore pour les coupures de MacNeille.

Le fait que (S,T) < (S′,T′) contredit (S,T) ≥ (S′,T′) se voit ainsi : le premier signifie qu'il existe d>0 rationnel tel que (S+d) ⊆ S′, et le second signifie S′⊆S : on aurait donc (S+d) ⊆ S, et il s'agit de voir que ceci conduit à une absurdité. Or si r∈S (qui existe par la propriété (a)), ceci nous donnerait, par une récurrence immédiate, r + i·d ∈ S pour tout i∈ℕ : mais en prenant r′∈T (toujours par (a)) et i tel que r + i·d > r′ (il suffit pour ça de prendre un entier i > (r′−r)/d), on contredit la propriété (d).

Montrons maintenant que la négation de (S,T) ⊲ (S′,T′), c'est-à-dire T∩S′=∅, implique (S,T) ≥ (S′,T′), c'est-à-dire S′⊆S. Soit donc r∈S′. D'après la propriété (c) de la coupure (S′,T′), il existe r′>r qui est aussi dans S′, et comme T∩S′=∅, on a ¬(r′∈T). D'après la propriété (e⁻) de la coupure (S,T) appliquée à r<r′, on en déduit r∈S, comme on voulait.

On vient de voir que (⊲) ⇒ (<) ⇒ ¬(≥) (ce qui donne aussi, du coup, ¬¬(≥) ⇒ ¬(<) ⇒ ¬(⊲)) et que ¬(⊲) ⇒ (≥), et bien sûr on a (≥) ⇒ ¬¬(≥) : donc ¬¬(≥) ⇔ ¬(<) ⇔ ¬(⊲) ⇔ (≥). Enfin, comme (>) ⇒ (≥) est clair, on a ¬(≥) ⇒ ¬(>) ⇔ (≤). On a bien montré tout ce qui était affirmé. ∎

Il est facile de voir que les trois relations ‘⊲’, ‘<’ et ‘≤’ sont transitives ; ‘⊲’ et ‘<’ sont irréflexives et (donc) strictement antisymétrique, tandis que ‘≤’ est réflexive et antisymétrique au sens large. On a aussi diverses transitivités mixtes : si x<y≤z, ou si x≤y<z, alors on a x<z ; et si x⊲y≤z, ou si x≤y⊲z, alors on a x⊲z.

Comme pour les réels de Dedekind, et avec exactement la même preuve, on a :

Corollaire : Pour x et y deux coupures de MacNeille, x=y est la négation de x<y ou bien x>y. ❧ Par conséquent, ¬¬(x=y) équivaut à x=y : on rappelle que ceci exprime le fait que l'ensemble ℝ_MN des coupures de MacNeille est (¬¬)-séparé ; et de même, ¬¬(x≤y) équivaut à x≤y. ❧ Notamment, si x et y sont deux coupures de MacNeille et p une affirmation quelconque, et si on suppose que p implique x=y et que ¬p implique x=y, alors on a x=y inconditionnellement (et la même chose vaut en remplaçant x=y par x≤y).

On a des inclusions ℚ ⊆ ℝ ⊆ ℝ_MN en notant ℝ_MN l'ensemble des coupures de MacNeille, et les ordres ‘⊲’ et ‘<’ coïncident sur ℝ. Mieux : ils coïncident dès que l'un des deux éléments comparés est dans ℝ :

Proposition : Si (S,T) et (S′,T′) sont deux coupures de MacNeille dont au moins une est une coupure de Dedekind, alors (S,T) < (S′,T′) implique (S,T) ⊲ (S′,T′).

Démonstration : La situation étant symétrique (une fois faite la vérification facile que la définition de ‘<’ peut bien s'exprimer de façon symétrique !), mettons que (S,T) soit de Dedekind. Notre hypothèse est donc que S+d ⊆ S′ pour un certain rationnel d>0, et on veut prouver que T∩S′ est habité. Mais cela découle du fait que T∩(S+d) est habité, qui a déjà été prouvé (dans l'équivalence entre ‘⊲’ et ‘<’ pour les coupures de Dedekind), ou, si on ne veut pas faire référence à une preuve, on peut observer que (S+d, T+d) est une coupure de Dedekind, donc l'inégalité (S,T) ⊲ (S+d, T+d) découle de (S,T) < (S+d, T+d) entre deux coupures de Dedekind. ∎

Il résulte notamment de ce que j'ai dit que si x=(S,T) est une coupure de MacNeille alors, comme pour les coupures de Dedekind, S = x^← := {r∈ℚ : r<x} et T = x^→ := {r∈ℚ : r>x} (puisque c'est à peu près évident pour l'ordre fort, et qu'on vient de dire qu'ils coïncident dès qu'un des nombres comparés est rationnel).

Comme pour les coupures de Dedekind, ℚ est dense dans les coupures de MacNeille pour l'ordre fort, c'est-à-dire que si x⊲x′ sont des coupures de MacNeille, il existe un rationnel r tel que x⊲r⊲x′ ; de plus, ℚ est cofinal au sens où si x est une coupure de MacNeille, il existe des rationnels r et r′ tels que r⊲x⊲r′. (Ces faits sont à peu près évidents, comme pour le cas de Dedekind.) Mais en fait, on peut remarquer que l'existence d'un rationnel r tel que x<r<x′ (ou meme d'un réel de Dedekind), équivaut à x⊲x′ (puisqu'on a r⊲x⊲r′ d'après la proposition précédente), ce qui explique peut-être un peu mieux le sens de l'ordre fort : il faut penser à x⊲x′ comme signifiant il existe un rationnel/réel entre les deux. Et comme je vais le dire plus bas, l'ordre fort est tellement mauvais qu'il est quasiment inutilisable (on ne peut même pas affirmer que x⊲(x+1) vaut en général, ce qui est quand même assez désastreux).

☞ Les bornes inf et sup pour les coupures de MacNeille

Un des rares points sur lesquels les coupures de MacNeille sont meilleures que les coupures de Dedekind, c'est pour l'existence de bornes supérieures, qui vont fonctionner en gros comme les réels en maths classiques (mais attention, il s'agit de bornes supérieures (faibles), c'est-à-dire les plus petits majorants, pas de suprema forts que je vais définir plus bas) :

Proposition : Si (x_i)_i∈I = (S_i,T_i)_i∈I est une famille de coupures de MacNeille qui est habitée (c'est-à-dire que l'ensemble I d'indices est habité) et majorée (c'est-à-dire qu'il existe une coupure de MacNeille, qu'on peut supposer rationnelle, qui majore tous les x_i), alors elle a une borne supérieure, c'est-à-dire que l'ensemble des majorants larges communs des x_i a un plus petit élément z. De plus, si I est fini, la coupure droite z^→ de z est l'intersection ⋂_i∈I T_i des coupures droites dont on est parti (et sans supposer I fini, ce sera l'ensemble int^→(⋂_i∈I T_i) qui va être défini dans la démonstration qui suit).

Démonstration : Remarquons pour commencer qu'une coupure de MacNeille (X,Y) majore au sens large tous les (S_i,T_i), si et seulement si Y ⊆ T_i pour chaque i, c'est-à-dire Y⊆E où on a posé E := ⋂_i∈I T_i.

Cette intersection E vérifie certaines propriétés d'une coupure droite. D'abord, E est habité : en effet, en considérant un majorant large commun aux x_i (qu'on a supposé exister), et quitte à le remplacer par un rationnel strictement plus grand, on a trouvé un élément dans tous les T_i. Ensuite, il existe un rationnel qui n'est pas dans E : n'importe quel élément d'un des S_i fera l'affaire (mais on notera que c'est ici qu'on utilise le fait que I est habité !). Enfin, nous allons montrer que E vérifie le renforcement (b⁺) suivant de (b) : ∀r∈ℚ.∀r′∈ℚ.((r′>r ∧ ¬¬(r∈E)) ⇒ r′∈E). En effet, si r′>r et que ¬¬(r∈E), prenons r″ tel que r<r″<r′ : pour chaque i∈I, on a ¬¬(r∈T_i), donc r″∈S_i est impossible (car par la propriété (d) cela entraînerait ¬(r∈T_i), une contradiction), c'est-à-dire ¬(r″∈S_i), mais par (e⁻) on en déduit r′∈T_i, et comme ceci est pour n'importe quel i, on a bien r′∈E.

Appelons maintenant V l'ensemble int^→(E) := {r∈ℚ : ∃r′∈ℚ.(r′<r ∧ r′∈E)}. Par la propriété (b) de E (ou a fortiori (b⁺) que nous venons de prouver), on a V⊆E. L'ensemble V est habité (il suffit de prendre r′ dans E et un r>r′ quelconque sera dans V), et il existe un rationnel qui n'y appartient pas (puisque V⊆E et qu'il existe un rationnel qui n'est pas dans E). De plus, V vérifie lui aussi la propriété (b⁺) du paragraphe précédent : en effet, si on suppose r′>r et ¬¬(r∈V), alors ¬¬(r∈E) par l'inclusion V⊆E, donc en prenant r″ tel que r<r″<r′, on a r″∈E par la propriété (b⁺) de E, et ceci montre bien r′∈V. Enfin, V vérifie la propriété (c) droite, à savoir ∀r∈ℚ.(r∈V ⇒ ∃r′∈ℚ.(r′<r ∧ r′∈V)) (puisque la définition de V assure que si r∈V il existe r″<r qui est dans E, et en prenant r′ tel que r″<r′<r on a bien r′∈V).

Oublions temporairement tout de V⊆ℚ à part qu'il vérifie les trois propriétés (a) ∃r∈ℚ.(r∈V) et ∃r∈ℚ.(¬(r∈V)), (b⁺) ∀r∈ℚ.∀r′∈ℚ.((r′>r ∧ ¬¬(r∈V)) ⇒ r′∈V), et (c) ∀r∈ℚ.(r∈V ⇒ ∃r′∈ℚ.(r′<r ∧ r′∈V)) qu'on a démontrées au paragraphe précédent, et appelons U := int^←(ℚ∖V) := {r∈ℚ : ∃r′∈ℚ.(r′>r ∧ ¬(r′∈V))}. On va vérifier que (U,V) est une coupure de MacNeille. Mais on a déjà ce qui concerne V des propriétés (a), (b) et (c) de (U,V), et les mêmes raisonnements qu'au paragraphe précédent (en remplaçant E par ℚ∖V et V par U et en changeant le sens de toutes les inégalités ; on remarque au passage que U ⊆ (ℚ∖V)) montrent aussi ce qui concerne U des propriétés (a), (b) et (c). La propriété (d) de (U,V) se vérifie ainsi : si u∈U et v∈V, il existe r′∈ℚ tel que r′>u et ¬(r′∈V) par définition de U, mais alors v<r′ aboutirait à une contradiction (car v∈V et que V vérifie (b)), c'est donc que v≥r′ donc u<v comme souhaité. Enfin montrons (e⁻) : d'une part, si u<v et que ¬(v∈V) alors on a u∈U par définition même de U ; et d'autre part, si ¬(u∈U) alors ¬¬(u∈V) car U ⊆ (ℚ∖V), et par la propriété (b⁺) de V on a v∈V.

On a donc montré que (U,V) était une coupure de MacNeille. Elle majore au sens large tous les (S_i,T_i), car V⊆E (première remarque de la présente démonstration). Et inversement, si (X,Y) est une coupure de MacNeille qui majore au sens large tous les (S_i,T_i), on a Y⊆E (même remarque), d'où on déduit Y ⊆ int^→(E) = V par la propriété (c) de la coupure (X,Y) : ainsi, (X,Y) est majorée par (U,V). On a bien montré que (U,V) est le plus petit majorant large des (S_i,T_i).

Enfin, si I est fini, disons I, on veut montrer que V=E, c'est-à-dire que ∀r∈E.∃r′∈ℚ.(r′<r ∧ r′∈E), c'est-à-dire juste la propriété (c) sur E. Pour ça, on applique la propriété (c) des coupures (S_i,T_i) pour trouver un r_i<r dans chaque T_i, et si r′ est leur maximum (qui a bien un sens car on a affaire à un ensemble fini de rationnels), on a r′<r, et r′ est dans chacun des T_i car il est ≥r_i (et par la propriété (b)). ∎

Bien sûr, exactement les mêmes choses valent pour les bornes inférieures : on en fabrique la coupure gauche en prenant l'intersection ⋂_i∈I S_i des coupures gauches dont on est partis, si l'ensemble d'indice I est (habité ! et) fini, et plus généralement int^←(⋂_i∈I S_i).

On remarque qu'il résulte de la proposition que, si x,y sont deux réels de Dedekind, alors x⊔y (et bien sûr symétriquement x⊓y) a le même sens en tant que coupure de MacNeille qu'en tant que réel de Dedekind, car ils ont la même coupure droite (obtenue en prenant l'intersection des coupures droites de x et y), et que la coupure droite détermine complètement la coupure gauche. Néanmoins, la formule pour la coupure gauche de x⊔y donnée pour les réels de Dedekind n'a pas de raison de valoir encore pour les coupures de MacNeille !

En fait, si je regarde ce qui s'est passé pour le cas binaire, disons si x=(S,T) et y=(U,V) sont deux coupures de MacNeille, pour définir x⊔y, on prend comme coupure droite l'ensemble T∩V comme pour les réels (= coupures de Dedekind), mais pour coupure gauche, selon la démonstration qui vient d'être faite, il faut la reconstruire à partir de la coupure droite, c'est-à-dire que c'est l'ensemble des rationnels strictement plus petit qu'un rationnel qui n'est pas dans T∩V : autrement dit, x⊔y = (X, T∩V) où X = {r∈ℚ : ∃r′∈ℚ.(r′>r ∧ ¬(r′∈T ∧ r′∈V))}. (Il y a peut-être moyen de définir ce X de façon plus simple, en faisant référence uniquement à S et U, mais je n'ai pas trouvé ; on peut bien sûr réécrire T comme {r′∈ℚ : ∃r″∈ℚ.(r″<r′ ∧ ¬(r″∈S))} là-dedans et de même pour V, mais ça donne quand même quelque chose de bien compliqué, X = {r∈ℚ : ∃r′∈ℚ.(r′>r ∧ ∀r″∈ℚ.(r″<r′ ⇒ ¬¬(r″∈S∨r″∈U)))} — que je ne sais pas réécrire. Je me suis demandé si ce serait par hasard égal à {r∈ℚ : ((¬(r∈S))⇒(r∈U)) ∧ ((¬(r∈U))⇒(r∈S))}, mais je n'ai pas réussi à trancher, et j'ai abandonné avant d'avoir mal à la tête.)

On verra plus loin quelques conditions permettant d'affirmer l'existence d'une borne supérieure d'un ensemble de réels de Dedekind, mais je peux d'ores et déjà divulgâcher que c'est moins commode que pour les coupure de MacNeille. Donc sur ce terrain-là, les coupures de MacNeille gagnent (on peut d'ailleurs les définir très exactement comme un complété de ℚ par l'opération de prendre les bornes supérieures d'ensembles habités et majorés, mais je ne le ferai pas).

Le fait suivant marche comme pour les coupures de Dedekind, mais il faut que je refasse un peu la démonstration :

Proposition : Pour x,y,z trois coupures de MacNeille, on a d'une part x⊔y ⊲ z si et seulement si x⊲z et y⊲z, et d'autre part x⊔y < z si et seulement si x<z et y<z.

Démonstration : La preuve donnée de l'équivalence entre x⊔y < z et x<z ∧ y<z pour les réels de Dedekind donne exactement telle quelle une preuve de l'équivalence entre x⊔y ⊲ z et x⊲z ∧ y⊲z pour les coupures de MacNeille. Reste à montrer l'équivalence x⊔y < z et x<z ∧ y<z pour les coupures de MacNeille.

Or x⊔y < z signifie qu'il existe d>0 rationnel tel que x⊔y ≤ z−d ; ceci équivaut au fait qu'il existe d>0 rationnel tel que x ≤ z−d et y ≤ z−d. Ceci implique trivialement qu'il existe d′>0 rationnel tel que x ≤ z−d′ et d″>0 rationnel tel que y ≤ z−d″, c'est-à-dire x<z et y<z ; et dans l'autre sens, si d′,d″>0 comme on vient de dire existe, alors d := min(d′,d″) vérifie x ≤ z−d et y ≤ z−d, ce qui donne l'équivalence souhaitée. ∎

☞ Maintenant les mauvaises nouvelles

Ayant expliqué quelques (relativement) bonnes propriétés des coupures de MacNeille, il est temps d'expliquer pourquoi elles sont assez pourries quand même. Pour ça, je vais définir une coupure de MacNeille qui va servir à faire des contre-exemples brouwériens dans tous les sens : si p∈Ω est une valeur de vérité, l'ensemble {0} ∪ {1 : p} de ℚ, c'est-à-dire {t∈ℚ : (t=0) ∨ (t=1 ∧ p)} est habité et majoré, donc, d'après la proposition sur la construction des bornes supérieures, il possède une borne supérieure dans les coupures de MacNeille (la proposition parle d'une famille de coupures, mais on peut indicer l'ensemble par lui-même, ce n'est pa sun problème). Je vais noter θ_p la coupure en question.

Proposition : Si p∈Ω, la borne supérieure θ_p de {0} ∪ {1 : p} dans les coupure de MacNeille est donnée par la coupure (U,V) où U = {r∈ℚ : r<0 ∨ (¬¬p ∧ r<1)} et V = {r∈ℚ : r>1 ∨ (¬p ∧ r>0)}. (En particulier, on a θ_p = θ_¬¬p.)

Démonstration : La construction donnée par la proposition précédente considère d'abord l'intersection E des t^→ := {r∈ℚ : r>t} pour tous les t de {0} ∪ {1 : p}. Cette intersection est l'ensemble des rationnels qui sont dans tous les t^→, soit {r∈ℚ : r>0 ∧ (p ⇒ r>1)}. Maintenant, pour tout rationnel r, on a r>1 ou bien r≤1 : dans le premier cas, l'affirmation p ⇒ r>1 est vraie et dans le second elle est équivalente à ¬p ; donc p ⇒ r>1 équivaut à r>1 ∨ ¬p dans chacun des deux cas, donc c'est vrai en général (j'insiste sur le fait qu'il était crucial que r fût un rationnel pour tenir ce raisonnement). Et on a donc E = {r∈ℚ : r>0 ∧ (r>1 ∨ ¬p)} = {r∈ℚ : r>1 ∨ (¬p ∧ r>0)}. Sous cette forme (et en regardant chaque cas de la disjonction), il est clair que pour tout r∈E il existe r′<r tel que r′∈E : donc E = int^→(E) := {r∈ℚ : ∃r′∈ℚ.(r′<r ∧ r′∈E)}, et la proposition assure que ceci constitue notre coupure droite V.

La construction de la coupure gauche commence par considérer ℚ∖V = ℚ∖E = {r∈ℚ : r≤1 ∧ (¬p ⇒ r≤0)}. Un raisonnement analogue à celui qu'on vient de tenir (en distinguant les deux cas r≤0 et r>0) montre que c'est aussi {r∈ℚ : r≤0 ∨ (¬¬p ∧ r≤1)}. Sous cette forme, on voit alors que int^←(ℚ∖V) := {r∈ℚ : ∃r′∈ℚ.(r′>r ∧ r′∈(ℚ∖V))} = {r∈ℚ : r<0 ∨ (¬¬p ∧ r<1)}, et c'est notre coupure gauche U annoncée. ∎

Un point de vue différent pour décrire θ_p est que θ_p est l'unique coupure de MacNeille qui vaut 1 si p (ou même si ¬¬p) et 0 si ¬p : l'existence d'un tel élément n'est aucunement garanti par cette description (d'ailleurs, sur les réels de Dedekind, on ne peut l'affirmer), mais on vient de voir qu'il existe bien, et l'unicité résulte du corollaire ci-dessus.

Digression : Plus généralement, l'ensemble ℝ_MN des coupures de MacNeille a la propriété que, si p est une valeur de vérité quelconque, et x,y deux éléments de ℝ_MN, alors il existe z unique dans ℝ_MN qui vaut x si p et y si ¬p. Cette propriété est un peu plus faible que celle qui caractérise les (¬¬)-faisceaux, mais elle s'en approche (les réels étendus généraux ou réels classiques, eux, sont vraiment un (¬¬)-faisceau). ❧ Pour les gens savants : les réels étendus généraux sont justement l'ensemble des réels dans le topos des (¬¬)-faisceau, et les coupures de MacNeille sont ceux des étendus généraux qui sont bornés par deux rationnels (ou deux réels) de notre topos de départ. On peut en définir encore d'autres, par exemple les réels singleton qui sont le (¬¬)-faisceautisé de ℝ, ou, ce qui revient au même, ceux des réels étendus généraux qui (¬¬)-appartiennent à ℝ.

L'intérêt de la construction θ_p est qu'elle permet de construire toutes sortes de contre-exemples brouwériens :

Contre-exemples brouwériens :

1. θ_p est un réel de Dedekind si seulement si ¬p ∨ ¬¬p. En particulier, si toute coupure de MacNeille est un réel de Dedekind, alors pour tout p on a ¬p ∨ ¬¬p (la loi faible du tiers exclu).

2. On a : θ_p ⊓ θ_¬p = 0 et θ_p ⊔ θ_¬p = 1. On a aussi θ_p + θ_¬p = 1 pour n'importe quelle opération binaire ‘+’ sur ℝ_MN qui prolonge l'addition sur ℚ. Par ailleurs, ¬(θ_p = θ_¬p).

3. On a θ_p < θ_p + ½ inconditionnellement, mais θ_p ⊲ θ_p + ½ équivaut à ¬p ∨ ¬¬p. En particulier, si ‘<’ et ‘⊲’ coïncident sur les coupures de MacNeille, ou (ce qui revient au même) si ℝ est dense dans ℝ_MN pour l'ordre ‘<’, alors la loi faible du tiers exclu vaut.

4. On a (θ_p ⊓ θ_¬p) ⊲ ½, mais (θ_p<½) ∨ (θ_¬p<½) équivaut à ¬p ∨ ¬¬p. En particulier, si l'affirmation si x⊓y ⊲ z alors x<z ou bien y<z (et a fortiori si x⊓y < z alors x<z ou bien y<z) vaut pour les coupures de MacNeille, alors la loi faible du tiers exclu vaut.

5. L'ensemble {θ_p, θ_¬p} a exactement deux éléments. Son plus petit majorant (i.e., sa borne supérieure) vaut 1 ; mais il contient un élément >0 si et seulement si ¬p ∨ ¬¬p. En particulier, si la borne supérieure de tout ensemble fini de coupures de MacNeille est un sup fort (au sens qui sera défini plus bas), alors la loi faible du tiers exclu vaut.

6. On a 0⊲½, mais (θ_p<½) ∨ (θ_p>0) équivaut à ¬p ∨ ¬¬p. En particulier, si l'affirmation (❀) donnés x<x′ et y, on a soit x<y soit y<x′ (ou même celle-ci en renforçant l'hypothèse x<x′ en x⊲x′) vaut pour les coupures de MacNeille, alors la loi faible du tiers exclu vaut.

7. S'il existe un discernement (c'est-à-dire une relation irréflexive, symétrique et cotransitive) ‘⋄’ sur ℝ_MN tel que 0⋄1, alors la loi faible du tiers exclu vaut.

Démonstration : Montrons le (1). Si ¬p vaut, alors θ_p=0, qui est certainement un réel de Dedekind. Si ¬¬p vaut, alors θ_p=1, qui est aussi certainement un réel de Dedekind. Donc on a montré que ¬p ∨ ¬¬p implique θ_p∈ℝ. Montrons la réciproque : si θ_p est un réel de Dedekind, par la propriété (e) des coupures (ou, ce qui revient au même, par (❀)), on a θ_p>¼ ou bien θ_p<¾ : d'après la valeur que nous avons vue des coupures gauche et droite de θ_p, le premier implique ¬¬p et le second implique ¬p. On a bien l'équivalence.

Montrons le (2). D'après ce qu'on a vu, pour montrer une égalité (ou une négation d'égalité) entre coupures de MacNeille, on se contenter de la démontrer séparément dans les cas p et ¬p : or dans un cas θ_p=0 et θ_¬p=1, et dans l'autre cas c'est le contraire. Les égalités affirmées sont donc claires.

Montrons le (3). L'inégalité θ_p < θ_p + ½ est triviale sur la définition de <. Quant à l'inégalité θ_p ⊲ θ_p + ½, elle est claire si ¬p ∨ ¬¬p (puisque θ_p est alors un réel de Dedekind) ; mais réciproquement, θ_p ⊲ θ_p + ½ signifie que {r∈ℚ : r>1 ∨ (¬p ∧ r>0)} ∩ {r∈ℚ : r<½ ∨ (¬¬p ∧ r<3⁄2)} est habité, et en distinguant chacun des trois cas 0<r<½ (qui implique ¬p), ½≤r≤1 (impossible) et 1<r<3⁄2 (qui implique ¬¬p), ce qui est légitime car on compare des rationnels, on voit que ¬p ∨ ¬¬p vaut. (L'affirmation sur la densité de ℝ découle du fait qu'on a vu que x⊲y équivaut à l'existence d'un réel entre les deux.)

Montrons le (4). Le fait que (θ_p ⊓ θ_¬p) ⊲ ½ découle du fait que θ_p⊓θ_¬p=0. Comme précédemment, si ¬p ∨ ¬¬p alors (θ_p<½) ∨ (θ_¬p<½) est clair. Mais si θ_p<½ alors ¬p vaut et si θ_¬p<½ alors ¬¬p vaut.

Montrons le (5). L'ensemble F := {θ_p, θ_¬p} a exactement deux éléments car on a vu que θ_p et θ_¬p ne sont pas égaux. On a vu que son plus petit majorant θ_p ⊔ θ_¬p vaut 1. Si ¬p ∨ ¬¬p alors l'un de θ_p, θ_¬p vaut 1, donc l'ensemble contient bien un élément >0 ; mais réciproquement, si tel est le cas, on a θ_p>0 ou bien θ_¬p>0, et ceci entraîne ¬¬p ou ¬p. Enfin, pour ce qui est de l'affirmation sur le sup fort, la définition de ce terme exige, pour que 1 soit un sup fort, que F contienne un élément >b pour tout b<1, et on vient de voir que si c'est le cas pour b=0 alors ¬p ∨ ¬¬p.

Montrons le (6). Le fait que 0⊲½ est clair. On a déjà dit plus haut que θ_p<½ équivaut à ¬p et on voit de même que θ_p>0 équivaut à ¬¬p. Le reste est alors clair.

Montrons le (7). Si ‘⋄’ est irréflexive, symétrique et cotransitive et que 0⋄1, alors la cotransitivité nous assure que 0⋄θ_p ou bien θ_p⋄1. L'irréflexivité nous assure alors que ¬(θ_p=0) ou ¬(θ_p=1). Mais le premier implique ¬¬p et le second implique ¬p. ∎

Une fois admis qu'on ne peut pas affirmer la loi faible du tiers exclu (même si par ailleurs elle ne permet pas de prouver la loi du tiers exclu), ceci nous assure qu'on ne peut pas affirmer toutes sortes de choses sur les coupures de MacNeille : par exemple, on ne peut pas affirmer que ℝ est dense dedans pour ‘<’ ; on ne peut même pas affirmer que x ⊲ x+1 vaut pour tout x (le (3) nous le dit pour x ⊲ x+½, mais on voit bien qu'on peut tout doubler ou diviser par deux sans difficulté).

Tant qu'à faire, signalons que l'invocation de la loi faible du tiers exclu est ici optimale, en vertu de la :

Proposition : Si la loi faible du tiers exclu vaut, i.e. ∀p∈Ω.(¬p ∨ ¬¬p), alors toute coupure de MacNeille est une coupure de Dedekind.

Démonstration : Supposons la loi faible du tiers exclu. Soit (S,T) une coupure de MacNeille. Il s'agit de prouver la propriété (e), ∀s∈ℚ.∀t∈ℚ.((s<t) ⇒ (s∈S ∨ t∈T)) : soient s<t deux rationnels. Soit r rationnel tel que s<r<t. Par la loi faible du tiers exclu, on a ¬(r∈T) ou bien ¬¬(r∈T). Dans le premier cas, la propriété (e⁻) des coupures de MacNeille appliquée à s<r montre s∈S. Dans le second cas, on conclut t∈T par la propriété (b⁺) (qui dit : ∀r∈ℚ.∀t∈ℚ.((t>r ∧ ¬¬(r∈T)) ⇒ t∈T)) qu'on a montré sur les coupures droites dans la preuve de la proposition sur l'existence des bornes supérieures (je rappelle l'argument : si ¬¬(r∈T), prenons r″ tel que r<r″<t, alors r″∈S est impossible car par la propriété (d) cela entraînerait ¬(r∈T), une contradiction, c'est-à-dire que ¬(r″∈S), et la propriété (e⁻) permet d'en déduire t∈T). ∎

(On peut dire qu'on a affaire ici à des maths constructives à rebours : la loi faible du tiers exclu étant exactement équivalente à l'affirmation que, disons, ℝ = ℝ_MN, on a calibré précisément la force de cette affirmation.)

Le discernement standard sur ℝ

Il sera utile d'introduire sur les réels la notation x⋕y, lire x est discerné de y, pour x<y ou bien x>y. Cette relation s'appelle le discernement standard sur ℝ (et on va voir ci-dessous que c'est aussi équivalent à |x−y|>0, à x⊓y < x⊔y, ou encore à ∃u∈ℝ.(u·(x−y)=1)). Il s'agit bien d'un discernement au sens défini précédemment, c'est-à-dire que cette relation est irréflexive, symétrique et cotransitive : les deux premiers points sont triviaux, et la cotransitivité — laquelle affirme que si x⋕z et y est quelconque alors on a soit x⋕y soit y⋕z — découle immédiatement de la proposition (❀) : dans le cas où x<z, la proposition en question entraîne qu'on a soit x<y soit y<z, et mutatis mutandis dans le cas où x>z.

De plus, le discernement standard ‘⋕’ est serré, c'est-à-dire que si ¬(x⋕y) alors x=y (la réciproque étant évidente) : en effet, ¬(x⋕y) signifie ¬(x<y) et ¬(x>y), et on a vu que c'est pareil que x≥y et x≤y.

Plutôt que définir ‘⋕’ à partir de ‘<’ et ‘>’, on peut d'ailleurs préférer imaginer le contraire : x<y équivaut évidemment à x≤y et x⋕y (donc strictement inférieur peut se lire comme inférieur et discerné si on veut).

Si on s'intéresse aux réels étendus bornés (définis, je le rappelle, par les coupures de MacNeille, c'est-à-dire en affaiblissant (e) en (e⁻)), la relation x<y ou bien x>y n'est pas très intéressante : il reste vrai que à leur sujet ¬(x<y ∨ x>y) équivaut à x=y (puisque ¬(x<y) implique x≥y et ¬(x>y) implique x≤y), mais on ne peut pas affirmer que la relation en question soit un discernement, parce que ceci repose crucialement sur la proposition (❀). Peut-être qu'une meilleure relation à utiliser serait x⊓y < x⊔y, ce qui est équivalent à x⋕y pour les réels (de Dedekind), comme je le montrerai plus bas, mais pas pour les réels étendus bornés ; mais bon, ça ne change fondamentalement pas grand-chose : la négation de cette relation-là est aussi l'égalité, et on ne peut pas non plus affirmer qu'il s'agisse d'un discernement. En fait, j'ai expliqué par des contre-exemples brouwériens qu'on ne peut même pas affirmer qu'il existe de discernement sur ℝ_MN qui discerne 0 et 1. Du coup, il vaut mieux éviter d'utiliser le symbole ‘⋕’ pour les réels étendus bornés.

Récapitulatif des propriétés importantes de l'ordre sur les réels

(Propriétés à quantifier universellement sur toutes les variables libres.)