Herbrand structure

Please help to eliminate the shortcomings of this article, and please take part you in the discussion! (Insert item)

A right to a predicate logic formula set F structure is called Herbrand structure if the following properties are satisfied:

• The universe is generated from F Herbrand universe, ie.
• The interpretations I are Herbrand interpretations.

In an interpretation of the function and constant symbols actual functions and constants are assigned. In the Herbrand interpretation one assigns to each function term to an interpretation by itself. This is possible because the Herbrand universe consists exactly of the set of all possible terms with function and constant symbols. This is a Herbrand structure is a term interpretation.

Example: Let the Herbrand universe. Then the mapping between function symbols and elements is from the universe:

Herbrand structures are used in the set of Herbrand and are named after Jacques Herbrand.