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

If is a constant occurring in , then is .${\ displaystyle c}$${\ displaystyle F}$${\ displaystyle c \ in H_ {0}}$

If no constant occurs in , a new constant is introduced and included in.${\ displaystyle F}$${\ displaystyle a}$${\ displaystyle H_ {0}}$

${\ 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}$