# 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}$