# Herbrand Universe

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 .

## definition

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: ${\ displaystyle F}$ ${\ displaystyle F}$ ${\ displaystyle H_ {F}}$ 1. If is a constant occurring in , then is .${\ displaystyle c}$ ${\ displaystyle F}$ ${\ displaystyle c \ in H_ {0}}$ 2. If no constant occurs in , a new constant is introduced and included in.${\ displaystyle F}$ ${\ displaystyle a}$ ${\ displaystyle H_ {0}}$ 3. ${\ displaystyle H_ {k + 1}}$ 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 .${\ displaystyle H_ {k} \ cup G}$ ${\ displaystyle G}$ ${\ displaystyle F}$ ${\ displaystyle H_ {k}}$ ${\ displaystyle g}$ ${\ displaystyle t_ {1}, t_ {2}, ..., t_ {n}}$ ${\ displaystyle H_ {k}}$ ${\ displaystyle g (t_ {1}, t_ {2}, ..., t_ {n}) \ in H_ {k + 1}}$ ${\ displaystyle F}$ ${\ displaystyle H_ {k}}$ ${\ displaystyle H_ {k + 1}}$ The Herbrand universe results from this : ${\ displaystyle F}$ ${\ displaystyle H_ {F} = \ bigcup _ {k \ geq 0} H_ {k}}$ ### example

F denote a predicate logic formula with

${\ displaystyle F: = \ forall x \ forall y \ left (P \ left (x, a \ right) \ vee Q \ left (x, f \ left (y \ right) \ right) \ right)}$ ${\ displaystyle H_ {F}}$ arises to

${\ displaystyle H_ {F} = \ left \ {a, f \ left (a \ right), f \ left (f \ left (a \ right) \ right), \ ldots \ right \}}$ One can see that just one function symbol in leads to an infinite number of terms. ${\ displaystyle F}$ ### Example 2

F denote a predicate logic formula with

${\ displaystyle F: = \ forall x \ forall y \ left (f (x) \ vee g (y) \ right)}$ The respective subsets look like this:

${\ displaystyle H_ {0} = \ {a \}}$ (Constant a was introduced and inserted in)${\ displaystyle H_ {0}}$ ${\ displaystyle H_ {1} = \ {a, f (a), g (a) \}}$ ${\ displaystyle H_ {2} = \ {a, f (a), g (a), f (f (a)), f (g (a)), g (f (a)), g (g ( a)) \}}$ ${\ displaystyle H_ {3} = H_ {2} \ cup \ dots}$ ${\ displaystyle H_ {F} = \ lim _ {n \ to \ infty} H_ {n}}$ ### Example 3

F denote a predicate logic formula with

${\ displaystyle F: = \ forall x \ forall y \ left [F (x, a) \ vee \ neg G (b, f (y)) \ right]}$ ${\ displaystyle H_ {0} = \ {a, b \}}$ ${\ displaystyle H_ {1} = \ {a, b, f (a), f (b) \}}$ ${\ displaystyle H_ {2} = \ {a, b, f (a), f (b), f (f (a)), f (f (b)), \ dots \}}$ ${\ displaystyle \ dots}$ ${\ displaystyle H_ {F} = \ lim _ {n \ to \ infty} H_ {n} = H_ {0} \ cup H_ {1} \ cup H_ {2} \ cup {} \ dots}$ 