# Herbrand structure

For a language^{} $\mathcal{L}$, define the *Herbrand universe* to be the set of closed terms (alternatively ground terms) of $L$.

A structure^{} $\U0001d510$ for $\mathcal{L}$ is a *Herbrand structure* if the domain of $\U0001d510$ is the Herbrand universe of $\mathcal{L}$. This fixes the domain of $\U0001d510$, 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$.

Title | Herbrand structure |
---|---|

Canonical name | HerbrandStructure |

Date of creation | 2013-03-22 14:33:13 |

Last modified on | 2013-03-22 14:33:13 |

Owner | iwnbap (1760) |

Last modified by | iwnbap (1760) |

Numerical id | 4 |

Author | iwnbap (1760) |

Entry type | Definition |

Classification | msc 03B10 |

Synonym | HerbrandModel HerbrandInterpretation |

Related topic | HerbrandsTheoremFirstOrderLogic |

Defines | HerbrandModel HerbrandInterpretation HerbrandUniverse |