Herbrand structure

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

Herbrand structures play an important role in the foundations of logic programming.^[1]

Herbrand universe

Definition

The Herbrand universe serves as the universe in a Herbrand structure.

1. The Herbrand universe of a first-order language ${\displaystyle L^{\sigma }}$, is the set of all ground terms of ${\displaystyle L^{\sigma }}$. If the language has no constants, then the language is extended by adding an arbitrary new constant.

   • The Herbrand universe is countably infinite if ${\displaystyle \sigma }$ is countable and a function symbol of arity greater than 0 exists.
   • In the context of first-order languages we also speak simply of the Herbrand universe of the vocabulary ${\displaystyle \sigma }$.
2. The Herbrand universe of a closed formula in Skolem normal form ${\displaystyle F}$ is the set of all terms without variables that can be constructed using the function symbols and constants of ${\displaystyle F}$. If ${\displaystyle F}$ has no constants, then ${\displaystyle F}$ is extended by adding an arbitrary new constant.

   • This second definition is important in the context of computational resolution.

Example

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

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

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

${\displaystyle 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.^[2]

Herbrand structure

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

Definition

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

1. ${\displaystyle U=W_{0}}$
2. ${\displaystyle f^{S}(t_{1},\dots ,t_{n})=f(t_{1},\dots ,t_{n})}$ for every ${\displaystyle n}$-ary function symbol ${\displaystyle f\in \sigma }$ and ${\displaystyle t_{1},\dots ,t_{n}\in W_{0}}$
3. ${\displaystyle c^{S}=c}$ for every constant ${\displaystyle c}$ in ${\displaystyle \sigma }$

Remarks

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

Examples

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

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

Herbrand base

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

Definition

A Herbrand base ${\displaystyle {\mathcal {B}}_{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 ${\displaystyle R}$, we get with the terms from above:

${\displaystyle {\mathcal {B}}_{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