AC et théorie des ensembles

Un détail m'échappe sur la formulation de la question. Si on a une assertion démontrable qui n'a pas été prouvée, alors on ne peut pas être sûr qu'elle est démontrable.

Par contre, oui, en ajoutant l'axiome du choix, on n'ajoute pas de contradiction.

En résumant la preuve, l'idée est la suivante (sans donner trop de détails dans les définitions).

Une partie $X$ d'un ensemble $Y$ est définissable s'il existe une formule logique (avec des paramètres dans $Y$) qui distingue les éléments de $X$.
On suppose qu'on a un modèle de ZF. On considère alors $L_0=\emptyset$, et $L_{\alpha+1}$ les parties définissables de $L_\alpha$, si $\alpha$ est un ordinal limite on pose $L_\alpha=\bigcup\limits_{\beta<\alpha} L_\beta$.
Enfin on regarde $L$ la réunion de tous les $L_\alpha$. On peut démontrer que $L$ marche comme ZF. Mais on a même mieux. Premièrement les ordinaux sont bien ordonnés, de plus l'ensemble des formules est bien ordonné. On peu alors construire un bon ordre sur $L_0,\ L_1,\ L_2$, etc. De plus on peut se débrouiller pour que le bon ordre sur $L_\alpha$ étende les bons ordres sur les $L_\beta$, pour $\beta<\alpha$.
Au final on se retrouve avec $L$ un modèle de ZF, mais on a en plus un bon ordre "naturel" sur $L$. On en déduit alors l'axiome du choix.

Bon j'ai un peu triché, en ne donnant pas précisément les définitions (ni la manière de mettre le bon ordre, etc.), mais ça devient assez technique.

La Théorie axiomatique des ensembles de Jean Louis Krivine, que l'on retrouve dans "Théorie des ensembles" aux éditions Cassini, est un excellent ouvrage, bien rédigé et clair.

Mpif et Christophe : Soyez plus clair dans vos propos. Les [méta]démonstrations de non-contradictions relatives ne sont pas aussi intuitives que çà et je sais bien, Christophe, que ce n'est pas ça que tu voulais dire. Cependant, O-b1 écrit : "[N]'ayant pas les ressources bibliographiques (et il faut le dire pas assez d'expérience en théorie des ensembles pour ces [méta]théorèmes), je ne pense pas me pencher sur les détails de ces démonstrations."

Pour conclure, les modélisations utilisées par K. Gödel et P. Cohen révèlent toutes les difficultés liées à la théorie des modèles.

A +