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

Suites convergentes et suites de Cauchy

☞ Convergence et convergence modulée

Une suite de réels est, bien sûr, une fonction ℕ→ℝ (et on note généralement quelque chose comme x_i l'image de n par la fonction) : rien de nouveau ici.

On dit qu'une suite (x_i) de réels tend ou converge (ou, pour insister, converge simplement) vers x_∞, ou qu'elle a x_∞ comme limite, lorsque, comme en maths classiques : ∀ε>0.∃n∈ℕ.∀i≥n.(|x_i−x_∞|<ε). Bien sûr, grâce à la densité de ℚ dans ℝ, il ne change rien ici d'imposer à ε d'être rationnel, ou même d'être de la forme, disons, 2^−m (puisque tout rationnel strictement positif majore un rationnel de cette forme) ; on peut aussi remplacer la dernière inégalité stricte par une inégalité large sans rien changer.

On dira qu'une suite (x_i) converge de façon modulée vers x_∞ (ou qu'elle tend de façon modulée, ou modulément si on me pardonne ce néologisme ; ou encore, que la convergence est modulée) lorsque ∃ν:ℕ→ℕ.∀m∈ℕ.∀i≥ν(m).(|x_i−x_∞|<2^−m). D'après ce qui a été dit sur le fait de pouvoir prendre ε de la forme 2^−m, la convergence modulée implique la convergence au sens du paragraphe précédent (convergence non supposée modulée s'il y a besoin de souligner).

Classiquement ou bien en présence de l'axiome du choix dénombrable, toute convergence est automatiquement modulée : en effet, en présence de l'axiome du choix dénombrable, on peut, pour chaque m, choisir un n tel que ∀i≥n.(|x_i−x_∞|<2^−m), et définir ν(m) comme le n choisi ; en fait, l'axiome du choix dénombrable pour les parties habitées de ℕ suffit, et en maths classiques cette forme de choix est démontrable car on peut prendre le plus petit élément. Mais dans les maths constructives sans choix, on ne peut pas affirmer que toute suite de réels qui tend vers zéro (disons) tende vers zéro de façon modulée.

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 la différence entre la convergence et la convergence modulée, une suite de réels (u_i) est représentée (de façon externe dans un topos de faisceaux) par une suite de fonctions continues, disons X→ℝ pour simplifier. Le fait que (u_i) converge vers u_∞ se traduit de façon externe par : pour tout ε>0 il existe un recouvrement ouvert (V_j)_j∈J de X tel que pour tout j∈J il existe n∈ℕ tel que si ξ∈V_j et i≥n on ait |u_i(ξ) − u_∞(ξ)| ≤ ε. En revanche, le fait que (u_i) converge modulément vers u_∞ se traduit de façon externe par : il existe un recouvrement ouvert (V_j)_j∈J de X tel que pour tout ε>0 et pour tout j∈J il existe n∈ℕ tel que si ξ∈V_j et i≥n on ait |u_i(ξ) − u_∞(ξ)| ≤ ε (donc en permutant le quantificateur universel sur le ε>0 et le quantificateur existentiel sur le recouvrement ouvert). Ces deux notions de convergence, que je suis tenté de qualifier respectivement de convergence locale et de convergence localement uniforme, sont strictement intermédiaires entre la convergence ponctuelle (ou convergence simple) et la convergence uniforme : je renvoie à cette question MathOverflow pour une discussion un peu plus longue et des contre-exemples à toutes les implications : notamment, la réponse que j'ai reçue, réinterprétée de façon interne, montre que la convergence n'entraîne pas en général la convergence modulée.

☞ On ne peut pas affirmer qu'une suite croissante majorée ait une limite

Mais je ne veux pas trop insister ici sur la convergence modulée : je l'ai mentionnée juste parce que c'est un point qui peut être source de confusion (certains auteurs appellent convergence ce que j'appelle convergence modulée). Le problème suivant est plus sérieux et ne repose pas sur des questions de choix :

Classiquement, une suite de réels qui est décroissante et minorée, ou bien croissante et majorée, admet une limite. Constructivement, on ne peut pas l'affirmer. En effet :

Contre-exemple brouwérien : Soit (u_i) une suite binaire (c'est-à-dire à valeurs dans {0,1}) croissante. Si elle a une limite b, alors : soit b=0 et la suite vaut constamment 0, soit b=1 et la suite prend la valeur 1 (et bien sûr elle est alors constamment égale à 1).

En particulier, si toute suite de réels croissante et majorée a une limite, alors le principe limité d'omniscience LPO vaut (je rappelle que LPO affirme que toute suite binaire est soit nulle soit a un terme égal à 1).

Démonstration : On a ¼<¾, donc par (❀), soit b<¾ soit b>¼. Si b<¾, (en prenant ε=¼ dans la définition de la convergence) on voit qu'il existe n tel que pour i≥n on ait u_i<1, c'est-à-dire u_i=0 puisqu'on a affaire à une suite binaire ; et comme elle est croissante, elle vaut en fait constamment 0. De même b>¼, (en prenant ε=¼ dans la définition de la convergence) on voit qu'il existe n tel que pour i≥n on ait u_i>0, c'est-à-dire u_i=1 puisqu'on a affaire à une suite binaire. ∎

☞ Le critère de Cauchy

On dit qu'une suite (x_i) de réels est (simplement) de Cauchy lorsque, comme en maths classiques : ∀ε>0.∃n∈ℕ.∀i,j≥n.(|x_i−x_j|<ε). C'est évidemment le cas des suites convergentes. Comme précédemment, grâce à la densité de ℚ dans ℝ, il ne change rien ici d'imposer à ε d'être rationnel, ou même d'être de la forme, disons, 2^−m ; on peut aussi remplacer la dernière inégalité stricte par une inégalité large sans rien changer. On dira que (x_i) est modulément de Cauchy ou que sa cauchyïtude est modulée (désolé pour tous les néologismes) lorsque ∃ν:ℕ→ℕ.∀m∈ℕ.∀i,j≥ν(m).(|x_i−x_j|<2^−m) : là aussi, les suites modulément de Cauchy sont de Cauchy, et les suites modulément convergentes sont modulément de Cauchy.

Les suites de Cauchy sont-elles convergentes ? Oui ! On va le prouver en commençant par le :

Lemme : L'image d'une suite de Cauchy (i.e., l'ensemble de ses valeurs) est une partie localisée inférieurement (et, bien sûr, supérieurement).

Démonstration : Considérons u<v deux réels, d'écart ε := v−u et de moyenne z := ½(u+v). La propriété de Cauchy permet de trouver un rang n à partir duquel deux termes x_i,x_j quelconques de la suite sont à distance <¼·ε. Posons B := {x_i : i≥n}.

Comme z − ¼·ε < z + ¼·ε, par (❀), on a soit x_n > z − ¼·ε soit x_n < z + ¼·ε. Dans le premier cas, on en déduit x_i > z − ½·ε = u pour tout i≥n, c'est-à-dire que u minore B ; dans le second cas, l'élément x_i de B est <v. On vient donc de prouver que soit u minore B soit B a un élément <v.

Comme par ailleurs A := {x₀,…,x_n−1} est localisé inférieurement (on l'a vu plus haut), soit u minore A soit il existe un élément de A qui est <v. En mettant ces faits ensemble, sur A∪B on voit (comme on l'a fait pour montrer que la réunion de deux ensembles localisé inférieurement est localisée inférieurement) que soit u minore A∪B soit il existe un élément de A∪B qui est <v. Or A∪B est l'ensemble {x_i : i∈ℕ} des termes de la suite. ∎

Théorème : Dans les réels de Dedekind, toute suite de Cauchy admet une limite.

Démonstration : Si (x_i) est une suite de Cauchy, l'ensemble {x_i} de ses valeurs est habité (trivialement), minoré (par la propriété de Cauchy) et localisée inférieurement (d'après le lemme). Comme on a vu qu'une partie habitée, minorée et localisée inférieurement a un infimum, inf {x_i} a bien un sens, et plus généralement inf {x_i : i≥n} en a un quel que soit n (retirer des termes au début d'une suite de Cauchy donne évidemment encore une suite de Cauchy). Symétriquement, sup {x_i : i≥n} existe. Les inf {x_i : i≥n} forment une suite croissante en n, et les sup {x_i : i≥n} une suite décroissante. Ces suites sont elles-mêmes de Cauchy (car si |x_i−x_j|≤ε pour i,j≥m, alors |(inf {x_i : i≥n}) − x_m| ≤ ε pour tout n≥m, donc |(inf {x_i : i≥p}) − (inf {x_i : i≥q})| ≤ 2·ε pour tous p,q≥m). On peut donc prendre le sup de la première et l'inf de la seconde. On peut donc poser liminf_i (x_i) := sup_n inf_i≥n x_i, et symétriquement limsup_i (x_i) := inf_n sup_i≥n x_i. Mais la propriété de Cauchy permet facilement de voir qu'elles sont égales (leur écart est ≤ε pour tout ε>0).

Si z est cette valeur commune, et si ε>0, alors comme z−ε < liminf_i (x_i) = sup_n inf_i≥n x_i, par définition du supremum, il existe n tel que inf_i≥n x_i > z−ε, ce qui (comme l'infimum est un minorant) assure x_i > z−ε pour tout i≥n. Symétriquement, on peut trouver un (autre) n tel que x_i < z+ε pour tout i≥n ; et en prenant le plus grand de ces deux n, on a trouvé un n tel que |x_i−z|<ε pour tout i≥n. ∎

On peut aussi se convaincre, par le caractère explicite du dernier paragraphe de cette démonstration, que toute suite modulément de Cauchy converge modulément. (C'est d'ailleurs également facile à déduire du théorème qui précède sans aller fouiller dans sa démonstration.)

Donc en fait convergent équivaut à de Cauchy, et l'équivalence analogue vaut pour les propriétés modulées.

☞ Un mot sur les séries

On peut bien sûr développer une théorie des séries de nombres réels en définissant simplement la série (Σx_i) comme la suite de ses sommes partielles (∑_i<n x_i), comme d'habitude. On dit que la série est convergente, resp. modulément convergente, resp. de Cauchy, resp. modulément de Cauchy, lorsque la suite de ses sommes partielles a la même propriété. On dit que la série est absolument convergente lorsque la série des valeurs absolues est convergentes, et on peut faire la même définition sous forme modulée. Comme en maths classiques, l'inégalité triangulaire permet de montrer :

Corollaire : Dans les réels de Dedekind, toute série absolument convergente est convergente.

À titre d'exemple, si (b_i) est une suite binaire, c'est-à-dire à valeurs dans {0,1}, on peut définir le nombre réel ∑_i b_i·2⁻⁽ⁱ⁺¹⁾ (compris entre 0 et 1) dit défini par ce développement binaire.

⚠ Attention : Je dois souligner qu'en maths constructives on ne peut pas l'affirmer qu'un réel (entre 0 et 1, disons), même si je le suppose de Cauchy ou de Cauchy modulé (ce terme sera défini ci-dessous), ou même si je suppose l'axiome du choix dénombrable, ait nécessairement un développement binaire, c'est-à-dire s'écrive sous la forme ∑_i b_i·2⁻⁽ⁱ⁺¹⁾ avec b_i∈{0,1}. Ce n'est pas un problème de choix ici : c'est que l'existence d'un tel développement assure (en regardant la valeur de b₀) qu'on a soit x≥½ soit x≤½, chose qu'on ne peut pas affirmer en général, on verra ci-dessous le lien avec LLPO analytique. (Cf. le problème à la fin de ce contrôle où je demandais en quelque sorte de prouver — évidemment sans le dire comme ça — que dans le topos effectif l'affirmation tous les réels entre 0 et 1 ont un développement binaire n'est pas valable, et que les réels ayant un développement binaire ne sont même pas stables par addition.) En revanche, tout réel de Cauchy modulé (entre −1 et 1, disons) peut au moins s'écrire ∑_i b_i·2⁻⁽ⁱ⁺¹⁾ avec b_i∈{−1,0,1} : cf. cet article pour les explications.

[Optionnel] Et les réels de Cauchy ?

☡ Guide de lecture : Hic sunt leones ! On peut survoler ou sauter cette section, qui n'est là en gros que parce que des gens insistent pour parler de réels de Cauchy.

☞ Réels de Cauchy et réels de Cauchy modulés

On dit qu'un réel de Dedekind est (simplement) de Cauchy lorsqu'il est la limite d'une suite de rationnels. On dit qu'il est modulément de Cauchy (ou que c'est un réel de Cauchy modulé voire un réel modulé tout court) lorsqu'il est la limite modulée d'une suite de rationnels. Attention car la terminologie fluctue pas mal : beaucoup d'auteurs disent juste de Cauchy pour demander l'existence d'une suite modulément de Cauchy de rationnels ; d'autres appellent ça un nombre réel régulier.

Notons qu'on peut simplifier un peu la définition d'un réel de Cauchy modulé : quitte à remplacer le module ν(n) par max(ν(0),…,ν(n)) et ensuite r_i par r_ν(i), on peut supposer que |r_i−x| < 2⁻ⁱ ; c'est-à-dire que x est un réel de Cauchy modulé lorsqu'il existe une suite (r_i) de rationnels telle que ∀i∈ℕ.(|r_i−x|<2⁻ⁱ).

Classiquement ou bien en présence de l'axiome du choix dénombrable, ces distinctions sont sans objet : tous les réels sont modulément de Cauchy. En effet, en présence de l'axiome du choix dénombrable, si x est un réel, on peut choisir un rationnel r_n tel que x − 2⁻ⁿ < r_n < x + 2⁻ⁿ, et alors la suite r_n est modulément de Cauchy et converge vers x ; et classiquement, on peut prendre le premier rationnel (pour une énumération explicite quelconque de ℚ) dans l'intervalle qu'on vient de dire.

Mais constructivement et sans choix… c'est un peu le chaos. Bien que ℚ soit dense dans ℝ, on ne peut pas affirmer que tout réel soit de Cauchy, et on ne peut pas affirmer que tout réel de Cauchy soit modulément de Cauchy.

Par ailleurs, on ne peut même pas affirmer que la limite d'une suite de Cauchy de réels de Cauchy soit un réel de Cauchy, et même en saupoudrant le mot modulé un peu partout ça ne marche toujours pas : le problème est double, d'une part se donner une suite de Cauchy de réels de Cauchy n'est pas la même chose que se donner une suite double (parce que chaque réel de Cauchy est limite d'une suite de Cauchy de rationnels, mais on n'a pas le moyen de les choisir), et même si on se donne la suite double, une suite de Cauchy de suites de Cauchy de rationnels ne permet pas forcément de fabriquer une suite de Cauchy de rationnels ; les explications sont dans ce papier, qu'on peut compléter par cette petite note de ma part (source LaTeX ici), dont j'extrais notamment (en l'adaptant un peu) l'énoncé positif un peu surprenant et subtil suivant (il partie du folklore) :

☞ Modulation automatique

Proposition : Si x est un réel modulément de Cauchy, et si (s_i) est une suite de rationnels qui tend (sans hypothèse de modulation !) vers x, alors en fait cette convergence est automatiquement modulée.

(Autrement dit, si un réel est limite d'une suite de rationnels modulément convergente, alors toute suite de rationnels qui converge vers lui le fait de façon modulée. Dit de façon encore différente : si deux suites de rationnels ont la même limite et que la convergence de l'une est modulée, alors la convergence de l'autre est aussi modulée.)

Démonstration : Par hypothèse, il existe une suite de rationnels (r_i) qui converge modulément vers x ; et comme expliqué ci-dessus, on peut supposer que |r_i−x| < 2⁻ⁱ. On suppose que (s_i) est une suite de rationnels qui tend vers x et on veut montrer qu'elle le fait de façon modulée.

Soit n∈ℕ. Comme (s_i) tend vers x, il existe m, dont on peut certainement supposer m≥n+2, tel que i≥m implique |s_i−x| < 2⁻⁽ⁿ⁺²⁾ ; par ailleurs, pour i≥m on a aussi |r_i−x| < 2⁻⁽ⁿ⁺²⁾ (puisque i≥n+2), et ces deux inégalités ensemble impliquent |s_i−r_i| < 2⁻⁽ⁿ⁺¹⁾. On vient de montrer : (†) pour tout n∈ℕ il existe m≥n+2 tel que i≥m implique |s_i−r_i| < 2⁻⁽ⁿ⁺¹⁾.

Maintenant, posons E_n := {m∈ℕ : m≥n+2 ∧ ∀i≥m.(|s_i−r_i| < 2⁻⁽ⁿ⁺¹⁾)}. On vient de montrer que (†) E_n est habité pour tout n. Par ailleurs, j'affirme que E_n est décidable (je rappelle que ça signifie que pour tout m∈ℕ on a m∈E_n ou bien ¬(m∈E_n)). En effet, une fois qu'on a un m₀∈E_n, tout m≥m₀ est trivialement encore dans E_n, et pour ce qui est des m<m₀, on procède par récurrence décroissante sur m : d'une part si ¬(m∈E_n) alors certainement ¬((m−1)∈E_n), et d'autre part si m∈E_n alors on a (m−1)∈E_n si et seulement si (m−1)≥n+2 et |s_m−1−r_m−1| < 2⁻⁽ⁿ⁺¹⁾, et toutes ces conditions sont décidables (booléennes, si on veut : elle sont soit vraies soit fausses), parce que les inégalités entre entiers ou entre rationnels sont décidables. Bref, l'ensemble E_n est une partie habitée et décidable de ℕ.

Or on a vu au début du volet précédent que toute partie habitée et décidable de ℕ a un plus petit élément. On peut donc appeler μ(n) := min(E_n) son plus petit élément, c'est-à-dire le plus petit m≥n+2 tel que i≥m implique |s_i−r_i| < 2⁻⁽ⁿ⁺¹⁾.

Maintenant, si i≥μ(n), on a d'une part |s_i−r_i| < 2⁻⁽ⁿ⁺¹⁾ et d'autre part |r_i−x| < 2⁻⁽ⁿ⁺²⁾. Ces deux inégalités ensemble impliquent |s_i−x| < 2⁻ⁿ. La convergence de (s_i) vers x est donc bien modulée par la fonction μ qu'on a construite. ∎

En particulier, on peut garder à l'esprit qu'une suite de rationnels qui tend vers 0 tend vers zéro de façon automatiquement modulée.

Le point crucial dans la proposition ci-dessus était la décidabilité des inégalités entre rationnels. On ne peut certainement pas affirmer que si deux suites de réels ont la même limite et que la convergence de l'une est modulée, alors la convergence de l'autre est aussi modulée.

Bon, la notion de nombres réels de Cauchy est assez pourrie si la limite d'une suite de Cauchy de nombres réels de Cauchy n'est pas forcément de Cauchy. Dans mon esprit cela suggère qu'il faut laisser tomber cette notion, mais il est vrai qu'ils sont utiles du point de vue computationnel (noter cependant que dans le topos effectif, les réels de Cauchy et de Dedekind coïncident, donc on n'a pas trop à se poser la question).

Une notion potentiellement intéressante serait la clôture de Cauchy des rationnels : c'est la plus petite partie de l'ensemble ℝ des réels de Dedekind qui contienne les rationnels et qui soit stable par limites de suites de Cauchy (et on peut bien sûr aussi définir une version modulée de la même chose), c'est-à-dire l'intersection de toutes les parties de ℝ contenant ℚ et stables par limites de suites de Cauchy (ou, si on veut, l'« adhérence séquentielle » de ℚ). Mais je ne sais pas si on sait en dire grand-chose d'intéressant.

Redite des principes (séquentiels) d'omniscience

☞ Redite des principes séquentiels

Dans le volet précédent de cette série de billets, j'avais introduit divers principes d'omniscience, dont je reproduis un énoncé possible ici (je rappelle à toutes fins utiles que ℕ_∞ désigne l'ensemble des suites binaires croissantes et que, dedans, la suite identiquement nulle peut être notée soit 0 soit ∞ — cette dernière notation étant commode pour comparer ℕ_∞ à ℕ mais qu'il vaut mieux éviter quand, comme ici, je préfère le voir comme une partie de 2^ℕ) :

• Le principe limité d'omniscience ou LPO affirme qu'une suite binaire (qu'on peut supposer croissante si on veut) est soit nulle soit a un terme non-nul : ∀u∈ℕ_∞.(u=0 ∨ u⋕0).

• Le principe limité faible d'omniscience ou WLPO affirme qu'une suite binaire (qu'on peut supposer croissante si on veut) est soit nulle soit n'est pas nulle : ∀u∈ℕ_∞.(u=0 ∨ ¬(u=0)).

• Le principe de Markov ou MP affirme qu'une suite binaire (qu'on peut supposer croissante si on veut) qui n'est pas nulle a un terme non-nul : ∀u∈ℕ_∞.((¬(u=0)) ⇒ (u⋕0)).

• Le moindre principe limité d'omniscience ou LLPO affirme à propos de deux suites binaires (qu'on peut supposer croissantes si on veut) que s'il n'est pas vrai que toutes les deux ont un terme non-nul, alors l'une des deux est nulle : ∀u∈ℕ_∞.∀v∈ℕ_∞.((¬((u⋕0) ∧ (v⋕0))) ⇒ ((u=0) ∨ (v=0))).

• Le moindre principe limité faible d'omniscience ou WLLPO (peut-être plus souvent appelé principe de Markov disjonctif ou MP^∨) affirme à propos de deux suites binaires (qu'on peut supposer croissantes si on veut) que s'il n'est pas vrai que toutes les deux ont un terme non-nul [cf. remarque ci-dessous] et s'il n'est pas non plus vrai que toutes les deux sont nulles, alors l'une des deux n'est pas nulle : ∀u∈ℕ_∞.∀v∈ℕ_∞.(((¬((u⋕0) ∧ (v⋕0))) ∧ (¬((u=0) ∧ (v=0)))) ⇒ ((¬(u=0)) ∨ (¬(v=0)))).

Pour distinguer ces principes de ceux qui vont suivre, on peut les qualifier de principes séquentiels d'omniscience (ou principes d'omniscience séquentiels pour réussir à caser les autres adjectifs, étant bien entendu que c'est le principe qui est séquentiel, pas l'omniscience ; i.e., on peut parler de LLPO séquentiel, par exemple).

Les formulations ne sont pas exactement celles que j'avais données précédemment, mais elles sont équivalentes. D'abord, le fait qu'on puisse supposer les suites binaires croissantes si on veut vient du fait qu'à toute suite binaire b∈{0,1}^ℕ on peut associer une suite binaire croissante μ(b)∈ℕ_∞ dont le n-ième terme est le maximum des termes ≤n de la suite b, de sorte que μ(b) a un terme non-nul si et seulement si b en a un (i.e. μ(b)⋕0 ssi b⋕0), et par ailleurs μ(b) = b si b est déjà croissante, ce qui permet de mettre comme on veut {0,1}^ℕ (l'ensemble des suites binaires) ou ℕ_∞ (l'ensemble des suites croissantes) dans les quantificateurs.

☞ Sur les hypothèses de WLLPO séquentiel

Ma formulation de WLLPO peut sembler plus surprenante : par rapport à ma formulation dans le billet précédent, j'ai ajouté une hypothèse demandant qu'il ne soit pas vrai que les deux suites ont un terme non-nul, en plus de l'hypothèse (que j'avais déjà écrite) qu'il n'est pas non plus vrai que toutes les deux sont nulles. La raison pour laquelle je veux mettre cette hypothèse supplémentaire est qu'elle sera importante pour avoir un parallèle parfait avec les principes analytiques que je vais dire. La raison pour laquelle elle ne change rien est la remarque suivante.

Remarque : L'affirmation pour deux suites binaires, s'il n'est pas vrai que toutes les deux sont nulles, alors l'une des deux n'est pas nulle (∀u∈ℕ_∞.∀v∈ℕ_∞.((¬((u=0) ∧ (v=0))) ⇒ ((¬(u=0)) ∨ (¬(v=0))))) équivaut à la même affirmation à laquelle on ajoute l'hypothèse Ⓗ qu'il ne soit pas vrai que les deux suites ont un terme non-nul (l'hypothèse Ⓗ est donc ¬((u⋕0) ∧ (v⋕0)), et l'affirmation complète avec elle est ∀u∈ℕ_∞.∀v∈ℕ_∞.(((¬((u⋕0) ∧ (v⋕0))) ∧ (¬((u=0) ∧ (v=0)))) ⇒ ((¬(u=0)) ∨ (¬(v=0))))). Autrement dit, cette hypothèse supplémentaire ne ne change rien dans la formulation de WLLPO séquentiel ; de plus, ceci est orthogonal à la possibilité d'ajouter l'hypothèse que les suites soient croissantes.

Démonstration : Je reprends une construction et en gros le raisonnement que j'ai utilisés pour prouver que LLPO ⇒ WLPO (où WLPO avait été formulé sans l'hypothèse Ⓗ) : si u,v sont deux suites binaires, je peux définir deux suites binaires a,b en décrétant que a_n vaut 1 lorsque u_n=1 et que pour tout k<n on a u_k=0 et v_k=0, et 0 sinon, et (pas tout à fait symétriquement) que b_n vaut 1 lorsque v_n=1 et u_n=0, et que pour tout k<n on a u_k=0 et v_k=0, et 0 sinon. (En plus clair, on entrelace les suites u,v dans l'ordre u₀,v₀,u₁,v₁,u₂,… on garde le premier 1 éventuel, et tous les autres termes valent 0, et ceci définit les suites a,b entrelacées dans l'ordre a₀,b₀,a₁,b₁,a₂,….)

Sur cette construction, il est facile de voir qu'on ne peut pas avoir simultanément a⋕0 et b⋕0 (autrement dit, a,b vérifient toujours Ⓗ). D'autre part, a=b=0 implique u=v=0 (donc si on suppose que ce dernier ne vaut pas, le premier ne vaut pas non plus). Et enfin, u=0 implique a=0 (donc ¬(a=0) implique ¬(u=0)) et bien sûr v=0 implique b=0 (donc ¬(b=0) implique ¬(v=0)).

Bref, en appliquant ma formulation de WLLPO avec l'hypothèse Ⓗ aux suites a,b, on obtient la formulation d'origine sur les suites u,v. (Et si on veut en outre pouvoir supposer les suites croissantes, on applique à a,b la même construction μ discutée plus haut, qui ne modifie pas la validité de toutes les égalités ou discernements.) ∎

Énoncés analogues des principes analytiques

☞ Formulation des principes analytiques

Voici maintenant des principes analogues portant sur les réels, et qu'on peut collectivement qualifier de principes analytiques d'omniscience :

• Le principe limité d'omniscience analytique ou LPO analytique affirme qu'un réel est soit nul soit discerné de zéro : ∀x∈ℝ.(x=0 ∨ x⋕0).

• Le principe limité faible d'omniscience analytique ou WLPO analytique affirme qu'un réel est soit nul soit n'est pas nul : ∀x∈ℝ.(x=0 ∨ ¬(x=0)).

• Le principe de Markov analytique ou MP analytique affirme qu'un réel qui n'est pas nul est discerné de zéro : ∀x∈ℝ.((¬(x=0)) ⇒ (x⋕0)).

• Le moindre principe limité d'omniscience analytique ou LLPO analytique affirme à propos de deux réels que s'il n'est pas vrai que toutes les deux sont discernés de zéro, alors l'un des deux est nul : ∀x∈ℝ.∀y∈ℝ.((¬((x⋕0) ∧ (y⋕0))) ⇒ ((x=0) ∨ (y=0))).

• Le moindre principe limité faible d'omniscience analytique ou WLLPO analytique affirme à propos de deux réels que s'il n'est pas vrai que tous les deux sont discernés de zéro et s'il n'est pas non plus vrai que tous les deux sont nuls, alors l'un des deux n'est pas nul : ∀x∈ℝ.∀y∈ℝ.(((¬((x⋕0) ∧ (y⋕0))) ∧ (¬((x=0) ∧ (y=0)))) ⇒ ((¬(x=0)) ∨ (¬(y=0)))).

On note souvent LPO_ℝ, WLPO_ℝ, MP_ℝ, LLPO_ℝ, WLLPO_ℝ (respectivement) pour les principes analytiques que je viens d'énoncer. (Et pour insister, les principes séquentiels peuvent se noter : LPO_séq, WLPO_séq, MP_séq, LLPO_séq, WLLPO_ℝ respectivement.)

Je vais donner des formulations équivalentes plus agréables ci-dessous, mais celles-ci sont destinées à maximiser le parallélisme entre la version séquentielle et la version analytique.

☞ Chaque principe analytique impliquent le principe séquentiel correspondant…

Chaque principe analytique implique le principe séquentiel de même nom : tels que je les ai formulés (de façon complètement parallèle), c'est facile, donnée une suite binaire croissante u (et éventuellement une autre v), il suffit d'appliquer le principe analytique à 2^−u (et éventuellement 2^−v) que j'ai défini plus haut comme le réel dont l'écriture binaire est donnée par u, et faire usage du fait vu précédemment que 2^−u ⋕ 0 équivaut à u⋕0 (et se rappeler que, sur les réels comme sur les suites binaires, x=0 est la négation de x⋕0).

☞ …et réciproquement avec le Choix dénombrable

Les réciproques (c'est-à-dire les implications dans le sens principe d'omniscience séquentiel ⇒ principe d'omniscience analytique) valent en présence de l'axiome du choix dénombrable, mais ne peuvent pas être affirmées en général. Voici qui justifie les réciproques en présence de l'axiome du choix dénombrable, et qui est par ailleurs une construction par ailleurs assez intéressante et instructive pour être signalée :

Proposition : En supposant l'axiome du choix dénombrable, si x est un réel, il existe une suite binaire croissante (b_i) (i.e., un élément de ℕ_∞) telle que x⋕0 équivaille à b⋕0.

Démonstration : Pour chaque i∈ℕ, comme 2⁻ⁱ>0, d'après (❀), on a soit |x|<2⁻ⁱ soit |x|>0 (ce dernier étant équivalent à x⋕0). Si on veut, cela se traduit en disant que la partie B_i := {0 : |x|<2⁻ⁱ} ∪ {1 : |x|>0} de {0,1}, c'est-à-dire la partie contenant 0 si |x|<2⁻ⁱ et 1 si |x|>0, est habitée pour chaque i. L'axiome du choix dénombrable permet de choisir un élément b_i de chaque B_i : on a alors |x|<2⁻ⁱ si b_i=0 et |x|>0 si b_i=1 ; par ailleurs, quitte à modifier la suite binaire (b_i) pour remplacer chaque terme par le maximum de toutes les valeurs jusqu'à lui, on peut avoir (b_i) croissante.

Si b⋕0, cela signifie qu'il existe i tel que b_i=1, ce qui implique |x|>0 (i.e., x⋕0) d'après ce qui a été dit. Réciproquement, si x⋕0, c'est-à-dire |x|>0, il existe i tel que |x|≥2⁻ⁱ, donc b_i≠0, mais comme b_i est une suite binaire, b_i=1, et on a bien b⋕0. On a donc prouvé l'équivalence. ∎

En appliquant cette proposition aux différents réels dont parlent les principes d'omniscience analytique, on voit que l'axiome du choix dénombrable donne les réciproques annoncées.

En fait, même en maths constructives sans choix, on a une réciproque partielle : chaque principe d'omniscience séquentiel implique le principe d'omniscience analytique de même nom si on le restreint aux réels de Cauchy modulés. (Et comme la preuve que j'ai donnée dans le sens principe d'omniscience analytique ⇒ principe d'omniscience séquentiel construit des réels de Cauchy modulés 2^−u, on a du coup une équivalence.) En effet, si x est un réel de Cauchy modulé, c'est-à-dire s'il existe une suite (r_i) de rationnels telle que |r_i−x|<2⁻ⁱ pour tout i, alors on peut définir une suite binaire (b_i) par b_i=0 si |r_i|≤2⁻ⁱ et b_i=1 si |r_i|>2⁻ⁱ (cette définition a bien un sens car l'inégalité sur les rationnels est décidable : c'est ce qui fait qu'on n'a pas besoin de choix ici — enfin, on utilise le choix unique) : alors il n'est pas difficile de vérifier que x⋕0 vaut si et seulement si la suite b a un terme égal à 1, i.e. b⋕0. Je crois avoir montré que, au moins pour LPO, on a même l'implication de LPO séquentiel vers LPO analytique pour les réels de Cauchy (non supposés modulés cette fois), mais c'est plus technique et il faut utiliser trois fois LPO : je n'ai pas eu le courage d'essayer de savoir si on a quelque chose d'analogue pour les autres principes d'omniscience.

☞ Implications entre principes analytiques

Pour ce qui est des implications entre les principes analytiques que j'ai évoqués, on a (exactement comme entre les principes séquentiels) :

LEM (le tiers exclu) ⇒ LPO_ℝ ⇒ WLPO_ℝ ⇒ LLPO_ℝ ⇒ WLLPO_ℝ,
et LPO_ℝ ⇒ MP_ℝ ⇒ WLLPO_ℝ,

Celles qui ne sont pas complètement évidentes sur les définitions sont le fait que WLPO_ℝ ⇒ LLPO_ℝ (pour ça on peut soit reprendre la démonstration que j'ai donnée dans le cas séquentiel, soit utiliser l'équivalence que je donne plus bas de WLPO_ℝ et LLPO_ℝ avec ∀x∈ℝ.(x⋖0 ∨ x=0 ∨ x⋗0) et ∀x∈ℝ.(x≤0 ∨ x≥0) respectivement), et MP_ℝ ⇒ WLLPO_ℝ (pour ça on peut utiliser l'équivalence que je donne plus bas de WLLPO_ℝ avec ∀x∈ℝ.((¬(x=0)) ⇒ (x⋖0 ∨ x⋗0)) en se rappelant que x⋕0 équivaut à x<0 ∨ x>0).

À part ça, il y a plein de choses que personne ne semble savoir. Par exemple, j'ignore (et je pense que tout le monde ignore) si la conjonction de WLLPO_ℝ et de LLPO_séq implique LLPO_ℝ.

Divers équivalents des principes analytiques

☞ Reformulations de LPO analytique

Les formulations que j'ai données de certains des principes d'omniscience analytique ne sont pas les plus heureuses. Mais il y a des équivalents plus agréables :

Proposition : LPO analytique admet les équivalents suivants :

• ∀x∈ℝ.(x=0 ∨ x⋕0) : tout réel est soit nul soit discerné de zéro.
• ∀x∈ℝ.(x<0 ∨ x=0 ∨ x>0) : tout réel est soit nul soit strictement négatif soit strictement positif.
• ∀x≥0.(x=0 ∨ x>0) : tout réel positif au sens large est soit nul soit strictement positif.
• ∀x∈ℝ.(x>0 ∨ x≤0) : tout réel est soit strictement positif soit négatif au sens large.

Démonstration : La première formulation est celle que j'ai prise comme définition. L'équivalence entre les deux premières formulations résulte du fait que x⋕0 équivaut à x<0 ∨ x>0. La seconde formulation implique trivialement la troisième, et pour ce qui est de la réciproque il suffit d'appliquer la troisième à |x| et se rappeler que |x|>0 équivaut à x⋕0. La quatrième formulation découle évidemment de la seconde, et pour la réciproque il suffit d'appliquer la quatrième à x et −x séparément et d'écarter le cas manifestement impossible. ∎

☞ Reformulations de WLPO analytique

Proposition : WLPO analytique admet les équivalents suivants :

• ∀x∈ℝ.(x=0 ∨ ¬(x=0)) : tout réel est soit nul soit n'est pas égal à zéro.
• ∀x∈ℝ.(x⋖0 ∨ x=0 ∨ x⋗0) (où je rappelle que x⋗0 désigne la négation de x≤0) : tout réel est soit nul soit n'est pas positif au sens large soit n'est pas négatif au sens large.
• ∀x≥0.(x=0 ∨ x⋗0) : tout réel positif au sens large est soit nul soit n'est pas négatif au sens large.
• ∀x∈ℝ.(x⋗0 ∨ x≤0) : tout réel soit n'est pas négatif au sens large soit est négatif au sens large.

Démonstration : Pour voir que la première formulation implique la seconde, on l'applique successivement à 0⊔x et 0⊔(−x) : d'abord, comme x<0 implique 0⊔x > 0 donc 0⊔x ⋕ 0, on en déduit que 0⊔x = 0 implique x≤0, et symétriquement 0⊔(−x) = 0 implique x≥0 ; ensuite, comme x≤0 implique 0⊔x = 0, on en déduit que ¬(0⊔x = 0) implique x⋗0, et symétriquement ¬(0⊔(−x) = 0) implique x⋖0 ; en mettant tout ça ensemble, on a l'implication souhaitée. Tout le reste est complètement analogue à la proposition précédente. ∎

☞ Reformulations de MP analytique

Proposition : MP analytique admet les équivalents suivants :

• ∀x∈ℝ.((¬(x=0)) ⇒ (x⋕0)) : tout réel qui n'est pas nul est discerné de zéro (et bien sûr, la réciproque vaut trivialement).
• ∀x∈ℝ.((x⋗0) ⇒ (x>0)) : tout réel qui n'est pas négatif au sens large est strictement positif (et bien sûr, la réciproque vaut trivialement).

Démonstration : Le premier, qui est ma formulation de référence, implique à peu près trivialement le second ; et pour l'autre sens on applique le second à |x|. ∎

☞ Reformulations de LLPO et WLLPO analytiques

Avant de passer à LLPO, je vais avoir besoin du fait suivant, qui peut être utile en lui-même :

Lemme : Si H := {(x,y)∈ℝ² : x≥0 ∧ y≥0 ∧ ¬(x>0 ∧ y>0)} désigne l'ensemble des couples de réels positifs au sens large et qui ne sont pas tous les deux strictement positifs, alors la fonction H→ℝ donnée par (x,y) ↦ x−y, et la fonction ℝ→H donnée par z ↦ (z₊,z₋) := (0⊔z, 0⊔(−z)), sont des bijections réciproques.

Démonstration : Appelons f:H→ℝ donnée par (x,y) ↦ x−y, et d'autre part g:ℝ→ℝ² donnée par z ↦ (0⊔z, 0⊔(−z)). D'abord, l'image de g est bien dans H : en effet, 0⊔t≥0 pour n'importe quel t, et d'autre part on a vu que 0⊔t > 0 équivaut à 0>0 (impossible !) ou bien t>0, c'est-à-dire juste à t>0, et on ne peut pas avoir simultanément z>0 et −z>0.

Ensuite, on a (0⊔z) − (0⊔(−z)) = (0⊔z) − (z⊔0) + z = z en utilisant pour la première égalité le fait que (x⊔y)+t = (x+t) ⊔ (y+t) (qui découle de l'invariance par translation de l'ordre). Ceci montre que f∘g est l'identité sur ℝ.

Montrons enfin que g∘f est l'identité sur H : soient x,y deux réels positifs au sens large et qui ne sont pas tous les deux strictement positifs. Comme x≥0 et que x ≥ x−y, on a x ≥ 0⊔(x−y). On veut montrer l'inégalité de sens contraire : mais c'est la négation de x > 0⊔(x−y), donc il suffit d'arriver à une contradiction à partir de ça. Or x > 0⊔(x−y) équivaut à la conjonction de x>0 et de x > x−y, ce dernier étant équivalent à y>0 : et on a justement supposé que la conjonction de x>0 et de y>0 était absurde. Bref, on n'a pas x > 0⊔(x−y), c'est-à-dire qu'on a x ≤ 0⊔(x−y), et finalement x = 0⊔(x−y). Symétriquement y = 0⊔(x−y). On a bien montré que g∘f est l'identité sur H, et finalement que f et g sont des bijections réciproques. ∎

Proposition : LLPO analytique équivaut à l'affirmation :

• ∀x∈ℝ.(x≤0 ∨ x≥0) : tout réel est soit positif au sens large soit négatif au sens large.

Démonstration : Montrons que ma formulation de référence implique z≤0 ∨ z≥0 pour tout réel z (je change la lettre de x en z par rapport à l'énoncé, ce sera plus commode pour la preuve). D'après le lemme, les deux composantes du couple (x,y) := (0⊔z, 0⊔(−z)) sont positifs et ne sont pas simultanément strictement positifs (donc pas simultanément discernés de 0), donc la formulation de référence du LPO analytique montre que l'un des deux est nul, et comme le lemme assure aussi que z = x−y, on obtient z≤0 ou bien z≥y.

Réciproquement, montrons que l'affirmation que z≤0 ∨ z≥0 pour tout réel z implique la formulation de référence du LPO analytique. Si x,y sont deux réels qui ne sont pas simultanément discernés de 0, remplaçons les par |x| et |y| pour pouvoir les supposer positifs au sens large (donc pas simultanément strictement positifs) : le lemme assure que z := x−y permet de retrouver x,y par (x,y) = (0⊔z, 0⊔(−z)) ; du coup, si z≤0 ou z≥0 on obtient bien x=0 ou y=0. ∎

Proposition : WLLPO analytique équivaut aux affirmations :

• ∀x∈ℝ.((¬(x=0)) ⇒ (x≤0 ∨ x≥0)) : tout réel qui n'est pas nul est soit positif au sens large soit négatif au sens large.
• ∀x∈ℝ.((¬(x=0)) ⇒ (x⋖0 ∨ x⋗0))

Démonstration : Comme on a déjà remarqué que x⋗0 équivaut à la conjonction de x≥0 et ¬(x=0), les deux énoncés énumérés sont équivalents. La preuve de l'équivalence avec la formulation initiale est complètement analogue à la preuve précédente, et repose simplement sur le lemme, avec l'observation triviale supplémentaire que les bijections réciproques f et g mettent (0,0) en correspondance avec 0. ∎

[Optionnel] Un principe entre LLPO et WLLPO : MLLPO

☡ Guide de lecture : Cette section doit être considérée comme étant en petits caractères parce que c'est vraiment une digression, ou un développement sur un sujet que je n'avais pas anticipé : je suis tombé sur ce principe MLLPO en écrivant ce texte et en essayant d'avoir un parallélisme parfait entre principes séquentiels et analytiques d'omniscience, et en me rendant compte que quelque chose clochait. Si on n'est pas intéressé par ce développement, on peut le sauter.

Pour appliquer le lemme de manière à démontrer que ∀z∈ℝ.((¬(z=0)) ⇒ (z≤0 ∨ z≥0)) implique ma formulation de référence de WLLPO analytique, on a eu besoin de l'hypothèse que x,y ne sont pas tous les deux discernés de 0. Comme je l'ai démontré plus haut, cette hypothèse (que j'ai notée Ⓗ dans ce contexte) est gratuite dans le cas séquentiel, c'est-à-dire que WLLPO est équivalent qu'il soit formulé avec ou sans elle. Pour le cas analytique, en revanche, je soupçonne qu'elle n'est pas gratuite. Ceci amène à considérer l'énoncé analogue à WLLPO mais sans cette hypothèse, à savoir :

• donnés deux réels, s'il n'est pas vrai que tous les deux sont nuls, alors l'un des deux n'est pas nul, soit en symboles : ∀x∈ℝ.∀y∈ℝ.((¬((x=0) ∧ (y=0))) ⇒ ((¬(x=0)) ∨ (¬(y=0)))))

Je ne sais pas quel nom donner au principe ci-dessus : peut-être Mild Lesser Limited Principle of Omniscience ? appelons-le donc MLLPO analytique (ou MLLPO_ℝ, sachant que le MLLPO séquentiel est de toute façon pareil que WLLPO) pour les besoins de la discussion qui va suivre. Sous ces conditions, je peux au moins dire :

Proposition : LLPO_ℝ implique MLLPO_ℝ (défini ci-dessus), qui à son tour implique WLLPO_ℝ. Par ailleurs, MP_ℝ implique lui aussi MLLPO_ℝ.

Démonstration : Le fait que MLLPO analytique implique WLLPO analytique est logiquement trivial (ce dernier a une hypothèse de plus). Expliquons pourquoi LLPO analytique implique MLLPO analytique. Soient x,y deux réels dont il n'est pas vrai que tous les deux sont nuls, et on veut montrer que l'un d'entre eux n'est pas nul. Quitte à remplacer x,y par |x|,|y|, on peut supposer sans perte de généralité que x,y sont positifs au sens large. Comme on l'a vu, LLPO analytique (qu'on suppose) équivaut à l'énoncé que tout réel est positif ou négatif au sens large : en appliquant ce fait à x−y, on a soit x≥y≥0 soit y≥x≥0. Dans le premier cas, x=0 est impossible car il entraîne y=0 alors qu'il n'est pas vrai que x=y=0 : on a donc prouvé ¬(x=0). Le second cas est analogue et aboutit à la conclusion ¬(y=0).

La démonstration du fait que MP analytique implique MLLPO analytique est extrêmement semblable. Soient x,y deux réels dont il n'est pas vrai que tous les deux sont nuls, et on veut montrer que l'un d'entre eux n'est pas nul. Quitte à remplacer x,y par |x|,|y|, on peut supposer sans perte de généralité que x,y sont positifs au sens large. Comme on l'a vu, MP analytique (qu'on suppose) équivaut à l'énoncé que tout réel positif au sens large et non-nul est strictement positif : en appliquant ce fait à x+y, vu que x+y=0 est impossible (car cela entraînerait x=y=0, qui n'est pas vrai), on a x+y>0. Par (❀), on a lors soit x>0 soit x<x+y, ce second cas étant équivalent à y>0. On a donc prouvé x>0 ou y>0, et à plus forte raison ¬(x=0) ou ¬(y=0). ∎

En commençant à rédiger ce bout de ce texte, je pensais que MLLPO_ℝ serait équivalent à WLLPO_ℝ (i.e., je pensais juste avoir deux formulations équivalentes de WLLPO dans le cas analytique comme il y en a deux dans le cas séquentiel. Je me suis rendu compte que je n'arrivais pas à démontrer leur équivalence, et je soupçonne maintenant que les deux implications ci-dessus sont strictes en général. Mais je n'y ai pas vraiment réfléchi (de toute façon, rien dans ce billet ne donne les outils pour construire des contre-modèles permettant de montrer que tel ou tel énoncé n'en implique pas un autre) : peut-être bien que WLLPO_ℝ et MLLPO_ℝ sont en fait équivalents et que toute cette section est sans objet. Je remarque cependant que LLPO_ℝ et MLLPO_ℝ semblent porter en eux une forme de Choix (au sens où la disjonction dans la conclusion n'est pas exclusive), alors que WLLPO_ℝ ne l'a pas (la conclusion est une disjonction exclusive).

Je finis cette digresson par une observation qui peut justifier l'intérêt porté à MLLPO :

Observation : MLLPO_ℝ équivaut à l'affirmation que la non-égalité sur les réels est cotransitive (ou ce qui revient au même, est un discernement) : ∀x∈ℝ.∀y∈ℝ.∀z∈ℝ.((¬(x=z)) ⇒ ((¬(x=y)) ∨ (¬(y=z)))).

Démonstration : Montrons d'abord que MLLPO analytique implique la cotransitivité de la non-égalité : on veut donc prouver (¬(x=y)) ∨ (¬(y=z)) sous l'hypothèse ¬(x=z). Or les réels x−y et y−z ne peuvent pas être tous les deux nuls sous cette hypothèse (car leur somme x−z n'est pas nulle) : alors MLLPO analytique (qu'on suppose) entraîne que l'un des deux n'est pas nul, ce qui signifie bien (¬(x=y)) ∨ (¬(y=z)).

Réciproquement, supposons la cotransitivité de la non-égalité, et soient x,y deux réels dont il n'est pas vrai que tous les deux sont nuls, et on veut montrer que l'un d'entre eux n'est pas nul. Quitte à remplacer x,y par |x|,|y|, on peut supposer sans perte de généralité que x,y sont positifs au sens large. Maintenant, x+y=0 entraîne x=y=0, ce qui n'est pas le cas : c'est-à-dire qu'on a ¬(x+y=0), et la cotransitivité assure donc ¬(x+y=y) ou bien ¬(y=0). Le premier cas est équivalent à ¬(x=0), et on a bien la conclusion recherchée. ∎

[Optionnel] Le principe de Markov faible

☡ Guide de lecture : Là aussi, toute cette section est moralement en petits caractères, et doit être considérée comme optionnelle : je n'avais pas vraiment prévu d'en parler, et je me suis un peu laissé entraîner par une sorte de scrupule à laisser ce pauvre principe de Markov faible abandonné sur le bord de la route.

☞ Équivalents de WMP séquentiel

L'idée du principe de Markov faible est, en quelque sorte, de prendre la conclusion de la cotransitivité de la non-égalité comme hypothèse pour affirmer un discernement.

Proposition : les affirmations suivantes sont équivalentes :

1. ∀u∈2^ℕ.((∀w∈2^ℕ.((¬(w=0)) ∨ (¬(w=u)))) ⇒ (u⋕0))
2. ∀u∈ℕ_∞.((∀w∈2^ℕ.((¬(w=0)) ∨ (¬(w=u)))) ⇒ (u⋕0))
3. ∀u∈ℕ_∞.((∀w∈ℕ_∞.((¬(w=0)) ∨ (¬(w=u)))) ⇒ (u⋕0))

— En revanche, le principe

4. ∀u∈2^ℕ.((∀w∈ℕ_∞.((¬(w=0)) ∨ (¬(w=u)))) ⇒ (u⋕0))

les implique toutes et équivaut au principe de Markov (séquentiel).

Démonstration : L'implication (1)⇒(2) est logiquement triviale. Montrons (2)⇒(3). Pour cela, on se donne u∈ℕ_∞ dont on suppose qu'il vérifie ∀w′∈ℕ_∞.((¬(w′=0)) ∨ (¬(w′=u))), et on souhaite (de manière à pouvoir appliquer (2)) prouver qu'il satisfait aussi ∀w∈2^ℕ.((¬(w=0)) ∨ (¬(w=u))). Or donné w∈2^ℕ, on définit comme précédemment la suite binaire croissante μ(w)∈ℕ_∞ dont le n-ième terme est le maximum des termes ≤n de la suite w. D'après notre hypothèse appliquée à w′ := μ(w), on a (¬(μ(w)=0)) ∨ (¬(μ(w)=u)). Mais comme w=0 entraîne μ(w)=0 et que w=u entraîne μ(w)=u (puisque μ(u)=u), et comme l'une de ces deux choses est exclue, on a (¬(w=0)) ∨ (¬(w=u)), comme voulu. Alors (2) donne la conclusion u⋕0 souhaitée. Ceci achève de prouver (2)⇒(3).

Montrons enfin (3)⇒(1). Pour cela, on se donne u∈2^ℕ dont on suppose qu'il vérifie ∀w′∈2^ℕ.((¬(w′=0)) ∨ (¬(w′=u))). On définit μ(u) comme au paragraphe précédent, et on veut lui appliquer (3). Pour ça, on souhaite prouver ∀w∈ℕ_∞.((¬(w=0)) ∨ (¬(w=μ(u)))). Donné un w∈ℕ_∞ (vu comme une suite binaire croissante), on définit w′ := w ⊓ u, c'est-à-dire la suite dont le n-ième terme est le minimum entre les termes correspondants de w et u. Notre hypothèse assure que (¬(w′=0)) ∨ (¬(w′=u)). Or w=0 entraîne w′=0, et w=μ(u) entraîne w′=u (vu que μ(u) est en chaque point supérieur ou égal à u) : comme l'une de ces deux choses est exclue, on a donc (¬(w=0)) ∨ (¬(w=μ(u))), ce qui permet bien d'appliquer (3) à μ(u) pour conclure μ(u)⋕0, qui équivaut à u⋕0. Ceci achève de prouver (3)⇒(1).

Le fait que (4)⇒(1) est logiquement trivial. Prouvons enfin l'équivalence (MP)⇔(4). L'implication (MP)⇒(4) est logiquement triviale (appliquer l'hypothèse de (4) à w=0). Reste donc à prouver (4)⇒(MP). Soit donc v∈2^ℕ dont on suppose qu'il vérifie ¬(v=0), et on souhaite montrer qu'il vérifie v⋕0. Appelons u la suite obtenue en intercalant des 0 et termes de v (c'est-à-dire, disons, u_2i=v_i et u_2i+1=0). On va montrer que u vérifie ∀w∈ℕ_∞.((¬(w=0)) ∨ (¬(w=u))) de manière à pouvoir appliquer (4). Or w=u entraîne que la moitié des termes de w sont nuls, si bien que w=0 (c'est-à-dire ∞) puisque w∈ℕ_∞, et du coup u=0 ; mais comme on a supposé ¬(v=0), on a ¬(u=0), c'est-à-dire que w=u entraîne une absurdité : on a donc prouvé ¬(w=u), et a fortiori (¬(w=0)) ∨ (¬(w=u)), pour tout w∈ℕ_∞. Ceci nous permet d'appliquer (4) et de conclure u⋕0, qui entraîne évidemment v⋕0. Ceci achève de prouver (4)⇒(MP). ∎

Les énoncés équivalents (1)–(3) de la proposition ci-dessus portent le nom de principe de Markov faible (séquentiel) ou WMP (séquentiel).

☞ Le lien entre MP et WMP séquentiels

Proposition : MP séquentiel équivaut à la conjonction de WLLPO séquentiel et de WMP séquentiel.

Démonstration : Rappelons pourquoi MP implique WLLPO : si u,v sont deux suites binaires et s'il n'est pas vrai que toutes les deux sont nulles, alors la suite w obtenue en entrelaçant les termes de u et v n'est pas nulle, donc par MP elle a un terme non-nul, ce qui montre que l'une des deux suites de départ a un terme non-nul : on a donc montré WLLPO. Pour ce qui est du fait que MP implique WMP, il suffit d'appliquer l'hypothèse ∀w∈2^ℕ.((¬(w=0)) ∨ (¬(w=u))) de WMP à w=0 pour obtenir ¬(u=0), c'est-à-dire que l'hypothèse de WMP est plus forte que celle de MP, et ils ont la même conclusion, donc (MP)⇒(WMP).

Dans l'autre sens, si on a à la fois WLLPO et WMP, on veut montrer MP. Or WLLPO entraîne la cotransitivité de la non-égalité sur 2^ℕ (on l'a déjà vu au billet précédent) : donc si ¬(u=0), pour tout w on a (¬(w=0)) ∨ (¬(w=u)), ce qui est exactement l'hypothèse demandée par WMP et qui permet de conclure u⋕0. ∎

☞ Équivalents de WMP analytique

Passons maintenant à la variante analytique de WMP.

Proposition : Les affirmations suivantes sont équivalentes (où je rappelle que a⋗b signifie ¬(a≤b), ou, ce qui revient au même, a≥b et ¬(a=b)) :

1. ∀x∈ℝ.((∀t∈ℝ.((¬(t=0)) ∨ (¬(t=x)))) ⇒ (x⋕0))
2. ∀x∈ℝ.((∀t∈ℝ.(t⋗0 ∨ x⋗t)) ⇒ (x>0))
3. ∀x≥0.((∀t∈ℝ.(t⋗0 ∨ x⋗t)) ⇒ (x>0))
4. ∀x≥0.((∀t≥0.(t⋗0 ∨ x⋗t)) ⇒ (x>0))

Démonstration : Montrons que (1)⇒(2). Supposons donc d'un réel x qu'il vérifie ∀t∈ℝ.(t⋗0 ∨ x⋗t) et on souhaite montrer x>0. En appliquant l'hypothèse à t=0, on obtient x⋗0 et en particulier x≥0. On souhaite montrer que x vérifie ∀t∈ℝ.((¬(t=0)) ∨ (¬(t=x))) pour pouvoir appliquer (1) ; soit donc t∈ℝ arbitraire. Notre hypothèse assure t⋗0 ∨ x⋗t. Or t=0 entraîne t≤0, et t=x entraîne x≤t ; comme l'une de ces deux choses est exclue, on a on a donc bien montré (¬(t=0)) ∨ (¬(t=x)), comme voulu. Alors (1) donne x⋕0. Comme on a montré à la fois x≥0 et x⋕0, on a bien x>0, comme souhaité.

Le fait que (2)⇒(3) est logiquement trivial. Montrons que (3)⇒(4). Supposons donc d'un réel x≥0 qu'il vérifie ∀t′≥0.(t′⋗0 ∨ x⋗t′) et on souhaite montrer x>0. On souhaite (de manière à pouvoir appliquer (3)) prouver que x vérifie ∀t∈ℝ.(t⋗0 ∨ x⋗t) : soit donc t∈ℝ arbitraire. Posons t′ := 0⊔t (il est bien ≥0). Notre hypothèse assure t′⋗0 ∨ x⋗t′. Or t≤0 entraîne t′≤0 (même t′=0 mais peu importe), et x≤t entraîne x≤t′, et comme l'une de ces deux choses est exclue, on a t⋗0 ∨ x⋗t, comme voulu. Alors (3) donne la conclusion x>0 souhaitée.

Montrons enfin que (4)⇒(1). Supposons donc d'un réel x qu'il vérifie ∀t′∈ℝ.((¬(t′=0)) ∨ (¬(t′=x))) et on souhaite montrer x⋕0. Appliquons d'abord notre hypothèse à t′ := 0⊔x : on a (¬(t′=0)) ∨ (¬(t′=x)). Comme x≤0 entraîne t′=0, et x≥0 implique t′=x, et comme l'une de ces deux choses est exclue, on a x⋖0 ∨ x⋗0. On va raisonner dans chacun des deux cas x⋖0 et x⋗0. Commençons par nous placer dans le cas x⋗0, qui entraîne notamment x≥0. On souhaite (de manière à pouvoir appliquer (4)) prouver que x vérifie ∀t≥0.(t⋗0 ∨ x⋗t). Soit donc t≥0 quelconque. Posons t′ := x⊓t : d'après notre hypothèse, on a (¬(t′=0)) ∨ (¬(t′=x)). Or t≤0 (c'est-à-dire en fait t=0) entraîne t′=0 (car on a x≥0), et t≥x entraîne t′=x : l'une de ces deux choses étant exclue, on a donc t⋗0 ∨ x⋗t. Par (4), on en déduit x>0, et en particulier x⋕0. Dans le cas x⋖0, on raisonne de façon analogue sur −x (qui est ≥0), pour arriver à la même conclusion. Ceci achève la preuve de notre implication. ∎

Les énoncés équivalents de la proposition ci-dessus portent le nom de principe de Markov faible analytique ou WMP analytique (qu'on peut bien sûr noter : WMP_ℝ).

☞ Le lien entre MP et WMP analytiques

Proposition : MP_ℝ équivaut à la conjonction de MLLPO_ℝ (c'est-à-dire : ∀x∈ℝ.∀y∈ℝ.((¬((x=0) ∧ (y=0))) ⇒ ((¬(x=0)) ∨ (¬(y=0)))))) et de WMP_ℝ.

Démonstration : Rappelons pourquoi MP analytique implique MLLPO analytique : si x,y sont deux réels et s'il n'est pas vrai que tous les deux sont nuls, alors z := |x| ⊓ |y| n'est pas nul (car clairement z=0 entraîne x=y=0), donc z⋕0 par MP analytique, c'est-à-dire z>0, ce qui équivaut à |x|>0 ∨ |y|>0 soit x⋕0 ∨ y⋕0, et en particulier (¬(x=0)) ∨ (¬(y=0)). On a donc bien montré MLLPO analytique.

Toutes les autres parties de la preuve se démontrent de façon analogue mutatis mutandis, au cas séquentiel : je rappelle qu'on a vu plus haut que MLLPO analytique équivaut à la cotransitivité de la non-égalité sur ℝ. ∎

☞ Le lien entre WMP analytique et WMP séquentiel

Pour relier la version analytique avec la version séquentielle de WMP, on a besoin d'un raffinement d'un résultat déjà vu :

Lemme : En supposant l'axiome du choix dénombrable, si 0≤x≤1 est un réel compris entre 0 et 1 au sens large, il existe une suite binaire croissante b∈ℕ_∞ telle que :

• on a b⋕0 si et seulement si x>0 (et en particulier, on a b=0 si et seulement si x=0) ;
• si x=2^−u pour u∈ℕ_∞, alors b=u ;
• et dans tous les cas, x ≤ 2^−b.

(Intuitivement, on va définir b_i comme prenant la valeur 0 si x ≤ (5/8)×2⁻ⁱ, la valeur 1 si x ≥ (7/8)×2⁻ⁱ, et un choix arbitraire entre les deux ; mais il faut rédiger soigneusement, et utiliser le choix dénombrable, pour expliquer que ceci a bien un sens.)

Démonstration : Pour chaque i∈ℕ, comme 5×2⁻⁽ⁱ⁺³⁾ < 7×2⁻⁽ⁱ⁺³⁾, d'après (❀), on a soit x < 7×2⁻⁽ⁱ⁺³⁾, soit x > 5×2⁻⁽ⁱ⁺³⁾. Si on veut, cela équivaut à dire que la partie B_i de {0,1} contenant 0 si x < 7×2⁻⁽ⁱ⁺³⁾, et 1 si x > 5×2⁻⁽ⁱ⁺³⁾, est habitée pour chaque i. L'axiome du choix dénombrable permet de choisir un élément b_i de chaque B_i : on a alors, pour chaque i :

• b_i=0 ⇒ x < 7×2⁻⁽ⁱ⁺³⁾
• b_i=1 ⇒ x > 5×2⁻⁽ⁱ⁺³⁾

Il s'ensuit, par contraposées (même en logique intuitionniste, p⇒q entraîne (¬q)⇒(¬p)) :

• x ≤ 5×2⁻⁽ⁱ⁺³⁾ ⇒ b_i=0
• x ≥ 7×2⁻⁽ⁱ⁺³⁾ ⇒ b_i=1

La suite (b_i) est croissante, car b_i=1 implique x > 5×2⁻⁽ⁱ⁺³⁾ qui implique x ≥ 7×2⁻⁽ⁱ⁺⁴⁾ (vu que 5 > 7/2) qui implique b_i+1=1. On a donc bien défini un élément de ℕ_∞.

Si b⋕0, c'est-à-dire s'il existe i tel que b_i=1, alors x > 5×2⁻⁽ⁱ⁺³⁾ et en particulier x>0. Réciproquement, si x>0, par densité de ℚ dans ℝ il existe i tel que x ≥ 7×2⁻⁽ⁱ⁺³⁾, ce qui entraîne b_i=1, et en particulier b⋕0.

Ensuite, si x=2^−u, on veut montrer que b_i=u_i pour tout i. En notant abusivement u−i la suite obtenue en décalant de i crans la suite u (en supprimant les i premiers termes et en numérotant les suivants), on a 2^−u ≥ 7×2⁻⁽ⁱ⁺³⁾ si et seulement si 2^−(u−i) ≥ 7/8, et par ailleurs 2^−u ≤ 5×2⁻⁽ⁱ⁺³⁾ si et seulement si 2^−(u−i) ≤ 5/8. Mais un 2^−v pour v∈ℕ_∞ est soit =1 soit ≤ 1/2 selon que v₀ vaut 1 ou 0 : en appliquant ce fait à u−i, on voit que si u_i=1 on a 2^−(u−i) ≥ 7/8 donc b_i=1 et que si u_i=0 on a 2^−(u−i) ≤ 5/8 donc b_i=0. Bref, b_i=u_i comme annoncé.

Enfin, il reste à montrer que x ≤ 2^−b dans tous les cas. Comme 2^−b est la borne inférieure (qui existe !) de 1 et des 2⁻ⁱ pour les i tels que b_i=0, il s'agit de prouver x ≤ 2⁻ⁱ pour tout i tel que b_i=0. Or on a vu ci-dessus que b_i=0 entraîne x < (7/8)×2⁻ⁱ, ce qui entraîne bien ce qu'on a dit. ∎

Proposition : En supposant l'axiome du choix dénombrable, WMP séquentiel est équivalent à WMP analytique.

Démonstration : (Toute la démonstration suppose l'axiome du choix dénombrable.) Montrons d'abord que WMP séquentiel, sous la forme ∀u∈ℕ_∞.((∀w∈ℕ_∞.((¬(w=0)) ∨ (¬(w=u)))) ⇒ (u⋕0)), implique WMP analytique, sous la forme ∀x≥0.((∀t≥0.(t⋗0 ∨ x⋗t)) ⇒ (x>0)). Soit x≥0 dont on suppose qu'il vérifie ∀t≥0.(t⋗0 ∨ x⋗t), et on veut montrer x>0. Rappelons tout d'abord que d'après (❀) on a soit x>0 soit x<1 : le premier cas est exactement notre conclusion souhaitée, donc on peut se placer dans le second. Soit b∈ℕ_∞ une suite binaire croissante telle que donnée par le lemme appliqué à x (qui est bien au sens large entre 0 et 1) : comme x>0 équivaut à x⋕0 (car on suppose x≥0), et que x⋕0 équivaut à b⋕0 (d'après le lemme), il nous suffit de montrer cette dernière affirmation. D'après notre formulation de WMP séquentiel (qu'on suppose), il suffit de montrer ∀w∈ℕ_∞.((¬(w=0)) ∨ (¬(w=b))) pour pouvoir conclure. Soit donc w∈ℕ_∞, et considérons le réel t := x ⊓ 2^−w : d'une part, w=0 (qui, rappelons, est la même chose que ∞ dans ℕ_∞) entraîne t=0 donc t≤0, et d'autre part w=b entraîne 2^−w = 2^−b ≥ x (d'après le lemme), donc t=x donc x≤t ; l'une de ces deux choses étant exclue, on a donc (¬(w=0)) ∨ (¬(w=b)), comme on voulait, ce qui conclut notre preuve.

Dans l'autre sens, montrons que WMP analytique, sous la forme ∀x≥0.((∀t≥0.(t⋗0 ∨ x⋗t)) ⇒ (x>0)), implique WMP séquentiel, sous la forme ∀u∈ℕ_∞.((∀w∈ℕ_∞.((¬(w=0)) ∨ (¬(w=u)))) ⇒ (u⋕0)). Soit u∈ℕ_∞ dont on suppose qu'il vérifie ∀w∈ℕ_∞.((¬(w=0)) ∨ (¬(w=u))), et on veut montrer u⋕0. Posons x := 2^−u : on a 0≤x≤1 ; et comme u⋕0 équivaut à x⋕0 qui est impliqué par x>0, il nous suffit de montrer cette dernière affirmation. D'après notre formulation de WMP analytique (qu'on suppose), il suffit de montrer ∀t≥0.(t⋗0 ∨ x⋗t). Soit donc t≥0, appelons y := t⊓x, et soit w∈ℕ_∞ une suite binaire croissante telle que donnée par le lemme appliqué à ce y (qui est bien au sens large entre 0 et 1). Alors t≤0 (c'est-à-dire en fait t=0) entraîne y=0 donc w=0 ; et d'autre part, x≤t entraîne y=x donc y = 2^−u, donc (d'après le lemme) w=u ; l'une de ces deux choses étant exclue, on a donc bien t⋗0 ∨ x⋗t, comme on voulait, ce qui conclut notre preuve. ∎

À cause de l'apparition d'un quantificateur dans l'hypothèse, ce qui nécessite une « conversion » dans les deux sens, il semble qu'on ait besoin de l'axiome du choix dénombrable pour chacune des deux implications (à la différence de tous les autres principes d'omniscience que j'ai énoncés, pour lesquels la version analytique entraînait toujours la version séquentielle). J'ignore si cette utilisation de l'axiome du choix dénombrable dans les deux sens est vraiment essentielle.

☞ La méta-recette de cette section

Méta-recette : Beaucoup des démonstrations de la section qui précède sont plus ou moins du type WMP_S ⇒ WMP_T où, si S est un ensemble muni d'un élément distingué ‘0’ et d'une relation de discernement ‘⋕’, l'affirmation WMP_S est la suivante : ∀u∈S.((∀w∈S.((¬(w=0)) ∨ (¬(w=u)))) ⇒ (u⋕0)). Si on analyse un peu le mécanisme de preuve qui a été utilisé, il est essentiellement le même (à de toutes petites variations) à chaque fois, et il prouve en fait que les hypothèses suivantes permettent de conclure WMP_S ⇒ WMP_T : ⓐ on se donne fonction ou même une multifonction φ:T⇉S (une multifonction est une relation dont la première projection surjecte l'ensemble de départ), ⓑ on se donne une fonction ou même une multifonction ψ:T×S⇉T, ⓒ on a ψ(x,0)=0 pour x∈T, ⓓ on a ψ(x,φ(x))=x pour x∈T, et ⓔ φ(x)⋕0 implique x⋕0. Voici le schéma général de preuve. On suppose WMP_S et on veut prouver WMP_T. Pour cela, on se donne x∈T dont on suppose qu'il vérifie ∀t∈T.((¬(t=0)) ∨ (¬(t=x))). Par ⓐ, on considère u := φ(x) (ceci voulant dire, une valeur quelconque de la multifonction) et on souhaite (de manière à pouvoir appliquer WMP_S) prouver qu'il satisfait ∀w∈S.((¬(w=0)) ∨ (¬(w=u))). Or donné w∈S, par ⓑ, on considère t := ψ(x,w). D'après notre hypothèse appliquée à t, on a (¬(t=0)) ∨ (¬(t=x)). Mais comme w=0 entraîne t=0 par ⓒ, et que w=u entraîne t=x par ⓓ, et comme l'une de ces deux choses est exclue, on a (¬(w=0)) ∨ (¬(w=u)), comme voulu. Alors WMP_S donne la conclusion u⋕0 souhaitée. Par ⓔ, on en déduit w⋕0. On a ainsi bien prouvé WMP_T. ∎