In first-order logic, a **Herbrand structure** *S* is a structure over a vocabulary σ that is defined solely by the syntactical properties of σ. The idea is to take the symbols 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.^{[1]}

## Herbrand universe

### Definition

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

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

- The Herbrand universe is countably infinite if σ 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 σ.

(2) 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*^{σ} be a first-order language with the vocabulary

- constant symbols:
*c* - function symbols:
*f*(.),*g*(.)

then the Herbrand universe of *L*^{σ} (or σ) is {*c*, *f*(*c*), *g*(*c*), *f*(*f*(*c*)), *f*(*g*(*c*)), *g*(*f*(*c*)), *g*(*g*(*c*)), ...}.

Notice that the relation symbols are not relevant for a Herbrand universe.

## Herbrand structure

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

### Definition

Let *S* be a structure, with vocabulary σ and universe *U*. Let *T* be the set of all terms over σ and *T*_{0} be the subset of all variable-free terms. *S* is said to be a *Herbrand structure* iff

*U*=*T*_{0}*f*^{ S}(*t*_{1}, ...,*t*_{n}) =*f*(*t*_{1}, ...,*t*_{n}) for every*n*-ary function symbol*f*∈ σ and*t*_{1}, ...,*t*_{n}∈*T*_{0}*c*^{S}=*c*for every constant*c*in σ

### Remarks

*U*is the Herbrand universe of σ.- A Herbrand structure that is a model of a theory
*T*, is called the*Herbrand model*of*T*.

### Examples

For a constant symbol *c* and a unary function symbol *f*(.) we have the following interpretation:

*U*= {*c*,*fc*,*ffc*,*fffc*, ...}*fc*→*fc*,*ffc*→*ffc*, ...*c*→*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* is the set of all ground atoms of whose argument terms are the Herbrand universe.

### Examples

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

{*R*(*c*, *c*), *R*(*fc*, *c*), *R*(*c*, *fc*), *R*(*fc*, *fc*), *R*(*ffc*, *c*), ...}

## See also

## Notes

## References

- Ebbinghaus, Heinz-Dieter; Flum, Jörg; Thomas, Wolfgang (1996).
*Mathematical Logic*. Springer. ISBN 978-0387942582. CS1 maint: discouraged parameter (link)