Herbrand Base

In first-order logic, a Herbrand structure $S$ is a structure over a vocabulary $\sigma$ (also sometimes called a ''signature'') that is defined solely by the syntactical properties of $\sigma$. The idea is to take the symbol strings of terms as their values, e.g. the denotation of a constant symbol $c$ is just "$c$" (the symbol). It is named after Jacques Herbrand.

Herbrand structures play an important role in the foundations of logic programming.

Herbrand universe

Definition

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

Example

Let $L^\sigma$, be a first-order language with the vocabulary
* constant symbols: $c$
* function symbols: $f(\cdot), \, g(\cdot)$
then the Herbrand universe $H$ of $L^\sigma$ (or of $\sigma$) is

$H = \$

The relation symbols are not relevant for a Herbrand universe since formulas involving only relations do not correspond to elements of the universe.

Formulas consisting only of relations $R$ evaluated at a set of constants or variables correspond to subsets of finite powers of the universe $H^n$ where $n$ is the arity of $R$.

Herbrand structure

A ''Herbrand structure'' interprets terms on top of a ''Herbrand universe''.

Definition

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

# $U = W_0$
# $f^S(t_1,\dots,t_n) = f(t_1,\dots,t_n)$ for every $n$-ary function symbol $f \in \sigma$ and $t_1,\dots,t_n \in W_0$
# $c^S = c$ for every constant $c$ in $\sigma$

Remarks

# $U$ is the Herbrand universe of $\sigma$.
# A Herbrand structure that is a model of a theory $T$ is called a ''Herbrand model'' of $T$.

Examples

For a constant symbol $c$ and a unary function symbol $f(\,\cdot\,)$ we have the following interpretation:

* $U = \$
* $fc \mapsto fc, ffc \mapsto ffc, \dots$
* $c \mapsto c$

Herbrand base

In addition to the universe, defined in , and the term denotations, defined in , the ''Herbrand base'' completes the interpretation by denoting the relation symbols.

Definition

A ''Herbrand base'' $\mathcal B_H$ for a Herbrand structure is the set of all atomic formulas whose argument terms are elements of the Herbrand universe.

Examples

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

: $\mathcal B_H = \$

See also

* Herbrand's theorem
* Herbrandization
* Herbrand interpretation

Notes

References

* {{cite book
, last1=Ebbinghaus
, first1=Heinz-Dieter
, authorlink1=Heinz-Dieter Ebbinghaus
, last2=Flum
, first2=Jörg
, last3=Thomas
, first3=Wolfgang
, title=Mathematical Logic
, publisher=Springer
, isbn=978-0387942582
, year=1996
, url-access=registration
, url=https://archive.org/details/mathematicallogi1996ebbi

Mathematical logic