Comments on Deux remarques sur l'intuition du théorème de Gödel

Non, je préfère vraiment dire qu'un système formel est « consistant » plutôt que « cohérent » (cohérent, c'est pour les faisceaux), et tant pis (ou tant mieux, en fait) si c'est un anglicisme.

@ooten: Franck Wolff a bien raison : certes il y a une infinité d'axiomes de récurrence[#], mais chaque utilisation qu'on fait de la récurrence dans une démonstration donnée ne fait appel qu'à un nombre fini d'entre eux, et donc qu'à un nombre fini d'axiomes. (Tout simplement parce qu'une démonstration est finie : ce n'est tout simplement pas possible de faire appel à une infinité d'axiomes dans une seule démonstration.) C'est bien tout le cœur de l'argument.

(La seule exception c'est quand on démontre des « schémas de théorèmes », c'est-à-dire un modèle permettant de fabriquer des théorèmes, où là on utilisera potentiellement une infinité d'axiomes dans le schémas. Notamment l'affirmation que j'ai encadrée dans mon entrée. Mais si on imagine une démonstration d'une contradiction dans PA ou ZFC, elle utilise un nombre fini d'axiomes vu qu'il y a une seule conclusion.)

[#] Enfin, ça c'est dans PA, dans ZFC la récurrence s'écrit comme un seul énoncé, et ce sont d'autres axiomes (sélection et remplacement) qui sont des schémas infinis ; mais peu importe ici.

@Franck Wolff: Ben oui, c'est exactement ce que je dis…

@ooten: Oui, c'est tout à fait analogue : PA, ZFC, et ZFC + tel ou tel grand cardinal, sont des théories qui produisent des prédictions expérimentales, à savoir les choses testables sur les entiers de taille raisonnable. (Par exemple, « il n'existe pas de contradiction dans ZFC » est une prédiction expérimentale de ZFC + il existe un cardinal inaccessible. Et « il n'existe pas de solution non-triviale de x^n+y^n=z^n pour n>2 » en est une de ZFC et vraisemblablement PA.) Et on peut tester expérimentalement ces prédictions expérimentales.

En un certain sens, le fait qu'on ne trouve pas de contradiction dans ZFC peut être considéré comme une confirmation expérimentale de la théorie « ZFC + il existe un cardinal inaccessible » (après, la bizarrerie due au théorème de Gödel, c'est qu'à chaque fois, le fait de ne pas trouver de contradiction dans une théorie T pourra être considéré comme confirmation expérimentale d'une théorie T′ plus forte que T, mais que du coup, on a envie de croire que T′ est vraie, donc consistante, donc de postuler une théorie encore plus forte, T″, qui prouve que T′ est consistante, et on ne s'arrête jamais…).

@ooten: Ah ben ça c'est la question à beaucoup de zorkmids… La réponse courte est qu'on n'en sait rien ; mais plein de gens ont plein d'arguments à proposer selon le plan sur lequel on se place (mathématique, philosophique, épistémologique, heuristique…), selon leur inclinaison philosophique (plus ou moins platonicienne, plus ou moins formaliste, plus ou moins finitiste), et selon qu'on parle de PA, de ZFC (qui est strictement plus fort), ou encore de ZFC + tel ou tel axiome de grands cardinaux (qui est encore plus fort). Voici quelques uns des points de vue qu'on peut proposer :

✱ D'abord, mathématiquement et « officiellement », on n'en sait rien : l'orthodoxie mathématique est « sauf précision expresse du contraire, on travaille dans ZFC, on appelle "théorème" ce qui est un théorème de ZFC dont la démonstration est publiée dans la litérature mathématique, et Consis(ZFC) n'en est pas un, en tout cas on ne peut pas l'utiliser dans un raisonnement mathématique (sauf à le préciser explicitement) ; et d'après le théorème de Gödel, on sait qu'on ne pourra jamais le démontrer sauf si, en fait, il est faux ». ✱ Ceci est proche du point de vue formaliste qui, à l'extrême, est : « les mathématiques ne sont de toute façon qu'un jeu typographique dont les règles sont fixées par ZFC et qui n'a aucun rapport avec la réalité, et peut-être que les règles permettent de fabriquer le théorème 0=1, qui est alors la conclusion ultime qui met fin au jeu, et nous n'avons aucun moyen de le savoir (et si ça se produit, on passera à un jeu différent) ».

✱ La plupart des mathématiciens (au moins ceux qui ne sont pas ultrafinitistes, et même ceux-ci dans une certaine mesure que je ne comprends pas très bien) pensent qu'il y a a quelque chose de « vrai » dans les mathématiques, donc que si ZFC, ou en tout cas PA, démontre un énoncé sur les entiers naturels qui peut être testé algorithmiquement, alors cet énoncé est vrai. Par exemple, maintenant qu'on a une preuve de ∀x,y,z,n∈ℕ n≥3∧xyz>0 ⇒ x^n+y^n≠z^n (le théorème de Fermat) dans ZFC (et vraisemblablement dans des systèmes plus faibles même si personne n'a vérifié de bout en bout), on ne se fatigue pas à vérifier par ordinateur si par hasard on ne peut pas trouver x,y,z,n tels que x^n+y^n = z^n : on admet donc que ZFC dit, au moins dans une certaine mesure, au moins dans ce cas, des chose vraies — du coup, la question intéressante n'est pas « [pourquoi] ZFC est-il non-contradictoire ? » mais « pourquoi ZFC dit-il des choses vraies ? » (et s'il ne dit que des choses vraies, au moins en arithmétique, il ne va certainement dire que 0=1).

✱ La position des plus platoniciens est la suivante : ZFC n'est pas contradictoire parce qu'il est complètement *vrai*, les ensembles existent vraiment (en un sens idéal), notamment les grands infinis, et ZFC dit des choses vraies à leur sujet (il dit la vérité, et rien que la vérité, mais il ne dit pas toute la vérité : il faut ajouter des axiomes de grands infinis, et aussi sans doute des axiomes sur l'« épaisseur » du monde des ensembles, et même comme ça, on n'aura évidemment jamais fini car la vérité est inépuisable par une théorie axiomatique, mais on peut quand même aller nettement plus loin que ZFC).

✱ La position des ultrafinitistes, si je la comprends bien (ce qui n'est pas certain) est quelque chose comme ceci : ZFC est probablement inconsistant, et même PA probablement. Il se trouve qu'on peut quand même en tirer des conséquences justes parce que la contradiction dans ZFC/PA est subtile alors que beaucoup de raisonnements qu'on peut mener dedans, tant qu'ils ne font pas intervenir des nombres trop grands ou des infinis trop bizarres, seraient recopiables dans un système beaucoup plus faible et non-contradictoire car vrai (car portant uniquement sur des entiers de taille raisonnable, et dont les axiomes seraient donc essentiellement « testables »). Mais [d'après ces ultrafinitistes, toujours] on finira par trouver des contradictions comme on en a trouvé dans la théorie des ensembles de Frege (pré-ZFC, et fondée sur essentiellement un seul axiome: « pour tout P, on peut former l'ensemble des x tels que P(x) »), qui avait pourtant l'air intuitivement sensée et qui supportait, de fait tout un tas de conclusions justes (comme beaucoup de travaux mathématiques pré-ensemblistes).

✱ Beaucoup de gens peuvent, évidemment, avoir une position intermédiaire entre ces deux dernières (« ZFC est *vrai*, les ensembles existent vraiment » et « ZFC n'est que superficiellement juste et probablement contradictoire, seuls existent les entiers naturels de taille raisonnable »). Toutefois, ces positions intermédiaires (et même, à mon avis, celle des ultrafinitistes) buttent dans une certaine mesure contre l'objection : « si les ensembles n'existent pas vraiment, comment se fait-il qu'ils prédisent des choses vraies sur des entiers sur lesquels on peut tester ? »

✱ Heuristiquement, on peut raisonnablement penser : comme on a torturé ZFC dans tous les sens pour tenter d'y trouver une contradiction, et qu'on a même étendu ses axiomes par des axiomes de grands cardinaux gigantesques, s'il y avait une contradiction, on l'aurait trouvée. Il serait très surprenant qu'une preuve de contradiction sur quelque chose qui est, au final, assez simple, soit immensément difficile à dériver et qu'on n'y soit pas arrivé malgré tout l'examen auquel on a soumis ZFC. (On a trouvé une contradiction dans un certain axiome de grands cardinaux, les « cardinaux Reinhardt », et encore, seulement contre ZFC, pas contre ZF seul, et surtout, elle était assez facile à exhiber, comme quand Russell a trouvé une contradiction dans la théorie des ensembles de Frege, donc on peut espérer que, heuristiquement, les contradictions dans les théories assez simples sont assez simples à trouver.)

✱ Dans le cas de PA (mais pas de ZFC), on a une preuve de non-contradiction, due à Gentzen, qui repose sur un principe combinatoire « simple » (en l'occurrence, le fait que l'ordinal ε₀ a bien un sens). (Bon, on a aussi une preuve de Consis(PA) dans ZFC, mais elle n'est pas très instructive, elle formalise juste l'argument « PA est vrai, or 0≠1, donc PA ne prouve pas 0=1 ». La preuve de Gentzen, elle, utilise des principes plus simples que ZFC, et surtout plus compréhensibles intuitivement.) Cette preuve s'étend à des systèmes un peu plus forts que PA (comme la théorie des ensembles de Kripke-Platek), mais on est très loin de ZFC à l'heure actuelle (on n'atteint même pas l'arithmétique du second ordre, c'est-à-dire essentiellement la théorie des ensembles restreinte aux entiers naturels et ensembles d'entiers naturels).

✱ Et, bien sûr, la position pratique du mathématicien en exercice, c'est généralement quelque chose comme : « on s'en fout complètement : si quelqu'un trouve une contradiction dans ZFC, ce sera sur un "problème légal", c'est-à-dire en utilisant un type de raisonnement qui n'apparaît jamais dans les mathématiques vivantes en-dehors de la théorie des ensembles, donc il suffira de corriger un peu ZFC et tout ce qu'on aura démontré restera correct ». (L'idée qu'on puisse trouver une contradiction dans PA, à cet égard, est sans doute beaucoup plus gênante, parce qu'il est difficile d'imaginer que ça ne mette pas à terre tout l'édifice des mathématiques existantes, quoi que les ultrafinitistes puissent dire à ce sujet.)

Voilà, maintenant sans doute que d'autres lecteurs peuvent apporter encore d'autres positions sur ce débat.