Herbrand structure

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

Herbrand structures play an important role in the foundations of logic programming.^[1]

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

Let ${\displaystyle L^{\sigma }}${\displaystyle L^{\sigma }}, be a first-order language with the vocabulary

• constant symbols: ${\displaystyle c}${\displaystyle c}
• function symbols: ${\displaystyle f(\cdot ),,円g(\cdot )}${\displaystyle f(\cdot ),,円g(\cdot )}

then the Herbrand universe ${\displaystyle H}${\displaystyle H} of ${\displaystyle L^{\sigma }}${\displaystyle L^{\sigma }} (or of ${\displaystyle \sigma }${\displaystyle \sigma }) is

${\displaystyle H=\{c,f(c),g(c),f(f(c)),f(g(c)),g(f(c)),g(g(c)),\dots \}}${\displaystyle H=\{c,f(c),g(c),f(f(c)),f(g(c)),g(f(c)),g(g(c)),\dots \}}

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

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

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

1. ${\displaystyle U=W_{0}}${\displaystyle U=W_{0}}
2. ${\displaystyle f^{S}(t_{1},\dots ,t_{n})=f(t_{1},\dots ,t_{n})}${\displaystyle f^{S}(t_{1},\dots ,t_{n})=f(t_{1},\dots ,t_{n})} for every ${\displaystyle n}${\displaystyle n}-ary function symbol ${\displaystyle f\in \sigma }${\displaystyle f\in \sigma } and ${\displaystyle t_{1},\dots ,t_{n}\in W_{0}}${\displaystyle t_{1},\dots ,t_{n}\in W_{0}}
3. ${\displaystyle c^{S}=c}${\displaystyle c^{S}=c} for every constant ${\displaystyle c}${\displaystyle c} in ${\displaystyle \sigma }${\displaystyle \sigma }

1. ${\displaystyle U}${\displaystyle U} is the Herbrand universe of ${\displaystyle \sigma }${\displaystyle \sigma }.
2. A Herbrand structure that is a model of a theory ${\displaystyle T}${\displaystyle T} is called a Herbrand model of ${\displaystyle T}${\displaystyle T}.

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

• ${\displaystyle U=\{c,fc,ffc,fffc,\dots \}}${\displaystyle U=\{c,fc,ffc,fffc,\dots \}}
• ${\displaystyle fc\mapsto fc,ffc\mapsto ffc,\dots }${\displaystyle fc\mapsto fc,ffc\mapsto ffc,\dots }
• ${\displaystyle c\mapsto c}${\displaystyle c\mapsto c}

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

A Herbrand base ${\displaystyle {\mathcal {B}}_{H}}${\displaystyle {\mathcal {B}}_{H}} for a Herbrand structure is the set of all atomic formulas whose argument terms are elements of the Herbrand universe.

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

${\displaystyle {\mathcal {B}}_{H}=\{R(c,c),R(fc,c),R(c,fc),R(fc,fc),R(ffc,c),\dots \}}${\displaystyle {\mathcal {B}}_{H}=\{R(c,c),R(fc,c),R(c,fc),R(fc,fc),R(ffc,c),\dots \}}

• Herbrand's theorem
• Herbrandization
• Herbrand interpretation

• Ebbinghaus, Heinz-Dieter; Flum, Jörg; Thomas, Wolfgang (1996). Mathematical Logic . Springer. ISBN 978-0387942582.

• Mathematical logic

• Articles with short description
• Short description matches Wikidata