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.

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.

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

Notes

1. "Herbrand Semantics". Archived from the original on 2017-05-23. Retrieved 2017-04-05.
2. Formulas consisting only of relations ${\displaystyle R}$ evaluated at a set of constants or variables correspond to subsets of finite powers of the universe ${\displaystyle H^{n}}$ where ${\displaystyle n}$ is the arity of ${\displaystyle R}$.