Herbrand structure

Herbrand structure

In mathematics, for a language \mathcal{L}, define the Herbrand universe to be the set of ground terms of \mathcal{L}.

A structure \mathfrak{M} for \mathcal{L} is a 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.

A Herbrand model of a theory T is a Herbrand structure which is a model of T.

See also


This article incorporates material from Herbrand structure on PlanetMath, which is licensed under the Creative Commons Attribution/Share-Alike License.