Quelqu'un pour m'expliquer CLAIREMENT le théorème d'imcomplétude de Gödel et ce que ça implique CONCRÈTEMENT ?

Je suis tombé dessus par hasard et j'ai tout de suite était fasciné. Mais en approfondissant un peu, je me suis vite rendu compte que c'était beaucoup plus complexe que je ne l'avais imaginé ...
Alors j'espère vraiment qu'on pourra m'éclairer ici a ce sujet.

Merci d'avance pour vos réponses

Les théorèmes d'incomplétude de Gödel (il y en a deux), s'inscrivent dans le programme de Hilbert du début du 20ème siècle. Le but de ce programme : formaliser les fondements des mathématiques, leur donner des bases solides, définir rigoureusement ce que sont les axiomes qu'on utilise, les règles de raisonnement qui sont autorisées, etc.

Cela a donné lieu, notamment, à la théorie des ensembles, que l'on considère aujourd'hui comme la théorie sur laquelle se basent la plupart des résultats mathématiques. Mais, dans ses débuts, les premières versions de la théorie des ensembles étaient incohérentes : elles permettaient de prouver n'importe quoi (exemple: le paradoxe de Russell). En modifiant un peu la théorie, en rajoutant des axiomes, les logiciens ont réussi à contourner ces problèmes, jusqu'à aboutir à la théorie des ensembles qu'on connait aujourd'hui. Mais comment être sûrs qu'il n'y a pas d'autre "bug" caché qui n'a tout simplement pas encore été découvert ? L'un des objectifs du programme de Hilbert était d'arriver à prouver la cohérence de la théorie sur laquelle on fonde les mathématiques, de façon à être surs qu'on ne puisse pas trouver de nouveau paradoxe.

Les théorèmes d'incomplétude viennent clore le projet de Hilbert par la négative : c'est impossible de construire une telle théorie "parfaite". Plus précisément, le premier théorème dit que parmi les quatre propriétés suivantes, une théorie mathématique ne peut en vérifier que trois au maximum :

• Cohérence : ne pas permettre de prouver de proposition fausse
• Complétude : tout théorème est soit prouvable, soit sa négation est prouvable
• Avoir la puissance de l'arithmétique : être capable de parler des entiers naturels, de l'addition et de la multiplication
• Être récursivement axiomatisable : étant donnée une formule quelconque, on sait dire si oui ou non c'est un axiome de la théorie

Par exemple, l'arithmétique de Presburger est cohérente, complète, et récursivement axiomatisable, mais elle ne permet pas de parler de la multiplication, et donc elle est très limitée.
On peut montrer qu'il existe des théories cohérentes, complètes, et qui contiennent l'arithmétique, mais ce sont des trucs totalement inutilisables.
En général, les théories mathématiques intéressantes, ce sont celles chez qui il manque la propriété de complétude : il y a des énoncés dont on ne peut ni prouver qu'ils sont vrais, ni prouver qu'ils sont faux. On dit qu'ils sont indécidables.

La preuve de ce premier théorème d'incomplétude construit un énoncé indécidable un peu artificiel : c'est juste un paradoxe du menteur un peu plus élaboré, style "cette phrase est fausse". On pourrait se dire que ce n'est pas très grave, ce qui nous intéresse c'est faire des maths, pas s'occuper de ce genre d'énoncés bizarres.

Le deuxième théorème d'incomplétude vient nous donner un autre exemple bien plus concret d'énoncé indécidable, et c'est lui qui vient tordre le cou au programme de Hilbert : dans une théorie cohérente, récursivement axiomatisable, et qui contient l'arithmétique, l'énoncé qui exprime la cohérence de cette théorie est indécidable. Notre théorie a beau être cohérente, elle ne pourra jamais le prouver, on ne peut que lui faire confiance et espérer...

Alors, bien sur, cinq ans après les théorèmes d'incomplétude, Gentzen se ramène avec une preuve de cohérence de l'arithmétique. Gödel ou Gentzen, lequel a raison ? En fait, les deux. L'arithmétique de Peano ne peut pas prouver sa propre cohérence, mais Gentzen a fait sa preuve dans une autre théorie strictement plus forte. Donc ce que dit cette preuve, c'est qu'on peut faire confiance à l'arithmétique, à condition que cette autre théorie plus forte soit cohérente, et on est revenus au point de départ...

D'accord, donc si j'ai bien compris, le 2ème théorème d'incomplétude nous dit qu'une théorie, aussi cohérente soit-elle, ne peut pas prouver qu'elle est vraie par elle même. Mais ne serai-t-il pas possible de la prouver par le biais d'une autre théorie ? Ou est ce que ce n'est pas possible du fait que cette théorie aussi est "improuvable", comme toutes les autres ( même si, pour moi, une théorie cohérente, prouvée par une seconde théorie, est suffisant pour que je lui fasse confiance )
Et est ce que cela implique que toutes nos plus belles théories mathématiques, physiques, etc ne sont que conjecture ? Qu'il n'existe pas de vérité absolue ?
Et pourquoi ce théorème pose les "limites de la logique" ?

Le 22 juin 2015 à 11:37:29 RISOTTODESBOAS a écrit :
D'accord, donc si j'ai bien compris, le 2ème théorème d'incomplétude nous dit qu'une théorie, aussi cohérente soit-elle, ne peut pas prouver qu'elle est vraie par elle même. Mais ne serai-t-il pas possible de la prouver par le biais d'une autre théorie ? Ou est ce que ce n'est pas possible du fait que cette théorie aussi est "improuvable", comme toutes les autres ( même si, pour moi, une théorie cohérente, prouvée par une seconde théorie, est suffisant pour que je lui fasse confiance )

Oui, tu as bien compris, c'est ce que je disais dans le dernier paragraphe : l'arithmétique ne peut pas prouver sa propre cohérence. Par contre, on peut prouver la cohérence de l'arithmétique par le biais d'une autre théorie plus forte. Mais l'intérêt philosophique de ce genre de preuve n'est pas très clair : on n'a fait que reculer, vu que maintenant pour être sûr qu'on ne fait pas n'importe quoi, il faudrait prouver la cohérence de cette autre théorie plus forte... mais vu qu'elle est plus forte, la tâche est devenue plus difficile qu'avant.

Par exemple si on a une théorie T dont on ne sait pas si elle est cohérente. Eh bien on n'a qu'à considérer la théorie T' où l'on rajoute la cohérence de T comme axiome : T' = T + «T est cohérente». La théorie T' prouve bien la cohérence de T, mais ça ne nous avance pas à grand chose...

Des gens ont essayé de construire des tours de théories où chacune prouve la cohérence de la précédente, mais ce n'est pas très clair que ça ait le moindre intérêt, ça ressemble fortement à l'histoire de la Terre plate posée sur le dos d'une tortue géante, elle même posée sur le dos d'une autre tortue encore plus grande, et ce «jusqu'en bas».

Et est ce que cela implique que toutes nos plus belles théories mathématiques, physiques, etc ne sont que conjecture ? Qu'il n'existe pas de vérité absolue ?

"Conjecture" est un peu péjoratif comme terme dans ce cadre là, mais dans l'idée, oui. On ne sera jamais sûrs à 100% que la théorie dans laquelle on travaille est cohérente, car si elle l'est, le théorème d'incomplétude nous dit qu'on ne peut pas le prouver.

Quant à la question de la vérité, c'est un peu plus ténu. Strictement parlant, dans le théorème de Gödel, il est question de prouvabilité et non de vérité d'un énoncé. La logique a un peu de mal à parler de la notion de vérité, d'ailleurs avec un peu d'imagination certains voient le théorème d'incomplétude comme un «théorème de non-définissabilité de la vérité». Quand à la non-existence de la vérité, c'est sans doute un peu tiré par les cheveux comme conclusion, la philosophie a encore pas mal de chemin à faire avant de répondre à ce genre de question et c'est pas l'incomplétude qui va clore définitivement le débat

Et pourquoi ce théorème pose les "limites de la logique" ?

Les limites de la logique, dans le sens où il met fin au rêve de Hilbert : disposer d'une théorie mathématique parfaite, unifiée, qui permette de répondre à toutes les questions mathématiques et à laquelle on puisse vouer une confiance sans limites. Une telle théorie n'existe pas.

Mais aujourd'hui, avec presque un siècle de recul, les logiciens sont un peu plus optimistes et ont tendance à se dire "heureusement qu'on a l'incomplétude !". Ce théorème laisse place à la créativité en mathématiques : quoi qu'on fasse, il y aura toujours de nouvelles théories à construire et à découvrir, on n'aura jamais "terminé les mathématiques". Par exemple, depuis les années 70, une nouvelle théorie a commencé à émerger, la théorie des types, qui offre un substitut intéressant à la théorie des ensembles. L'une n'est pas forcément "meilleure" que l'autre, elles sont juste différentes, avec tout plein de trucs intéressants à découvrir dans les deux mondes

Intéressant merci Lowenheim

Le 22 juin 2015 à 12:22:16 Lowenheim a écrit :
Des gens ont essayé de construire des tours de théories où chacune prouve la cohérence de la précédente, mais ce n'est pas très clair que ça ait le moindre intérêt, ça ressemble fortement à l'histoire de la Terre plate posée sur le dos d'une tortue géante, elle même posée sur le dos d'une autre tortue encore plus grande, et ce «jusqu'en bas».

N'est-il pas envisageable de construire un tore plutôt qu'une tour ?
C'est à dire une théorie qui prouve la cohérence d'une autre théorie elle même prouvant la cohérence d'une autre théorie ... et ainsi de suite jusqu'à construire une dernière théorie qui prouve la cohérence de la première (qui du coup peut ne pas être considérer première) ?

C'est peut être un peu tordu, et probablement déjà pensé, mais qu'est-ce qui empêcherait ce genre de chose d'arriver pour prouver la cohérence de tout le système ? Et est-ce qu'il n'y a pas un biai et que finalement, ça ne prouve pas vraiment la cohérence du tout ?

En tout cas, très bonne explication. Je vois plus clairement ce que signifie ce principe d'incomplétude.

J'avais entendu parler de ce principe la première fois avec les problèmes d'échelle d'infini. Comment prouver qu'il n'y a pas d’intermédiaire entre l'infini des entier naturelle (ou des nombre rationnelle, il y en a autant) et l'infini des nombres réels ? Godel s'est aussi penché sur cette question, et il en a conclu qu'il n'y a pas de solution. On peut parfaitement construire une théorie sur laquelle il y a des intermédiaires, comme en construire une autre sur laquelle il n'y a pas d'intermédiaire.

D'ailleurs il me semblait que c'était là dessus qu'il avait fini par construire son principe d'incomplétude. Mais j'ai dû mal comprendre

Je pense personnellement que pour qu'une théorie soit valable, c'est comme en science, il faut la blinder, qu'elle s'appuie sur des principes, d'autres théories, voir des applications qui vont dans le sens de cette théorie.

oui, en maths il peut y avoir des applications qui vont dans le sens d'une théorie mathématique. Je pense à la fameuse égalité 1+2+3 ... à l'infini = -1/12. ça parait absurde, on pourrait se dire qu'il faudrait construire une théorie qui évite ce genre d'égalité, et pourtant cette équation a déjà été utilisée en physique théorique (pour l'effet casimir, il me semble) et l'utilisation du résultat -1/12 a été validé par les expériences.
Du coup, il n'est plus possible de construire une théorie selon laquelle cette égalité est fausse (à mon sens, il n'y a plus vraiment de raison de le faire, sauf de montrer que c'est possible ... à moins que ça ne soit pas possible ?)

Et j'imagine qu'il doit existe d'autres exemple du genre.

P.S. : ça sert à quoi de prouver qu'un ensemble E contenant tout les ensembles qui n'appartiennent pas à E existe ? Cet ensemble ne sert à rien si ce n'est à faire perdre la tête XD. Et des paradoxes du genre, on peut en construire une infinité, sans passer par les maths. ça doit être inhérent à la logique, j'imagine. Une logique sans paradoxe n'est plus une logique ^^.

Le 22 juin 2015 à 18:56:35 Trent2 a écrit :
N'est-il pas envisageable de construire un tore plutôt qu'une tour ?
C'est à dire une théorie qui prouve la cohérence d'une autre théorie elle même prouvant la cohérence d'une autre théorie ... et ainsi de suite jusqu'à construire une dernière théorie qui prouve la cohérence de la première (qui du coup peut ne pas être considérer première) ?

Non : pour qu'une théorie puisse prouver la cohérence d'une autre, il faut qu'elle soit strictement "plus forte". Si tu fais un anneau, y'a forcément un endroit où une théorie plus faible va devoir prouver la cohérence d'une théorie plus forte, et ça sera pas possible.
Y'a vraiment pas de "remède" à l'incomplétude, on peut pas la contourner, faut faire avec

J'avais entendu parler de ce principe la première fois avec les problèmes d'échelle d'infini. Comment prouver qu'il n'y a pas d’intermédiaire entre l'infini des entier naturelle (ou des nombre rationnelle, il y en a autant) et l'infini des nombres réels ? Godel s'est aussi penché sur cette question, et il en a conclu qu'il n'y a pas de solution. On peut parfaitement construire une théorie sur laquelle il y a des intermédiaires, comme en construire une autre sur laquelle il n'y a pas d'intermédiaire.

Oui, c'est un autre exemple d'énoncé concret qui est indécidable dans ZFC : l'hypothèse (généralisée) du continu. Et au passage on peut aussi rajouter le plus connu, l'axiome du choix (indécidable dans ZF).
Gödel a montré qu'on ne pouvait pas réfuter l'hypothèse du continu quelques années après son théorème d'incomplétude, et Paul Cohen a montré bien plus tard qu'on ne pouvait pas non-plus la prouver, ce qui la rend indécidable.

Je pense personnellement que pour qu'une théorie soit valable, c'est comme en science, il faut la blinder, qu'elle s'appuie sur des principes, d'autres théories, voir des applications qui vont dans le sens de cette théorie.

C'est assez discutable, je trouve ça dommage de réduire les maths à leurs potentielles applications ou à leur capacité à décrire des phénomènes physiques concrets Tant qu'on trouve un intérêt intellectuel à développer une théorie mathématique, aussi farfelue soit-elle, pourquoi s'en priver ? Les poètes ont bien le droit au rêve et à l'insouciance, pourquoi pas les mathématiciens
Par exemple, le système T de Gödel est carrément incohérent (tout est prouvable), mais ça ne l'empêche pas d'être intéressant à étudier

à oui, mais en tant que physicien, je vois le coté pratique avant tout, alors j'oublie souvent que les mathématiques vont plus loin que ça. C'est un art pour certain, et c'est bien comme ça, car parfois la physique a besoin de concepts mathématiques nouveau, dont les mathématiciens ont le secret ^^.

En fait, j'ai du mal à cerner l'incomplétude ; est ce qu'elle relève de la métamathématique, est ce plus un courant de pensée philosophique, ou existe-il des applications concrètes de ce théorème.
Ou est ce tout simplement une belle preuve de l'étendue des mathématiques, et que ce théorème peut connaitre différentes approches ( philosophiques, mathématiques ...)

Merci pour toutes tes réponses Lowheim, très intéressant.
(Tu m'as l'air vraiment calé sur la chose, c'est un intérêt particulier pour ce théorème uniquement, ou est ce que tu es autant intéressé par les mathématiques en général ? )

C'est un théorème de maths, qui se prouve, tout comme on peut prouver le théorème de Pythagore. Ce n'est pas seulement un "courant de pensée", comme tu dis. C'est assez proche de la philosophie certes, puisque la logique et les fondements des mathématiques sont des sujets qui intéressent aussi bien les philosophes que les mathématiciens, mais c'est vraiment un théorème au sens où on l'entend habituellement.

Quant aux "applications concrètes", il n'y en a pas vraiment, c'est surtout un théorème qui signale un cul-de-sac mathématique, il indique l'impossibilité de trouver la théorie mathématique parfaite. Mais y'a quelques exemples concrets d'énoncés indécidables, cités plus haut : l'axiome du choix et l'hypothèse du continu

La logique a un statut un peu étrange au sein des mathématiques : c'est une branche des maths qui considère les formules, les preuves et les théories mathématiques comme des objets mathématiques à part entière, de la même manière que d'autres branches des maths étudient les entiers, les fonctions ou les espaces vectoriels. On fait "des maths à l'intérieur des maths", en quelque sorte.

Et de rien, ça me fait plaisir de répondre à ce genre de topics Je suis étudiant en logique, plus particulièrement je m'intéresse à la théorie des types (que j'ai mentionnée dans un message précédent).

D'accord, c'est plus clair maintenant

La théorie des types ? Ça à un quelconque rapport avec la théorie des groupes de Galois ? (c'est bien Galois la théorie des groupes ? )
Tu nous fais un petit topo ?

J'ai lu ce topic avec beaucoup d'intérêt, merci Lowenheim.

J'ai une question, qui peut-être montrera que je n'ai rien compris, mais c'est pas grave^^

Le théorème d'incomplétude n'est-il pas lui-même sujet à ce qu'il affirme ? Pour démontrer le théorème d'incomplétude, on utilise une logique et un formalisme choisis parmi ceux d'une théorie donnée, théorie qui elle-même "souffre" de l'incomplétude. Par conséquent, le théorème d'incomplétude n'est lui-même pas certain. Et alors on n'a rien dit, sur rien.

Exactement, c'est un point qui me tracassais aussi, c'est très pertinent. C'est bien pour ça qu'on dis que ce théorème pose des limites à la logique elle-même...

Mais j'ai l'impression que Mr Lowenheim nous a quitté

Le théorème d'incomplétude n'est-il pas lui-même sujet à ce qu'il affirme ? Pour démontrer le théorème d'incomplétude, on utilise une logique et un formalisme choisis parmi ceux d'une théorie donnée, théorie qui elle-même "souffre" de l'incomplétude. Par conséquent, le théorème d'incomplétude n'est lui-même pas certain. Et alors on n'a rien dit, sur rien.

Y'a un peu de ça, oui, en effet.
Comme je disais, quand on fait de la logique, on traite les théories mathématiques comme des objets mathématiques à part entière, et on raisonne dessus. Mais pour pouvoir raisonner sur des objets mathématiques, il faut bien qu'on dispose d'une autre théorie "ambiante", "intuitive". On parle de méta-théorie pour désigner la théorie qu'on utilise pour raisonner, et théorie cible pour désigner celle que l'on est en train d'étudier.

Idéalement, on veut utiliser une méta-théorie la moins "forte" possible. En général, si on arrive à s'en sortir en n'utilisant que des mathématiques finitistes, c'est-à-dire des manipulations basiques de suites finies d'un nombre fini de symboles, sans raisonnement par récurrence, on considère que le raisonnement est "sûr". On est donc bien en-dessous de l'arithmétique de Peano.
Je pense que le théorème d'incomplétude rentre dans ce cadre-là (j'en mettrais pas ma main à couper, faudrait vérifier dans les détails mais il se base juste sur des propriétés très basiques du langage).

Mais en effet il subsiste quand même une impression pesante que "on ne dit rien, sur rien" comme tu dis, mais cette impression est présente dans toutes les sciences, les mathématiques et la philosophie, alors il faut faire avec

La théorie des types ? Ça à un quelconque rapport avec la théorie des groupes de Galois ? (c'est bien Galois la théorie des groupes ? )

Euh, non pas du tout
D'ailleurs les "groupes de Galois" ça existe, la "théorie des groupes" aussi, mais c'est pas vraiment la même chose attention

Tu nous fais un petit topo ?

Hum, y'a plein de choses à dire et je suis pas super motivé pour écrire un pavé, je vais essayer de pas faire trop long

D'une part, autour des années 1950, des logiciens et informaticiens ont découvert la correspondance de Curry-Howard, ou encore "correspondance preuves-programmes" : un programme informatique et une preuve mathématique ont en fait la même structure, il s'agit du même objet mathématique sous-jacent.
Dans un premier temps, cette correspondance n'était pas facile à comprendre et à étudier : les informaticiens et les logiciens ont chacun développé leur truc de leur côté, et du coup ils manipulaient des formalismes très différents, même si "au fond" il s'agissait de la même chose.

Dans les années 1970, Per Martin-Löf a développé un langage, la théorie des types, qui est basée sur cette correspondance preuves / programmes. Elle a donc été conçue dès le début comme était à la fois un langage de programmation, et un langage pour écrire des preuves mathématiques.
L'intérêt, c'est que ça permet de mieux comprendre comment se comportent les preuves mathématiques informatiquement.

En maths, il y a la partie "calcul", qui peut facilement être automatisée par une calculatrice, un ordinateur, et la partie "raisonnement" qui demande de réfléchir et qu'un ordinateur ne sait pas faire. On a souvent du mal à les dissocier. Par exemple, on voit souvent les nouveaux entrants en prépa dire qu'en prépa ils font de "vraies" maths, alors qu'au lycée on n'en faisait pas. Plus que "vraies" et "fausses" maths, la distinction est surtout entre "preuves" et "calcul".

Avec la théorie des types, on arrive à mieux les dissocier, si bien que ça a permis de concevoir des logiciels permettant de faire vérifier ses preuves mathématiques par un ordinateur. Un des plus connus est Coq, et comme son nom l'indique il est français L'idée, c'est que l'utilisateur écrit sa preuve dans un langage qui ressemble un peu à de la programmation, et l'ordinateur fait les calculs et vérifie que tout est juste. C'est encore récent (Coq a une vingtaine d'années) donc c'est assez fastidieux pour l'instant, mais c'est assez prometteur

Salut, je te conseil "Gödel, Escher, Bach : Les Brins d'une Guirlande Éternelle" sur ce sujet ou le théorème est bien expliqué avec des images sympathiques. Ce que j'en ai retenu c'est qu'on fait "exploser" un système formel par résonance un peu comme dans la phrase "Cette phrase ne dis pas la vérité". Si cette phrase ne dis pas la vérité alors elle ment et si elle ment c'est qu'elle dit la vérité,... Bref dès qu'il y a auto-référence cela amène à des absurdités.

Ouais, c'est comme quand t'imagine une procédure mécanique, ou un algorithme, qui répond vrai ou faux à chaque affirmation.
Si tu lui dis : "La machine répondra jamais vrai a cette affirmation".
Si elle répond vrai, l'affirmation est fausse, or elle a répondu vrai.
Si elle répond faux, elle confirme l'affirmation, elle aurai donc du répondre vrai.

Mais que ce passerai-t-il dans ce genre de cas ?

Très bien expliqué