Inconsistance de ZF, avis des spécialistes ?

Je réponds plus longuement :

@Foys : D'accord, mais parfois, Christophe dit (Christophe, corrige-moi si je me trompe) que la théorie des ensembles (en tant que spécialité de recherche), c'est la recherche de démonstrations de $0=1$. Ce que j'en ai compris, c'est que les démonstrations recherchées par la plupart des mathématiciens (non théoriciens des ensembles), comme elles concernent des objets tout petits, ont très peu de chance d'égratigner la consistance de ZF (et je crois que Christophe disait que vu que l'inconsistance de ZF serait une découverte scientifique très importante, les maths "normales" sont une perte de temps et qu'il faut concentrer ses efforts sur la théorie des ensembles qui, seule, trouvera la contradiction s'il y en a une), et je suis plutôt d'accord. Est-ce à ça que tu penses quand tu dis qu'il ne faut pas financer la recherche de démonstrations $ZF \vdash 0=1$ ?

@ev : Merci ! Les physiciens ne méritent pas le respect des gens qui bossent.

@Max : Ok pour cohérente, je voulais dire "est-ce qu'il y a une démonstration de $0=1$". Pour ton 2-, ah oui ? Pour ton 3-, Christophe a dit une fois qu'il a mangé avec Woodin, et Martial doit avoir plein de contacts avec cette communauté, je pense !

@Foys et Max : Ah, oui, vous pariez sur "cohérente" ? Je n'aurais pas pensé ça de vous ! Mon "objection" immédiate est : "non mais vous trouvez pas ça fou, qu'on ait réussi à cohérer la théorie des ensembles à la première réparation (après l'apparition du paradoxe de Russell et en introduisant la compréhension restreinte) ?", mais vous avez probablement quelque chose d'évident que je ne vois pas à répondre, non ?

@Christophe : Toi, d'ailleurs, tu n'avais pas dit une fois que tu pensais Peano inconsistante ?

Enfin, pour cette histoire de démonstrations de $0=1$ infiniment longues, il faut que je réécrive ce que je voulais dire, parce que je n'y croyais pas moi-même, je simulais le "parler-logique".

Soit $P_\mathbb{N}$ l'énoncé qui dit "je suis l'ensemble des entiers naturels", c'est-à-dire, je contiens $\emptyset$ et je suis un sous-ensemble de tout ensemble qui contient $\emptyset$ et qui est stable par successeur ; de même, on définit $EstNaturel$ l'énoncé qui dit "je suis dans tout ensemble qui vérifie $P_\mathbb{N}$".

Ensuite, je fixe un codage de Gödel des formules, et on a le $Dem(n,m)$ qui est l'énoncé qui dit "$n$ est le nombre de Gödel d'une démonstration de l'énoncé dont le nombre de Gödel est $m$", et je note $\bot$ le nombre de Gödel de $\emptyset = \{\emptyset\}$.

Enfin, je note $ConsZF$ l'énoncé $\forall N,\ \forall n,\quad (P_\mathbb{N}(N)\text{ et } n\in N) \Rightarrow \neg Dem(n,\bot)$.

Alors : soit $ZF$ démontre $ConsZF$, auquel cas il démontre aussi, d'après le théorème de Gödel, $\neg ConsZF$.

Soit $ZF$ ne démontre pas $ConsZF$, auquel cas il démontre $\exists (M,e),\quad EstUnModeleDeZF(M,e) \text{ et } (M,e) \models \neg ConsZF$, et il démontre alors qu'il existe un modèle de $ZF$ qui voit un entier à lui comme étant une démonstration de $\bot$ ; mais ce truc, que lui voit entier, nous, qui sommes à l'extérieur de $M$, ne le voyons pas comme entier.

Bref, Christophe, pourquoi dis-tu que la question n'a pas de sens formel ? Si un jour, quelqu'un se ramène avec une démonstration écrite sur une feuille, dont toutes les hypothèses sont des théorèmes de $ZF$, que $0=1$, alors cela aura bien un sens de dire "$ZF$ est incohérente", non ?