The Herbrand Universe and Herbrand Base

The Herbrand universe of a 1st order language is the set of all ground terms. If the language has no constants, then the language is extended by adding an arbitrary new constant. It is enumerable, and infinite (the same cardinality as the integers) if a functor of arity greater than 0 exists.

The Herbrand base of a 1st order language is the set of all ground atoms formed using elements of the Herbrand universe as arguments. Like the Herbrand universe, it is enumerable, and infinite if the Herbrand universe is infinite and there is a predicate symbol of arity greater than 0.

Example
The Herbrand universe and Herbrand base of the language 
V = { V : V starts with uppercase }
F = { geoff/0, jim/0, brother_of/1 }
P = { wise/1, taller/2 }
are 
HU = { geoff,
       jim,
       brother_of(geoff),
       brother_of(jim),
       brother_of(brother_of(geoff)),
       ... }
HB = { wise(geoff),
       taller(geoff,geoff),
       wise(jim),
       taller(jim,jim),
       taller(jim,geoff),
       taller(geoff,jim),
       taller(geoff,geoff),
       wise(brother_of(geoff)),
       taller(geoff,brother_of(geoff)),
       taller(brother_of(geoff),geoff),
       taller(brother_of(geoff),brother_of(geoff)),
       ... }

Herbrand Interpretations

A Herbrand interpretation has R defines a mapping from the Herbrand base to {TRUE,FALSE}.

Example
One possible Herbrand interpretation of the language 
V = { V : V starts with uppercase }
F = { geoff/0, jim/0, brother_of/1 }
P = { wise/1, taller/2 }
is 
D = { geoff,
      jim,
      brother_of(geoff),
      brother_of(jim),
      brother_of(brother_of(geoff)),
      ... }
F = { geoff → geoff,
      jim → jim,
      brother_of(geoff) → brother_of(geoff)),
      brother_of(jim) → brother_of(jim),
      ... }
R = { wise(geoff) → TRUE,
      taller(geoff,geoff) → TRUE,
      wise(jim) → TRUE,
      taller(jim,jim) → FALSE,
      taller(geoff,jim) → FALSE,
      taller(jim,geoff) → FALSE,
      wise(brother_of(geoff)) → TRUE,
      taller(geoff,brother_of(geoff)) → FALSE,
      taller(brother_of(geoff),geoff) → FALSE,
      taller(brother_of(geoff),brother_of(geoff)) → FALSE,
      ... }

As R is the only variable part of a Herbrand interpretation, it is possible to identify a Herbrand interpretation with R. The number of Herbrand Interpretations is the size power set of the Herbrand Base - in general the same cardinality as the reals.

Each branch of the semantic tree for the Herbrand base identifies a Herbrand interpretation. A semantic tree for a Herbrand interpretation is fair if the Herbrand Base elements are ordered so that no element is ignored for ever, e.g., ordered by by non-decreasing symbol count.

A Herbrand interpretation is a Herbrand model of a formula (set of formulae) iff the formula (each formula in the set) is TRUE in the Herbrand interpretation

A Herbrand interpretation removes the infinite number of domains, and leaves one infinite domain and a possibly infinite number of Rs.

Model Preservation

A set of clauses has a model iff it has a Herbrand model.

Proof
  • If a set of clauses has a Herbrand model then it has a model.
    This is proved by constructing a model from the Herbrand model. In the model
    • The domain is the Herbrand universe
    • The function mapping is the identity function
    • The predicate mapping is as in Herbrand model.

  • If a set of clauses has a model, then it has a Herbrand model.
    This is proved by constructing a Herbrand model H from the existing model M. Let the subset of the Herbrand base that is TRUE in H be the subset that is TRUE in M. Let C| be a clause that is TRUE in M, with universally quantified variables X1,...,Xn. It is necessary to show that C| is TRUE in H.
    • Let θ = {X1/t1,...,Xn/tn} be any Herbrand universe substitution (each ti is a Herbrand universe element) such that C|θ is ground.
    • Let ei be the interpretation of ti in M, and σ = {X1/e1,...,Xn/en}.
    • C|σ is TRUE (accepting the technical scrumple) in M, so C|θ is TRUE in M.
    • Let Lσ be a literal of C|σ that is TRUE in M (Lσ must exist), and let Lθ be the corresponding literal in C|θ.
    • By the definition of H, Lθ is TRUE in H. Thus C|θ is TRUE in H.
    • But θ is arbitrary, i.e., C|θ is TRUE in H for all θ.
    • Thus C| is TRUE in H, i.e., H is a Herbrand model of C|.

Example
Consider the clause C| ~taller(Person,jim) | wise(Person)
  • ~taller(Person,jim) | wise(Person) has the Herbrand model that interprets every Herbrand base element as TRUE. This Herbrand model is also a normal model.

  • ~taller(Person,jim) | wise(Person) is TRUE in the model M: 
    D = { ,  }
F = { geoff → ,
      jim → ,
      brother_of() → ,
      brother_of() →  }
R = { wise() → FALSE,
      wise() → TRUE,
      taller(,) → FALSE,
      taller(,) → FALSE,
      taller(,) → TRUE,
      taller(,) → FALSE }
    Let the subset of the Herbrand base that is TRUE in H be the subset that is TRUE in M. It is necessary to show that C| is TRUE in H.
    • Let θ = {Person/brother_of(brother_of(jim))} be a Herbrand universe substitution, and (~taller(Person,jim) | wise(Person))θ is the ground clause ~taller(brother_of(brother_of(jim)),jim) | wise(brother_of(brother_of(jim)))
    • is the interpretation of brother_of(brother_of(jim)) in M, and σ = {Person/}.
    • (~taller(Person,jim) | wise(Person)){Person/} = ~taller(,jim) | wise() is TRUE (accepting the technical scrumple) in M, so ~taller(brother_of(brother_of(jim)),jim) | wise(brother_of(brother_of(jim))) is TRUE in M.
    • wise() is a literal of ~taller(,jim) | wise() that is TRUE in M, and wise(brother_of(brother_of(jim))) is the corresponding literal in ~taller(brother_of(brother_of(jim)),jim) | wise(brother_of(brother_of(jim))).
    • By the definition of H, wise(brother_of(brother_of(jim))) is TRUE in H. Thus ~taller(brother_of(brother_of(jim))),jim) | wise(brother_of(brother_of(jim))) is TRUE in H.
    • But {Person/brother_of(brother_of(jim))} is arbitrary, i.e., (~taller(Person,jim) | wise(Person))θ is TRUE in H for all θ.
    • Thus ~taller(Person,jim) | wise(Person) is TRUE in H, i.e., H is a Herbrand model of ~taller(Person,jim) | wise(Person).

The above theorem does not hold for non-clauses, e.g. {p(a), ∃X ~p(X)} has the model: 

D = { 0,1 }
F = { a → 0 }
R = { p(0) → TRUE, 
      p(1) → FALSE }
but the only Herbrand interpretations are 
R = { p(a) → FALSE }
and 
R = { p(a) → TRUE }
neither of which are Herbrand models of the formulae. This is because a non-Herbrand model can have domain elements that do not represent any Herbrand universe element. Skolemization removes existentially quantified variables, and replaces them with terms. Ground instances of such Skolen terms are Herbrand universe elements which can be aligned with domain elements.

Unsatisfiability for sets of clauses can now be considered in terms of Herbrand interpretations.

The Quest for Logical Consequence

To show that C is a logical consequence of Ax, it is necessary to: Ax ∪ {~C} is unsatisfiable iff CNF(Ax ∪ {~C}) is unsatisfiable, so ... A set of clauses has a model iff it has a Herbrand model, so ...

An inference rule for clauses is sound if every Herbrand model of the parents is a Herbrand model of the inferred clauses, so ...

Exam Style Questions

  1. What are the Herbrand Universe and Herbrand Base of a 1st order language?
  2. Define the three components of a Herbrand interpretation of a 1st order language.
  3. Prove that a set of clauses has a model iff it has a Herbrand model.