# Herbrand structure

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.
* The Herbrand universe of a first-order language $L^{\sigma }$, is the set of all ground terms of $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 $\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 $\sigma$.
* The Herbrand universe of a closed formula in Skolem normal form $F$ is the set of all terms without variables that can be constructed using the function symbols and constants of $F$. If $F$ has no constants, then $F$ is extended by adding an arbitrary new constant. This second definition is important in the context of computational resolution.

### 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
* $U=W_{0}$
* $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}$
* $c^{S}=c$ for every constant $c$ in $\sigma$

### Remarks

* $U$ is the Herbrand universe of $\sigma$.
* 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 § 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 ${\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 $R$, we get with the terms from above:
    ${\mathcal {B}}_{H}=\{R(c,c),R(fc,c),R(c,fc),R(fc,fc),R(ffc,c),\dots \}$