Herbrand Universe

from Wikipedia, the free encyclopedia

The Herbrand universe is a set in predicate logic that is used as a basic set to define the Herbrand structure . Both terms are part of the Herbrand theorem , named after Jacques Herbrand .


Let be a (closed) formula in adjusted Skolem form . The Herbrand universe , denoted by , is the smallest set of terms that meets the following conditions:

  1. If is a constant occurring in , then is .
  2. If no constant occurs in , a new constant is introduced and included in.
  3. is inductively defined by . There is a set of terms that can be formed using the function symbols occurring in and the terms that have already been constructed . Let, for example, be such an n-place function symbol and let terms be off , then is . Every term that can be formed from function symbols and terms is an element of .

The Herbrand universe results from this :


F denote a predicate logic formula with

arises to

One can see that just one function symbol in leads to an infinite number of terms.

Example 2

F denote a predicate logic formula with

The respective subsets look like this:

(Constant a was introduced and inserted in)

Example 3

F denote a predicate logic formula with

See also