Jacques Herbrand

En 1930, Jacques Herbrand soutient une thèse de logique mathématique, domaine alors peu valorisé en France. Son idée la plus célèbre relie deux étages du raisonnement : des formules portant sur des objets, puis des propositions que l'on peut tester comme vraies ou fausses.

Ce passage fournit un critère pour étudier des formules du calcul des prédicats du premier ordre. Il explique pourquoi le théorème de Herbrand demeure un fondement théorique de la démonstration automatique.

Jacques Herbrand (1908-1931) est un mathématicien et logicien français. Reçu premier à l'École normale supérieure en 1925 puis premier à l'agrégation de mathématiques en 1928, il soutient en 1930 une thèse dirigée par Ernest Vessiot. Cette thèse porte sur la logique mathématique.

Son résultat central, le théorème de Herbrand, concerne les formules du calcul des prédicats du premier ordre. Pour une formule universelle close dont la matrice est sans quantificateur, il caractérise l'insatisfaisabilité par l'existence d'une conjonction finie d'instances closes propositionnellement insatisfaisable. Pour traiter la validité d'une formule close, on applique ce critère à sa négation, préalablement mise sous forme prénexe et skolémisée. Cette réduction constitue encore un fondement théorique des logiciels de démonstration automatique.

Lors d'un séjour en Allemagne en 1931, Herbrand poursuit des travaux en logique et en théorie des nombres. Sa dizaine d'articles simplifie ou généralise des résultats de Kronecker, Heinrich Weber, Hilbert et Emil Artin. Son nom reste également attaché au théorème de Herbrand-Ribet en théorie des nombres et au modèle de Herbrand-Gödel des fonctions récursives, fondateur pour la théorie de la calculabilité.

Prenons une formule volontairement élémentaire pour voir le changement d'étage. Le symbole P représente une propriété quelconque, x représente un objet variable et a représente un objet particulier. On considère l'affirmation : tout objet possède la propriété P ou ne la possède pas.

1. La formule du premier ordre s'écrit $\mathrm{\forall }x(P(x)\vee \mathrm{\neg }P(x))\backslash forall\; x\backslash ,\backslash bigl(P(x)\backslash lor\; \backslash neg\; P(x)\backslash bigr)$.

2. On remplace l'objet variable x par l'objet particulier a. On obtient l'instance $P(a)\vee \mathrm{\neg }P(a)P(a)\backslash lor\; \backslash neg\; P(a)$.

3. Appelons maintenant p la proposition « P(a) ». L'instance prend la forme propositionnelle $p\vee \mathrm{\neg }pp\backslash lor\; \backslash neg\; p$. Elle est vraie que p soit vraie ou fausse : c'est une tautologie.

Le contrôle consiste à examiner les deux valeurs possibles de p. Cet exemple illustre seulement l'instanciation, c'est-à-dire le remplacement de x par a, puis le test propositionnel ; il ne déroule ni toute la procédure ni la preuve du théorème général. Dans le critère complet présenté par la définition, on part de la négation de la formule dont on étudie la validité, on la transforme, puis on cherche une famille finie d'instances dont la conjonction est propositionnellement insatisfaisable.

En démonstration automatique, l'approche de Herbrand sert de fondement théorique lorsque le problème est formulé dans le calcul des prédicats du premier ordre. Le geste consiste à chercher des instances qui transforment la question en un test propositionnel.

Pour lire un raisonnement fondé sur ce théorème, on repère d'abord les variables et leurs quantificateurs. On suit ensuite leur remplacement par des termes particuliers, puis on vérifie la tautologie propositionnelle obtenue.

Pour situer l'œuvre de Herbrand, il faut aussi distinguer ses domaines. Le théorème de Herbrand relève de la logique, le théorème de Herbrand-Ribet de la théorie des nombres, et le modèle de Herbrand-Gödel des fonctions récursives éclaire la calculabilité.

Jacques Herbrand et le théorème de Herbrand. Le premier est le mathématicien français né en 1908 ; le second est son résultat de logique. Une date biographique désigne la personne, tandis qu'un critère sur des formules désigne le théorème.

Théorème de Herbrand et théorème de Herbrand-Ribet. Le critère qui relie le calcul des prédicats aux tautologies propositionnelles appartient à la logique. Le résultat portant le double nom Herbrand-Ribet appartient à la théorie des nombres.

Théorème de Herbrand et modèle de Herbrand-Gödel. Le premier fournit le critère logique décrit dans la fiche. Le second concerne les fonctions récursives et joue un rôle fondateur dans la théorie de la calculabilité.

Une instance n'est pas le théorème entier. Dans l'exemple, $p\vee \mathrm{\neg }pp\backslash lor\; \backslash neg\; p$ est déjà une tautologie. Ce succès illustre le mécanisme, mais ne suffit pas à établir le résultat général pour toutes les formules du premier ordre.

« Réduire » ne signifie pas effacer les quantificateurs au hasard. Le symptôme d'une mauvaise lecture est un remplacement sans termes ni instances identifiés. Il faut conserver le lien entre la formule quantifiée, les instances choisies et le test propositionnel final.

Une carrière très brève n'est pas une œuvre mineure. Herbrand meurt à vingt-trois ans en 1931, mais laisse une dizaine d'articles et plusieurs contributions fondatrices. Il faut juger cette œuvre par ses résultats, non par sa durée.

Trois prolongements permettent de situer l'héritage de Jacques Herbrand : approfondir la réduction des formules du premier ordre à des tests propositionnels, étudier le théorème de Herbrand-Ribet en théorie des nombres, puis examiner le modèle de Herbrand-Gödel des fonctions récursives en théorie de la calculabilité.

Ces pistes correspondent à des contributions distinctes. Les suivre séparément évite d'attribuer au seul théorème de Herbrand tout ce que le logicien a apporté aux mathématiques.