Term algebra

With Herbrand universe is referred to a lot in the predicate logic, which is used as the base amount for the definition of Herbrand structure. Both terms are part of the Herbrand theorem, named after Jacques Herbrand.

Definition

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

From this the Herbrand universe given by:

Example

F denote a predicate logic formula with

Is given by

One can see that already a function symbol leads to an infinite set of terms.