Herbrand structure

Template:Short description In first-order logic, a Herbrand structure $S$ is a structure over a vocabulary $\sigma$ (also sometimes called a signature) that is defined solely by the syntactical properties of $\sigma$. The idea is to take the symbol strings of terms as their values, e.g. the denotation of a constant symbol $c$ is just "$c$" (the symbol). It is named after Jacques Herbrand.

Herbrand structures play an important role in the foundations of logic programming.

Herbrand universe

Definition

The Herbrand universe serves as the universe in a Herbrand structure. Template:Olist

Example

Let $L^{\sigma }$, be a first-order language with the vocabulary

• constant symbols: $c$
• function symbols: $f(\cdot ),g(\cdot )$

then the Herbrand universe $H$ of $L^{\sigma }$ (or of $\sigma$) is

$H=\{c,f(c),g(c),f(f(c)),f(g(c)),g(f(c)),g(g(c)),\dots \}$

The relation symbols are not relevant for a Herbrand universe since formulas involving only relations do not correspond to elements of the universe.

Herbrand structure

A Herbrand structure interprets terms on top of a Herbrand universe.

Definition

Let $S$ be a structure, with vocabulary $\sigma$ and universe $U$. Let $W$ be the set of all terms over $\sigma$ and $W_0$ be the subset of all variable-free terms. $S$ is said to be a Herbrand structure iff

1. $U=W_0$
2. $f^S(t_1,\dots ,t_n)=f(t_1,\dots ,t_n)$ for every $n$-ary function symbol $f\in \sigma$ and $t_1,\dots ,t_n\in W_0$
3. $c^S=c$ for every constant $c$ in $\sigma$

Remarks

1. $U$ is the Herbrand universe of $\sigma$.
2. A Herbrand structure that is a model of a theory $T$ is called a Herbrand model of $T$.

Examples

For a constant symbol $c$ and a unary function symbol $f(\cdot )$ we have the following interpretation:

• $U=\{c,fc,ffc,fffc,\dots \}$
• $fc\mapsto fc,ffc\mapsto ffc,\dots$
• $c\mapsto c$

Herbrand base

In addition to the universe, defined in Template:Sectionlink, and the term denotations, defined in Template:Sectionlink, the Herbrand base completes the interpretation by denoting the relation symbols.

Definition

A Herbrand base ${ℬ}_H$ for a Herbrand structure is the set of all atomic formulas whose argument terms are elements of the Herbrand universe.

Examples

For a binary relation symbol $R$, we get with the terms from above:

${ℬ}_H=\{R(c,c),R(fc,c),R(c,fc),R(fc,fc),R(ffc,c),\dots \}$

See also

• Herbrand's theorem
• Herbrandization
• Herbrand interpretation

References

• Template:Cite book