Petit résumé du théorème de Gödel

15 juin 2002

(cf. Complexité et complication)

Le théorème de Gödel [Gödel] a été publié en 1931. Il démontre que si l’on construit un système logique pour formaliser la théorie des nombres entiers, ce système contiendra au moins une formule A qui est vraie mais qui est telle que ni A, ni sa négation non-A ne pourront être formellement démontrées dans le cadre du système.

Russell et Whitehead avaient tenté de fonder l'ensemble de la logique sur une base axiomatique. Gödel a démontré avec son théorème que ce but était hors d'atteinte puisque, quel que soit le nombre (fini) des axiomes retenus pour fonder un système logique, il existera toujours des propositions vraies que l'on ne pourra pas démontrer dans le cadre de ce système. 

Cette découverte a été déchirante pour beaucoup de mathématiciens. "Karl Menger avait commencé sa carrière en s'intéressant à la logique et aux fondements des mathématiques. La publication du fameux théorème d'impossibilité de Gödel lui porta un coup dont il ne se remit jamais. (...) Y penser le déprimait et, alors qu'il me racontait cette histoire, il s'enferma peu à peu dans un silence sombre qui dura jusqu'à la fin du repas" (Herbert Simon, Models of my Life, MIT Press 1996, p. 101).

La démonstration de Gödel est très technique et sa lecture est difficile. Voici une description schématique de son raisonnement, tel qu’il le présente lui-même dans l’introduction de son article :

1) Supposons qu’il existe une Théorie Complète (TC) fondée sur un nombre fini d'axiomes et permettant, si l’on considère une phrase quelconque, de décider sans jamais se tromper si cette phrase est vraie ou non.

2) Considérons la phrase « TC ne dira jamais que la présente phrase est vraie ». Nommons cette phrase G, ce que nous noterons : G = « TC ne dira jamais que G est vraie ».

3) Soumettons G à TC et demandons à TC de dire si G est vraie ou non.

4) Si TC dit que G est vraie, alors G est fausse. Mais alors comme TC a dit que G était vraie, TC a commis une erreur. Cependant par hypothèse TC ne se trompe jamais. Donc TC ne dira jamais que G est vraie.

5) Si « TC ne dit jamais que G est vraie », G est vraie. Mais d'après ce que nous venons de voir TC ne pourra jamais le dire.  

6) Il ne peut donc pas exister de Théorie Complète, c’est-à-dire de théorie permettant, quelle que soit la phrase que l'on considère, de dire si elle est vraie ou non.

Ce raisonnement rappelle le paradoxe fameux qui met en scène un Crétois disant : « Les Crétois ne disent que des mensonges ». 

Application à l'informatique

Un des résultats importants de la théorie de l'informatique ([Sipser] p. 165), c'est qu'il est impossible de concevoir un programme capable de vérifier tous les programmes. Ce résultat est une application du théorème de Gödel. 

Supposons en effet qu'un tel programme P existe. 

1) Si le programme A est juste, P(A) = v (v pour « vrai »). 

2) Soumettons à P le programme G = « P(G) = f » (f pour « faux »).  

3) Si P(G) = v, le programme P(G) = f est faux ; donc P[P(G) = f ] = P(G) = f, ce qui est contraire à l'hypothèse. Si P(G) = f, alors on a P[P(G) = f ] = P(G) = v, ce qui est encore contraire à l'hypothèse. 

4) Ainsi G ne peut pas être vérifié par P. Il ne peut donc pas exister de programme capable de vérifier tous les programmes.

Certes on peut définir des méthodes de vérification efficaces et les outiller de sorte qu'elles soient faciles à utiliser. Mais ces méthodes, aussi efficaces soient-elles, ne garantissent pas que tous les programmes qu'elles valident soient corrects.

Retour à "Sortir de l'embarras"