Herbrand structure

In first-order logic, a Herbrand structure

S

{\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

c

{\displaystyle c}

is just "

c

{\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.

Example

Let

L

σ

{\displaystyle L^{\sigma }}

, be a first-order language with the vocabulary

constant symbols:

c

{\displaystyle c}

function symbols:

f

(

⋅

)

,

g

(

⋅

)

{\displaystyle f(\cdot ),\,g(\cdot )}

then the Herbrand universe

H

{\displaystyle H}

of

L

σ

{\displaystyle L^{\sigma }}

(or of

σ

{\displaystyle \sigma }

) is

H

=

{

c

,

f

(

c

)

,

g

(

c

)

,

f

(

f

(

c

)

)

,

f

(

g

(

c

)

)

,

g

(

f

(

c

)

)

,

g

(

g

(

c

)

)

,

…

}

{\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

S

{\displaystyle S}

be a structure, with vocabulary

σ

{\displaystyle \sigma }

and universe

U

{\displaystyle U}

. Let

W

{\displaystyle W}

be the set of all terms over

σ

{\displaystyle \sigma }

and

W

0

{\displaystyle W_{0}}

be the subset of all variable-free terms.