Herbrand structure
In first-order logic, a Herbrand structure S is a structure over a vocabulary σ that is defined solely by the syntactical properties of σ. 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.[1]
Herbrand universe
Definition
The Herbrand universe serves as the universe in the Herbrand structure.
- The Herbrand universe of a first-order language Lσ, is the set of all ground terms of Lσ. If the language has no constants, then the language is extended by adding an arbitrary new constant.
- The Herbrand universe is countably infinite if σ is countable and a function symbol of arity greater than 0 exists.
- In the context of first-order languages we also speak simply of the Herbrand universe of the vocabulary σ.
- The Herbrand universe of a closed formula in Skolem normal form F is the set of all terms without variables that can be constructed using the function symbols and constants of F. If F has no constants, then F is extended by adding an arbitrary new constant.
- This second definition is important in the context of computational resolution.
Example
Let Lσ, be a first-order language with the vocabulary
- constant symbols: c
- function symbols: f(·), g(·)
then the Herbrand universe of Lσ (or σ) is {c, f(c), g(c), f(f(c)), f(g(c)), g(f(c)), g(g(c)), ...}.
Notice that the relation symbols are not relevant for a Herbrand universe.
Herbrand structure
A Herbrand structure interprets terms on top of a Herbrand universe.
Definition
Let S be a structure, with vocabulary σ and universe U. Let W be the set of all terms over σ and W0 be the subset of all variable-free terms. S is said to be a Herbrand structure iff
- U = W0
- fS(t1, ..., tn) = f(t1, ..., tn) for every n-ary function symbol f ∈ σ and t1, ..., tn ∈ W0
- cS = c for every constant c in σ
Remarks
- U is the Herbrand universe of σ.
- 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(.) we have the following interpretation:
- U = {c, fc, ffc, fffc, ...}
- fc → fc, ffc → ffc, ...
- c → c
Herbrand base
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.
Definition
A Herbrand base is the set of all ground atoms whose argument terms are elements of the Herbrand universe.
Examples
For a binary relation symbol R, we get with the terms from above:
- {R(c, c), R(fc, c), R(c, fc), R(fc, fc), R(ffc, c), ...}
See also
Notes
References
- Ebbinghaus, Heinz-Dieter; Flum, Jörg; Thomas, Wolfgang (1996). Mathematical Logic. Springer. ISBN 978-0387942582.