Structure de Herbrand

En logique du premier ordre, une Structure de Herbrand S est une structure sur un vocabulaire σ qui est défini uniquement par les propriétés syntaxiques de σ. L'idée étant de se contenter de prendre les symboles des termes comme leurs valeurs. Ainsi la valeur d'un symbole constant c est juste "c"(en tant que symbole). Ces structures tirent leur nom du mathématicien français Jacques Herbrand.

Les structures de Herbrand jouent un rôle important dans les fondations de la programmation logique^[1].

Univers de Herbrand[modifier | modifier le code]

Définition[modifier | modifier le code]

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

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 $σ$ .
L'univers de Herbrand d'une formule close en forme normale de Skolem $F$ $F$ est l'ensemble de tous les termes sans variable qui peuvent être construit en utilisant les symboles de fonctions et les constantes de $F$ $F$ . Si $F$ $F$ n'a pas de constante, on en ajoute une.
- Cette seconde définition est importante dans le cadre du calcul de résolution.

Exemple[modifier | modifier le code]

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.

Structure de Herbrand[modifier | modifier le code]

Une structure de Herbrand interprète les termes d'un univers de Herbrand.

Définition[modifier | modifier le code]

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 :

$U = W 0$
$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 \in σ$ et $t 1, ..., t n \in W 0$
c^S = c pour toute constante c dans σ