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

Définition

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.

Exemple

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

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

Définition

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 σ

Remarques

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.

Exemple

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 }$

Base de Herbrand

Une base de Herbrand complète l'interprétation d'un univers et d'une structure de Herbrand en y ajoutant les symboles de relation.

Définition

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

Exemples

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 \}}$

Notes et références

1. « Herbrand Semantics »