Herbrand base

☆ Save On Wikipedia ↗

In first-order logic, a Herbrand structure S {\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 c {\displaystyle c} {\displaystyle c} is just " c {\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]

Herbrand universe

Definition

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

  1. The Herbrand universe of a first-order language L σ {\displaystyle L^{\sigma }} {\displaystyle L^{\sigma }}, is the set of all ground terms of L σ {\displaystyle L^{\sigma }} {\displaystyle L^{\sigma }}. If the language has no constants, then the language is extended by adding an arbitrary new constant.
    • The Herbrand universe is countably infinite if σ {\displaystyle \sigma } {\displaystyle \sigma } 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 σ {\displaystyle \sigma } {\displaystyle \sigma }.
  2. The Herbrand universe of a closed formula in Skolem normal form F {\displaystyle F} {\displaystyle F} is the set of all terms without variables that can be constructed using the function symbols and constants of F {\displaystyle F} {\displaystyle F}. If F {\displaystyle F} {\displaystyle F} has no constants, then F {\displaystyle F} {\displaystyle F} is extended by adding an arbitrary new constant.

Example

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

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

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

H = { c , f ( c ) , g ( c ) , f ( f ( c ) ) , f ( g ( c ) ) , g ( f ( c ) ) , g ( g ( c ) ) , … } {\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]

Herbrand structure

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

Definition

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

  1. U = W 0 {\displaystyle U=W_{0}} {\displaystyle U=W_{0}}
  2. f S ( t 1 , … , t n ) = f ( t 1 , … , t n ) {\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 n {\displaystyle n} {\displaystyle n}-ary function symbol f ∈ σ {\displaystyle f\in \sigma } {\displaystyle f\in \sigma } and t 1 , … , t n ∈ W 0 {\displaystyle t_{1},\dots ,t_{n}\in W_{0}} {\displaystyle t_{1},\dots ,t_{n}\in W_{0}}
  3. c S = c {\displaystyle c^{S}=c} {\displaystyle c^{S}=c} for every constant c {\displaystyle c} {\displaystyle c} in σ {\displaystyle \sigma } {\displaystyle \sigma }

Remarks

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

Examples

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

  • U = { c , f c , f f c , f f f c , … } {\displaystyle U=\{c,fc,ffc,fffc,\dots \}} {\displaystyle U=\{c,fc,ffc,fffc,\dots \}}
  • f c ↦ f c , f f c ↦ f f c , … {\displaystyle fc\mapsto fc,ffc\mapsto ffc,\dots } {\displaystyle fc\mapsto fc,ffc\mapsto ffc,\dots }
  • c ↦ c {\displaystyle c\mapsto c} {\displaystyle c\mapsto 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 B H {\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.

Examples

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

B H = { R ( c , c ) , R ( f c , c ) , R ( c , f c ) , R ( f c , f c ) , R ( f f c , c ) , … } {\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 \}}

See also

Notes

  1. "Herbrand Semantics". Archived from the original on 2017-05-23. Retrieved 2017-04-05.
  2. Formulas consisting only of relations R {\displaystyle R} {\displaystyle R} evaluated at a set of constants or variables correspond to subsets of finite powers of the universe H n {\displaystyle H^{n}} {\displaystyle H^{n}} where n {\displaystyle n} {\displaystyle n} is the arity of R {\displaystyle R} {\displaystyle R}.

References