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.

Le premier tome traite des propositions, des prédicats du premier ordre, de la récursivité primitive et de la formalisation de l’arithmétique ; des algorithmes de décision y sont développés et il s’achève sur un traitement des opérateurs de description.

Si, depuis 1970, la logique a été approfondie et son expression perfectionnée, le livre reste le témoin d’une grande époque de création en logique après les bouleversements dus à Gödel, Herbrand, Church et Turing.