Structure de Herbrand

L'Univers de Herbrand sert d'univers pour les Structures de Herbrand.

1. L'univers de Herbrand d'un langage du premier ordre L^σ est l'ensemble des termes clos de L^σ. Si le langage est dépourvu de constante, on l'étend alors en y ajoutant une constante arbitraire.
   • L'univers de Herbrand est infiniment dénombrable si σ est dénombrable et qu'il existe un symbole de fonction d'arité strictement supérieur à 0.
   • Dans le contexte des langages du premier ordre, on parle aussi simplement de l'univers de Herbrand du vocabulaire σ.
2. L'univers de Herbrand d'une formule close en forme normale de Skolem ${\displaystyle F}$ est l'ensemble de tous les termes sans variable qui peuvent être construit en utilisant les symboles de fonctions et les constantes de ${\displaystyle F}$. Si ${\displaystyle F}$ n'a pas de constante, on en ajoute une.
   • Cette seconde définition est importante dans le cadre du calcul de résolution.

Soit L^σ, un langage du premier ordre avec le vocabulaire constitué :

• du symbole constant: c
• des symboles de fonction: f(·), g(·)

l'univers de Herbrand de L^σ (ou σ) est alors : {c, f(c), g(c), f(f(c)), f(g(c)), g(f(c)), g(g(c)), ...}.

Notez que les symboles de relation ne sont pas pertinents pour l'univers de Herbrand.

Soit S une structure, avec un vocabulaire σ et un univers U. Soit W l'ensemble des termes sur σ et W₀ le plus petit ensemble de termes clos. On dit que S est une structure de Herbrand si et seulement si :

1. U = W₀
2. ${\displaystyle f^{S}(t_{1},t_{2},\ldots ,f_{n})=f(t_{1},t_{2},\ldots ,f_{n})}$ pour tout symbole de fonction d'arité n f ∈ σ et t₁, ..., t_n ∈ W₀
3. c^S = c pour toute constante c dans σ

1. U est l'univers de Herbrand de σ.
2. Une structure de Herbrand qui est aussi le modèle d'une théorie T est appelée le modèle de Herbrand de T.

Pour un symbole de constante c et le symbole de fonction unaire f(.), on a l'interprétation suivante :

• ${\displaystyle U=\{c,fc,ffc,fffc,\ldots \}}$
• ${\displaystyle c\rightarrow c}$
• ${\displaystyle fc\rightarrow fc,ffc\rightarrow ffc,\ldots }$

Une base de Herbrand est l'ensemble de tous les atomes clos dont les arguments sont des termes de l'univers de Herbrand.

Soit le symbole de relation binaire R, en poursuivant l'exemple précédent, on obtient la base :

${\displaystyle \{R(c,c),R(c,fc),R(fc,c),R(fc,fc),R(ffc,c),\ldots \}}$