L'ensemble de tous les termes sans variables (termes ground) pouvant être construits à partir des symboles de constantes et de fonctions d'un langage du premier ordre.

Principe

Construire la plus petite algèbre de termes fermée par les symboles du vocabulaire : on ferme l'ensemble des constantes par application répétée des symboles de fonctions sans introduire de variables.

Démonstration

Pour un vocabulaire contenant la constante a et la fonction unaire f, l'univers d'Herbrand est {a, f(a), f(f(a)), ...}, un ensemble souvent infini obtenu en appliquant f récursivement sur a.

Mauvaise application

Confondre l'univers d'Herbrand avec un domaine sémantique peuplé d'objets interprétés ou supposer qu'il est fini alors que des symboles de fonctions non triviaux génèrent une infinité de termes.

Conséquence

Fournit un domaine purement syntaxique pour fabriquer des instances ground de formules et définir des interprétations et modèles d'Herbrand, outils centraux en preuve automatique et en programmation logique.

Inversion

Au lieu de la clôture en termes ground, considérer l'ensemble des termes contenant des variables ou un domaine interprété — l'attention passe alors de la construction syntaxique des termes à l'interprétation sémantique ou aux schémas à variables.

Limite

Ne contient que les termes ground formés avec les constantes et fonctions du langage ; exclut les variables, les symboles de prédicat, les méta-termes et tout symbole externe à la signature, et ne porte pas en soi d'évaluation de vérité.

Tension sémantique

Tension entre l'univers d'Herbrand comme algèbre de termes purement syntaxique et la notion de domaine en théorie des modèles : deux usages du concept de 'domaine' qui ne désignent pas la même chose.

Synthèse

L'univers d'Herbrand est l'univers syntaxique des termes ground engendrés par les constantes et fonctions du langage ; il sert de base pour mettre à plat les formules, construire la base d'Herbrand et relier méthodes de preuve syntaxiques et raisonnements sémantiques.