Herbrand structure

In first-order logic, a Herbrand structure is a structure over a vocabulary that is defined solely by the syntactical properties of . The idea is to take the symbol strings of terms as their values, e.g. the denotation of a constant symbol is just "". 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.

Example

Let, be a first-order language with the vocabulary

constant symbols:
function symbols:

then the Herbrand universe of is
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 be a structure, with vocabulary and universe. Let be the set of all terms over and be the subset of all variable-free terms. is said to be a Herbrand structure iff

for every -ary function symbol and
for every constant in

Remarks

is the Herbrand universe of.
A Herbrand structure that is a model of a theory is called a Herbrand model of.

Examples

For a constant symbol and a unary function symbol we have the following interpretation:
*

Herbrand base

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

Definition

A Herbrand base 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, we get with the terms from above: