Construction de $\mathbb{R}$ et AC

Salut,
Attention à la distinction entre : "tout nombre réel donné possède une suite de Cauchy qui le représente" et "il existe une famille $(a_x)_{x\in\Bbb R}$ telle que, pour tout $x\in\Bbb R$, $a_x$ est une suite de Cauchy qui représente $x$". Dans la première proposition, on ne trouve une suite de Cauchy que pour un réel donné, alors que dans la deuxième on trouve des suites pour tous les réels à la fois. On n'a besoin de AC que dans la deuxième affirmation. La première affirmation est tautologique dans la construction de $\Bbb R$ que tu donnes.

Tu confonds deux choses. Là où tu as besoin de AC c'est pour fabriquer ce qu'on appelle un ensemble transverse, ce que tu appelles toi un système de représentants. Je te donne un exemple simple : considérons la relation $E_0$ définie sur $\mathbb{R}$ par $x E_0 y \Leftrightarrow x-y \in \mathbb{Q}$. AC est nécessaire pour prouver l'existence d'un ensemble qui rencontre chaque classe d'équivalence en un point et un seul.

En revanche, un réel est défini comme un ensemble de suites de Cauchy, donc il est représenté par $2^{\aleph_0}$ suites, et tu peux en choisir une comme tu le veux : c'est le principe du choix fini, qui est un théorème de ZFC. Il revient à ce qu'on appelle le TAC (Trivial Axiom of Choice) : "tout ensemble non vide a au moins un élément", qui lui-même est équivalent à la règle du tiers exclu (qui est fausse en intuitionnisme, mais vraie en logique du 1er ordre).
D'ailleurs, si tu me donnes l'écriture décimale de $\sqrt{2}$ je te donne sans difficulté un représentant de la classe des suites des Cauchy qui convergent vers $\sqrt{2}$. Il me suffit d'écrire la suite des approximations à $10^{-n}$ près.

A mon avis la question que tu te poses est la suivante : j'ai tous les réels sous les yeux, et je voudrais écrire une liste $L$ de suites de Cauchy telle que pour chaque réel $x$, il existe une suite élément de $L$ et une seule qui converge vers $x$. Alors là, oui, tu as besoin de AC.

Il y a quand-même le développement binaire par défaut par exemple qui donne un représentant dans chaque classe d'équivalence, croissant qui plus est!

Homo Topi, toute bijection $\Bbb Q\to\Bbb N$ fournit un bon ordre sur $\Bbb Q$.

Il faut que je précise un peu ce que j'ai dit (en rapport avec ce qu'ont ajouté Palabra et Christophe) : si on veut montrer de façon naïve "il existe une famille $(a_x)_{x\in\Bbb R}$ telle que, pour tout $x\in\Bbb R$, $a_x$ est une suite de Cauchy qui représente $x$", on a besoin de AC. Mais si on est un peu plus malin, on trouve un moyen constructif d'associer à chaque $x$ une suite le représentant (cf. le premier message de Palabra) et on n'a alors plus besoin d’utiliser AC.

Bonjour,

Comme l'indique Maxtimax, étant donné la projection canonique $p:\mathcal{C}\to\R$, la classe $p(c)$, pour $c\in\mathcal{C}$, est naturellement habitée, vu que $c\in{}p(c)$.

Cependant, je ne comprends pas ce refus presque pathologique de AC (dans le système bourbakiste, il s'agit d'un théorème à part entière, au même titre que le théorème global du choix ; point de salut pour une mathématique constructiviste avec Bourbaki). Un jour, j'ai acheté le livre "Modules sur les anneaux commutatifs" de Diaz-Toca - Lombardi - Quitté. J'ai été vraiment globalement déçu. Le livre est mal engagé ; difficile de rédiger un ouvrage basé sur une mathématique constructiviste. Même constat avec Ageron, où j'attends encore le point de vue constructiviste. Mais tout cela n'est qu'un point de vue ; rien d'autre (et tout aussi biaisé que celui de ne pas vouloir tenir compte de AC).

Cordialement,

Titi

@Christophe : bien vu, le coup du bon ordre sur $\mathbb{Q}$ !

@HT : Tu as entièrement raison de faire ça ! Je suis un grand défenseur de AC, mais je suis pour que les gens disent quand ils l'utilisent ou pas. (Bon, évidemment, dans certains cas il faut le dire au début du papier, ou du livre).
Rien ne m'énerve plus que les gens qui utilisent AC pour démontrer Cantor-Bernstein, ou qui utilisent l'axiome de l'ultrafiltre pour démontrer Tychonoff, et qui ensuite ne s'en servent que dans le cas d'un produit fini de compacts.

@Max : oui, tu as raison, oeuf corse !

Thierry : beh c'est la construction par suites de Cauchy, qui est celle qu'on fait même en logique classique :-S bon, là il rajoute le fait qu'elle soit "explicitement" de Cauchy, mais c'est exactement la même chose !

Quant à "être certain que AC ne se cache pas derrière un raisonnement", la réponse est : regarde à chaque étape si tu utilises un résultat qui utilise AC. Pour ne pas faire d'erreur, je te répondrai : comment être certain que tu ne fais pas d'erreur, de manière générale ?

Ce genre de questionnements mène à l'informatisation des preuves, et la plupart des gens qui font ça s'intéressent au constructivisme; puisqu'il est beaucoup plus proche de la manière dont l'informatique marche.