Aussi curieux que cela puisse paraître, ce monument de la pensée mathématique de la première moitié du vingtième siècle n’avait été traduit qu’en langue russe, alors qu’il intéresse au premier chef, aujourd’hui encore, logiciens, mathématiciens, informaticiens, historiens et philosophes. Il faut donc féliciter nos collègues de s’être lancés dans ce gigantesque travail qui non seulement traduit un texte au vocabulaire riche et précis mais compare les deux éditions, séparées d’une trentaine d’années fécondes en publications, et replace le texte dans la logique contemporaine, de l’avoir mené à terme et d’avoir réussi à le faire éditer grâce à leur opiniâtreté et à l’appui de la communauté.

L’objectif de cet ouvrage en deux volumes, poursuivi par les philosophes depuis l’antiquité, est de justifier les mathématiques ébranlées par des paradoxes comme ceux de Zénon et de Russell. L’entreprise d’Hilbert et Bernays comporte deux étages : le premier constate qu’une partie des mathématiques (par exemple les propriétés élémentaires des nombres premiers) est issue de l’expérience et par là justifiée ; le second part de l’idée que les mathématiques déjà justifiées devraient pouvoir servir à justifier le reste ; la méthode consisterait à formaliser les mathématiques en mettant le discours sous forme d’une suite de formules n’omettant aucune étape déductive puis à démontrer que cette partie formalisée n’est pas contradictoire. Ce second étage nécessite de longs développements techniques qui occupent la plus grande partie de l’ouvrage.

Ce second volume explicite le programme d’Hilbert pour prouver la non-contradiction de l’arithmétique de Péano du premier ordre. Il donne des preuves détaillées des deux théorèmes de Gödel. Le traité contient une avancée significative vers l’objectif d’Hilbert, mais encore aujourd’hui la tâche est loin d’être terminée, même pour la logique mathématique et pour l’arithmétique. Pour ce qui est de la géométrie, il laisse de côté la géométrie différentielle et quant à l’analyse, on en reste au stade de la formalisation sans preuve de non-contradiction.