Herbrand domain

Stub grade: A

This page is a stub

This page is a stub, so it contains little or minimal information and is on a to-do list for being expanded.The message provided is:

Being created at the moment

---

TODO: Create redirects to this page, eg Hebrand universe, Herbrand terms, possibly term domain and ground terms

---

Definition

Let $\mathscr{L}$ be a first order language. We define the set $H$ (this will be the Herbrand domain of $\mathscr{L}$), a subset of all the terms of a FOL, $\mathscr{L}_T$, inductively using the following two rules:

1. If $c\in\mathscr{L}_c$ ($c$ is a constant symbol of $\mathscr{L}$) then $c\in H$
2. If $f\in\mathscr{L}_f$ is an $n$-ary function symbol of $\mathscr{L}$ and the terms $t_1,\ldots,t_n\in H$ then $ft_1\cdots t_n\in H$

The resulting $H$ is the Herbrand domain (AKA: Hebrand universe or term domain) of $\mathscr{L}$. The elements of $H$ are called Herbrand terms (AKA: ground terms)

See next

• Hintikka set - where this definition is actually used