Herbrand structure

From Wikipedia, the free encyclopedia

In mathematical logic, Herbrand's theorem is a basic result of Jacques Herbrand from the 1920s. For a language $\mathcal{L}$ , define the Herbrand universe to be the set of closed terms (alternatively ground terms) of $\mathcal{L}$ .

A structure $\mathfrak{M}$ for $\mathcal{L}$ is an Herbrand structure if the domain of $\mathfrak{M}$ is the Herbrand universe of $\mathcal{L}.$ This fixes the domain of $\mathfrak{M}$ , and so each Herbrand structure can be identified with its interpretation, leading to the alternative nomenclature of Herbrand interpretation.