L'axiome du choix et la consistance de ZF

On prouve que si ZF a un modèle, alors ZF + négation de AC a un modèle. Ça ne prouve en rien que ZF a un modèle.

À partir du moment où la consistance de ZF n'est pas démontrée (démontrée dans quel cadre, d'ailleurs ?), il n'est pas démontré non plus que ZF ne démontre pas AC.

On dit souvent, à tort, que AC n'est pas démontrable dans ZF (et que sa négation non plus). C'est un raccourci, le vrai énoncé est : "si ZF est consistante, alors ZF ne prouve ni AC, ni sa négation" (Gödel et Cohen).

Pour ta deuxième question, tu as fait la démonstration. Il suffit de voir que le faux implique tout énoncé.

C'est un sujet gradué, c'est à dire que les théories sont "de plus en plus fortes" sans qu'on sache si ne serait-ce que l'une d'entre elles est consistante (et ça commence à peu près à l'arithmétique de Peano). Donc comme il t'a été dit ci-dessus, c'est qu'on déconne un peu en prenant des raccourcis du genre "Ce truc ne peut pas être prouvé sans AC", etc. On est vraiment dans l'abus de langage au sens le plus brutal du terme :-D (enfin l'abus sémantique, il n'y a pas de torsion grammaticale)

Je ne comprends ce que tu entends pas "dépendent-ils". C'est ta croyance qui en ces théorèmes qui va plutôt en dépendre non? Au passage, précision tout se fait avec les ensembles, il n'y a pas de maths en dehors, les entiers sont des ensembles précis qui ont une définition, etc.

Evidemment, le jour où on trouvera une contradiction dans ZF, de nombreux théorèmes de maths verront leur preuve enregistrée à l'ACAD des sciences très intensément revisitées. Mais attention: seuls des fragments assez "modérés" de ZF sont utilisés.

Par exemple, complétude, compacité, sont "essentiellement évidents" à l'admission près d'axiomes parfaitement identifiés (le choix ultrafiltrant essentiellement) et quand les phrases varient dans un ensemble dénombrables, ils sont effectifs (une preuve de maths est un jeu, et ils énoncent que l'un des deux a une stratégie gagnante, mais en plus, la stratégie pour gagner en tant que prouveur est "constante"***** et trivial!!! C'est pour "gagner vite" qu'il y a du taf mais ce n'est pas dans l'énoncé de tes théorèmes ci-dessus). Je ne sais pas ce que tu appelles "lecture unique".

***** la voici: tu as supposé nonP (tu veux prouver P). A chaque étape, tu dis au sceptique "tu veux que je te prouve Q_n=>\perp ou Q, tu choisis quoi?" ('après ça, tu mettras soit Qn, soit nonQn dans les hypothèses) où $n\mapsto Q_n$ est une surjection de IN sur l'ensemble des phrases. A la fin, si tu n'as pas gagné en temps fini, ce que tu as c'est un modèle de nonP (par définition quasiment). Et si t'as gagné, bin t'as gagné, t'es content et tu n'as même pas réfléchi à ta manière de jouer. Cette présente preuve résistera, ne t'inquiète pas, même à la chute de Peano 2nd ordre (je ne te parle même pas de ZF) et d'ailleurs, je me retiens de dire même à la théorie vide franchement. Quant à la compacité c'est une version affaiblie de l'axiome du choix quasiment texto aussi, donc on "sait" que ce n'est pas là que la bas blesse (justement par ton présent fil et les réponses reçues)