Herbrand structure

The Herbrand universe serves as the universe in the Herbrand structure.

Let L^σ, be a first-order language with the vocabulary

• constant symbols: c
• function symbols: f(·), g(·)

then the Herbrand universe of L^σ (or σ) is {c, f(c), g(c), f(f(c)), f(g(c)), g(f(c)), g(g(c)), ...}.

Notice that the relation symbols are not relevant for a Herbrand universe.

Let S be a structure, with vocabulary σ and universe U. Let W be the set of all terms over σ and W₀ be the subset of all variable-free terms. S is said to be a Herbrand structure iff

1. U = W₀
2. f^S(t₁, ..., t_n) = f(t₁, ..., t_n) for every n-ary function symbol f ∈ σ and t₁, ..., t_n ∈ W₀
3. c^S = c for every constant c in σ

1. U is the Herbrand universe of σ.
2. A Herbrand structure that is a model of a theory T is called a Herbrand model of T.

For a constant symbol c and a unary function symbol f(.) we have the following interpretation:

• U = {c, fc, ffc, fffc, ...}
• fc → fc, ffc → ffc, ...
• c → c

A Herbrand base is the set of all ground atoms whose argument terms are elements of the Herbrand universe.

For a binary relation symbol R, we get with the terms from above:

{R(c, c), R(fc, c), R(c, fc), R(fc, fc), R(ffc, c), ...}