Bon ordre sur $\R$
Grâce à l'AC il existe un bon ordre sur R. Ce bon ordre est-il susceptible d'être découvert un jour ou y a-t-il une impossibilité conceptuelle. Je croyais avoir les idées claires sur ça mais bon, peu à peu le doute s'insinue en mon esprit et...
Bonne soirée.
Jean-Louis.
Bonne soirée.
Jean-Louis.
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
0- "Ce bon ordre" : attention, AC nous dit qu'il en existe un, mais à partir de là il en existe des tonnes et des tonnes. Toute permutation de $\R$ t'en fournit un autre, isomorphe, mais il en existe d'autres non isomorphes aussi. Donc on ne peut pas parler "du bon ordre" qu'on pourrait décrire ou pas.
1- Même si tu me sors une formule $R(x,y)$ telle que parfois, elle définit un bon ordre, tu ne pourras de toute façon pas le prouver sans AC (ou une forme faible, je veux dire : dans ZF)
2- On a tendance à dire "AC => inexplicite" ou "pas constructible"; mais c'est une idée reçue : l'univers constructible de Gödel, $\mathbb L$ satisfait AC.
3- Joel David Hamkins a répondu à cette question sur MathOverflow, la voici. Cela donne une formule qui, sous réserve de $V=\mathbb L$ (qui est strictement plus fort qu'AC), définit un bon ordre de $\R$. Elle n'est pas extrêmement complexe (JDH affirme, sans le prouver, que sa complexité est $\Delta^1_2$, c'est relativement bas)
4- Il serait intéressant de voir si on peut déterminer, sous AC, la complexité minimale d'une telle formule. Je pense que c'est quelque chose que les "descriptive set theorists" sauraient étudier.
Hélas, je n'arrive plus à l'écrire.
Bref, si ce truc est vrai ça prouve en particulier que $\mathbb{V}= \mathbb{L}$ entraîne l'existence d'un sous-ensemble $\mathbf{\Delta^1_2}$ de $\mathbb{R}^2$ qui n'est pas LM.
A prendre avec des pincettes...
@Max : je sais construire le bon ordre "canonique" de $\mathbb{L}$ (enfin, surtout quand j'ai mes notes sous les yeux), mais je ne sais pas démontrer que la trace sur $\mathbb{R}$ de ce bon ordre est $\mathbf{\Delta^1_2}$. Et pourtant, il fut une époque où je bouffai de la théorie descriptive dès le p'tit dej. C'est vraiment la honte !!!
Tu vois bien que si tu disposais d'un bon ordre sur $\mathscr P(\omega)$ tu finirais par y arriver.
Hélas...
P.S. : "Tout le monde sait bien" que $\mathscr P(\omega)$ c'est la même chose que $\mathbb{R}$.
2/ Comme vous le savez tous 2, $V=L$ dit que $\R=$ ensemble des réels constructibles
3/ "Etre constructible" est $[\exists \forall]$ (il existe un modèle dénombrable de $ZF+V=L$ et bien fondé (c'est là que le $\forall$ de droite apparaît) qui me contient)
4/ Les bons ordres qu'on peut donc définir se devinent comme étant de la même complexité, sachant qu'à l'image de ce qui se passe pour la dualité récursif/récursivement énumérable, quand on a trouvé qui est le plus petit, l'autre est plus grand et donc on peut même avoir une complexité du genre $[\exists \forall] \cap [\forall \exists]$ (qui est réputée mieux, plus simple, mais pour ce contexte, ça ne change pas grand chose).
5/ @JL : il n'y a donc pas de réponse à ta question qui soit "fixe". Ça dépend de l'univers. Dans certains univers le BO n'est pas plus complexe que l'ensemble des dérivables** ou des $C^\infty$, dans d'autres, il n'est même pas projectif.
** vue comme l'ensemble des points à coordonnées rationnelles dans leur épigraphe
http://www.numdam.org/article/BSMF_1905__33__261_1.pdf
Ils n'avaient pas de forums internet, mais ça ne les empêchait pas de débattre .....
Je ne connais pas trop les histoires d'univers constructible (la logique formelle et la théorie des ensembles, j'aime bien mais à faibles doses...) mais dans les mathématiques que j'ai faites, à chaque fois que j'ai vu une utilisation de l'axiome du choix, ça détruisait l'aspect constructif de la preuve. Je veux bien qu'on puisse faire une construction explicite d'un ensemble/d'une classe et démontrer que le truc satisfait l'axiome du choix, mais je vois mal (vu la formulation de AC) comment une utilisation de AC puisse ne pas être non constructive (vive les doubles négations).
Je ne serais pas contre un petit peu de culture mathématique si je me trompe sur ce que je raconte.
Le théorème de complétude de la logique du premier ordre est-il constructif? On ne connait pas vraiment de modèle de ZF ou de PA.
Ce théorème admet pourtant une preuve intuitionniste, trouvable sur le site de Jean-Louis Krivine.
Par exemple soit $\approx$ la relation d'équivalence définie sur $\mathbb R$ par
$x \approx y \Leftrightarrow x-y \in \mathbb Z$.
Pour trouver un représentant de chaque classe, on peut invoquer AC, ou trouver une réponse explicite (même si AC est valide).
PS : en remplaçant $\mathbb Z$ par $\mathbb Q$, sans AC on ne sait pas faire
Des fois, on n'en a pas besoin. Pour prendre un exemple tout simple, le théorème de Rolle : on sait qu'il existe un $c$ dans $]a;b[$ tel que $f'(c)=0$ sous les hypothèses du théorème, mais on ne sait pas exactement qui est $c$. Pas grave, on n'en a pratiquement jamais besoin. Dans la pratique, la fonction à laquelle on appliquerait le théorème est clairement identifiée, donc on peut peut-être identifier $c$ quand même, ou au pire, on l'approche avec une précision arbitraire avec des méthodes numériques. Avec Rolle, je suis dans la situation de "il existe $c$" mais juste avec le théorème en lui-même (sans faire de travail supplémentaire), je ne peux pas écrire $c=$ un élément spécifique de $\R$. Donc pour moi, Rolle est un théorème "non constructif". Note que je ne lui en veux pas pour ça, il sert déjà très bien pour faire de la théorie, et on ne lui en demande pas plus.
J'ai travaillé sur un document qui construisait "la" mesure de Haar sur un groupe topologique localement compact. On construisait explicitement l'ensemble dans lequel on allait appliquer le lemme de Zorn pour dire "il existe une mesure qui fait exactement ce dont on a besoin". Elle existe, on connait ses propriétés et ça suffit pour l'utilisation qu'on veut en faire, mais si c'est pour écrire $\mu(A)=\dots$ en fonction de la partie $A$, ça ne marche pas trop, parce qu'on ne sait pas qui exactement est la mesure. Ce n'est pas ce qui nous intéresse, donc ça ne pose aucun problème, mais c'est "non constructif".
Est-ce que "constructif" ou "non constructif" peut avoir un sens mathématique ? Oui. Faut-il rejeter le non constructif pour autant ? Certainement pas. En tout cas, c'est mon avis.
Avec $\Z$, un nombre va être représenté par sa partie décimale, donc on comprend que le quotient sera en correspondance avec $[0;1[$. Pour le démontrer proprement, là j'avoue ne pas avoir essayé de l'écrire, j'ose prétendre que ça se fait.
Avec $\Q$, sans passer plus de temps dessus je ne sais même pas à quoi ressemble le quotient, donc pour trouver à la main un système de représentants, je jette l'éponge pour l'instant. C'est bien trouvé comme exemple :-D
Je t'exhibe un ensemble de représentants de $\mathbb{R/Q}$ sous l'hypothèse que $V=L$ (voire que $\mathbb R\subset L$) : pour chaque classe, prendre le plus petit réel qui lui appartient, au sens du bon ordre global défini sur $L$.
Tout à fait constructif, non ?
Mais peut-être que ma définition de "constructif" est également restrictive... à voir si je suis trop exigeant.
Je ne sais pas trop si les matheux constructivistes ont la même définition que moi. En tout cas, je ne rejette pas purement et simplement les démonstrations "non constructives", mais je préfère les constructives quand c'est possible d'en avoir. Même si elles sont plus compliquées, je trouve qu'on y gagne quand même en général.
HT : l'exemple de la mesure de Haar n'est pas idéal puisqu'elle est unique à renormalisation près, donc si tu fixes un sous-ensemble mesurable de mesure non nulle et que tu décrètes que sa mesure vaut $1$, en principe pour tout autre $A$, $\mu(A)$ est entièrement déterminé (quoique peut-être difficile à calculer - mais si on commence à refuser les choses difficiles à calculer comme "non constructives", on commence à avoir des soucis)
@Tous : tout cela me rappelle ce qu'on appelle le théorème de prolongement de la dérivée.
Théorème : Soit $f$ une fonction continue sur $[a,b]$ et dérivable sur $]a,b]$. Si $\lim \limits_{x \to a^+} f'(x)=l$, alors $f$ est dérivable à droite en $a$ et $f'_d(a)=l$.
La preuve classique dit : soit $x \in ]a,b]$. Par le TAF il existe $c_x \in ]a,x[$ tel que $\dfrac{f(x)-f(a)}{x-a} = f'(c_x)$. Par gendarmes on a $\lim \limits_{x \to a^+} c_x = a$, puis par hypothèse et par composition de limites on a
$$\lim \limits_{x \to a^+} \dfrac{f(x)-f(a)}{x-a}=l$$, CQFD.
Problème : il y a pléthore de tels $c_x$, donc sans le faire exprès on utilise AC. Certes, on peut se ramener à AC-dénombrable en remplaçant $\varepsilon$ par $\dfrac{1}{n}$.
Mais quelqu'un connaît-il une preuve totalement AC-free ?
J'aime beaucoup l'exemple de Martial, il montre à quel point c'est facile d'utiliser AC sans s'en rendre compte et à quel point il est utile même en dehors de "la théorie des ensembles pour elle-même" (je sais qu'il y a des gens qui adorent la TDE).
Quand j'étais étudiant, un de mes profs nous racontait que l'axiome du choix avait été très froidement accueilli par la communauté mathématique (c'est sans doute pour ça qu'il en existe des formes faibles, pour essayer d'apaiser un maximum de mathématiciens non convaincus), notamment parce qu'il permettait de construire des ensembles non mesurables et que les gens n'aimaient pas ça du tout.
Mais plus tard, j'ai appris que l'axiome du choix était équivalent à "toute relation d'équivalence admet un système de représentants". Depuis, je trouve ça complètement fou de vouloir se priver de l'axiome du choix, pour des raisons purement algébriques : on construit tellement de choses en faisant des quotients que de se priver de systèmes de représentants serait un handicap majeur pour pouvoir écrire des choses. Cependant, je n'avais pas d'exemple en tête d'une utilisation "a priori anodine" de AC dans un contexte simple, et surtout, non algébrique/ensembliste.
Je préfère toujours pouvoir me passer de AC quand c'est possible, dans le sens, quand c'est possible de faire une construction explicite du truc pour lequel AC servirait de raccourci. Mais parfois, ce n'est pas possible, et je ne pense pas qu'il faille vouloir se priver exprès de l'axiome du choix. Non pas que j'accuse quelqu'un de faire ça ici, bien entendu.
En tout cas, merci Martial pour ton exemple avec le prolongement de la dérivée !
A la fin de la démonstration, le prof nous signale qu'on a utilisé l'axiome du choix dans ce passage, puis reprend la démonstration et contourne le problème, de manière similaire à ce que j'ai proposé pour l'exemple de Martial.
Mais je suis certain qu'on a utilisé AC plein de fois pendant mes études, sans nous le dire explicitement. Certainement en topologie, mesure, ou même dans certains résultats d'analyse (cf Martial). C'est tellement simple de dire "il existe" sans se rendre compte que c'est grâce à un AC que c'est vrai. En un sens, ça rend presque le rejet de AC ironique vu à quel point c'est naturel de dire "il y a un truc dans le bazar, on ne sait pas où il est, mais on sait qu'il est dedans, alors c'est bon".
PS : Tu devrais faire l'exercice que je te propose ci-dessus. Ce n'est pas un problème de dire "il existe", c'est plus subtil que ça.
Et j'ai un peu dit n'importe quoi. On utilisait AC pour montrer que tout EV admet une base, donc spécifiquement pour la dimension infinie... on avait besoin de ça pour je ne sais plus quel exercice, en rapport avec le PT. On ne s'en servait effectivement ni pour démontrer l'existence du PT. Peut-être pour établir sa propriété universelle, je ne sais honnêtement plus.
La correspondance de Curry-Howard ne dit pas autre chose.
Si parmi les énoncés en question se trouve un énoncé qui dit qu'il existe certaines fonctions, bah dans les conclusions vous pouvez vous retrouver avec l'existence d'autres fonctions.
Si tu trouves mon exemple peu probant, on peut revenir sur l'exercice donné par Poirot à Homo Topi (caractérisation de la continuité en termes de suites dans un espace métrique). Ma prof de sup avait fait cette démonstration, et bien sûr je n'y avais vu que du feu. (Bon, d'accord, là il y a vraiment besoin de AC-Den, mais c'est juste pour dire).
Même sans connaître AC, si un prof m'avais montré ça j'aurais sûrement cherché une autre preuve.
Quant à chercher une autre preuve, je ne sais pas de quelle génération tu es mais à mon époque (1975/76 en sup), ce n'était vraiment pas dans notre culture : on avait une confiance absolue dans le prof. D'ailleurs ça a aidé à mal façonner ma formation. Prépa : tu n'as guère le temps d'aller traîner tes guêtres dans une bibliothèque. Licence de maths après une M' : tu te balades littéralement, je me souviens qu'en fonctions analytiques il y avait des DMs facultatifs, je les faisais de tête. Ce n'est qu'en maîtrise, voire en prépa agreg, que j'ai commencé à fourrer mon nez dans les bouquins. Erreur grave !
En ce qui concerne la confiance absolue dans les profs, tout ce que je sais c'est que si pour moi la preuve était dégueulasse et ben elle était dégueulasse confiance ou pas. D'ailleurs j'avais du mal à continuer à suivre un cours si le prof n'était pas très rigoureux. En stats/proba j'en ai bavé par exemple.
Petit souvenir : En proba le prof avait dit sans le dire qu'on pouvait additionner, multiplier etc. les variables aléatoires et qu'on obtenait encore une v.a. à la fin. Ce truc sans preuve me dérangeait tellement que j'avais essayé de le prouver seul mais sans succès (bien que ce ne soit pas très difficile). À la fin j'avais posé la question à l'assistant de topologie je crois. Je lui ai écrit sur le tableau noir ma question avec mon début de preuve foireuse... il a pris l'éponge et a tout effacé en disant qu'il ne supportait pas les proba. :-D
Finalement j'ai trouvé la preuve dans un bouquin de la bibliothèque.