In first-order logic, a Herbrand structure is a structure over a vocabulary (also sometimes called a signature) 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 "" (the symbol). It is named after Jacques Herbrand.

Herbrand structures play an important role in the foundations of logic programming.[1]

Herbrand universe

edit

Definition

edit

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

  1. The Herbrand universe of a first-order language  , is the set of all ground terms of  . 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   is the set of all terms without variables that can be constructed using the function symbols and constants of  . If   has no constants, then   is extended by adding an arbitrary new constant.

Example

edit

Let  , be a first-order language with the vocabulary

  • constant symbols:  
  • function symbols:  

then the Herbrand universe   of   (or 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.[2]

Herbrand structure

edit

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

Definition

edit

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

  1.  
  2.   for every  -ary function symbol   and  
  3.   for every constant   in  

Remarks

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

Examples

edit

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

  •  
  •  
  •  

Herbrand base

edit

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

edit

A Herbrand base   for a Herbrand structure is the set of all atomic formulas whose argument terms are elements of the Herbrand universe.

Examples

edit

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

 

See also

edit

Notes

edit
  1. ^ "Herbrand Semantics".
  2. ^ Formulas consisting only of relations   evaluated at a set of constants or variables correspond to subsets of finite powers of the universe   where   is the arity of  .

References

edit