Logic for Computer Scientists/Predicate Logic/Herbrand Theories
Herbrand Theories
editUntil now we considered arbitrary interpretations of formulae in predicate logics. In particular we sometimes used numbers as interpretation domain and functions, like addition or successor. In the following, we will concentrate on a special case, the Herbrand interpretation and we will discuss their relation to the general case.
Definition 11
editLet be a set of clauses. The Herbrand universe for is given by:
- All constants which occur in are in (if no constant appears in , we assume a single constant, say to be in ).
- For every -ary function symbol in and every , .
Examples: Given the clause set , we construct the Herbrand universe
For the clause set we get the Herbrand universe .
Definition 12
editLet be a set of clauses. An interpretation is an Herbrand interpretation iff
- For every -ary function symbol ( ) and
Note, that there is no restriction on the assignments of relations to predicate symbols (except, that, of course, they have to be relations over the Herbrand universe ).
In order to discuss the interpretation of predicate symbols, we need the notion of Herbrand basis.
Definition 13
editA ground atom or a ground term is an atom or a term without an occurrence of a variable. The Herbrand basis for a set of clauses is the set of ground atoms , where is a -ary predicate symbol from and
We will notate the assignments of relations to predicate symbols by
simply giving a set , where each
element is a literal with its atom is from the Herbrand basis.
Examples:
Definition 14
editLet be an interpretation for a set of clauses ; the Herbrand interpretation corresponding to is a Herbrand interpretation satisfying the following condition: Let be Elements from the Herbrand universe for . By the interpretation every is mapped to a . If , then have to be assigned in .
Let us now state a simple, very obvious lemma, which will help us, to focus on Herbrand interpretation in the following.
Lemma 4
editIf is a model for a set of clauses, then every corresponding Herbrand interpretation is a model for
Theorem 4
editA set of clauses is unsatisfiable iff there is no Herbrand model for .
Proof: If is unsatisfiable, there is obviously no Herbrand
model for .
Assume that there is no Herbrand model for and that is
satisfiable. Then, there is a model for and according to
lemma 4 the corresponding Herbrand
interpretation is a model for , which is a
contradiction.