L'incomplétude mathématique/Les prédicats de prouvabilité et le premier théorème d’incomplétude de Gödel
Gödel a prouvé qu’une théorie mathématique T vraie et suffisamment riche remplit une autre condition. Pour toute théorie axiomatique T’, il existe dans T un prédicat de prouvabilité pour T’, c’est-à-dire une formule à une variable x qui est vraie si et seulement si x représente un théorème de T’, c’est-à-dire une formule démontrable à partir des axiomes de T’. En particulier, T contient un prédicat de prouvabilité pour elle-même.
Même l’arithmétique formelle est capable de représenter ainsi toutes les théories axiomatiques. En ce sens on peut la voir comme une théorie universelle. Il suffit de savoir raisonner sur les nombres pour définir toutes les théories concevables. Les nombres peuvent être considérés comme les atomes, les principes premiers de la raison, au sens où tout le reste peut être construit à partir d’eux. Il y a quelque chose de pythagoricien, tout est nombre, dans cette approche gödelienne des mathématiques.
Comme pour la condition d du théorème de Tarski, la preuve de l’existence d’un prédicat de prouvabilité est un peu difficile quand on représente des formules par des nombres. Dans le chapitre suivant, on montrera que l’existence d’un prédicat de prouvabilité pour toute théorie axiomatique à l’intérieur d’une théorie élémentaire, Enum, est une conséquence directe du théorème fondamental de l’énumérabilité, qui sera démontré.
À partir du théorème de Tarski et de l’existence d’un prédicat de prouvabilité on déduit le premier théorème d’incomplétude de Gödel comme une conséquence directe.
Une théorie axiomatique, vraie (c'est-à-dire cohérente) et suffisamment riche, ne peut pas prouver toutes ses formules vraies.
Ce théorème peut être considéré comme un corollaire de celui de Tarski. Mais Gödel est le premier à avoir publié ses preuves. Tarski a eu les mêmes intuitions au même moment.
La fin de la preuve de Gödel est semblable à celle de Tarski, sauf qu’il se sert pas d’un prédicat de vérité mais du prédicat de prouvabilité dont il a montré auparavant l’existence.
Gödel considère alors la formule « il existe un z tel que SUBxxz et non Pz ». Elle est représentée par un nombre n de T. Il y a aussi un autre nombre KG tel que SUBnn(KG). n et (KG) sont des nombres bien définis que l’on peut calculer dès que les axiomes de T et le procédé de représentation des formules de T par des nombres sont précisément définis.
KG représente-t-il une formule prouvable ?
La formule représentée par KG dit que le prédicat représenté par n est vrai pour n. Le prédicat représenté par n est vrai pour x si et seulement s'il existe un z tel que SUBxxz et non Pz. La formule représentée par KG est donc équivalente à (il existe un z tel que SUBnnz et non Pz) par définition de KG. Or SUBnnz équivaut à z=(KG). Donc par définition de KG, la formule représentée par KG équivaut à non P(KG). Autrement dit la formule représentée par KG dit d’elle-même qu’elle n’est pas prouvable.
Si on suppose que T est cohérente alors KG est nécessairement vraie, parce que si elle ne l’était pas, alors elle serait prouvable, T permettrait de prouver une formule fausse et ne serait donc pas cohérente.
La partie longue de la démonstration de Gödel consiste à définir un prédicat de prouvabilité à l’aide d’une représentation des formules par numérotation. Après les découvertes de Church, Post et Türing, les résultats de Gödel sur la prouvabilité s’inscrivent dans un contexte plus général, celui des ensembles énumérables. Nous montrerons que l’ensemble des théorèmes, ou formules prouvables, d’une théorie axiomatique est énumérable.
On pourrait croire que les énoncés vrais mais non prouvables sont toujours des formules très compliquées, construites avec des techniques logiques paradoxales, qui n’interviennent jamais dans les mathématiques couramment étudiées. Autrement dit, on pourrait espérer que l’incomplétude est seulement marginale et qu’elle ne concerne pas les questions mathématiques importantes.
La preuve donnée par Cohen qu’une conjecture de Cantor, l’hypothèse du continu, n’est pas prouvable à partir des axiomes de ZFC, montre au contraire que l’improuvabilité est une question qui se pose vraiment. En nous fondant sur cette preuve nous montrerons que les ensembles indicibles sont indéfinis, au sens où il n’est pas possible de définir de façon univoque la notion de vérité à leur sujet.
Même des théorèmes des mathématiques élémentaires, sur les équations diophantiennes par exemple, ne peuvent pas être prouvés sur la base des seuls axiomes couramment acceptés.
