Logic for Computer Scientists/Predicate Logic/Herbrand Theories

Herbrand Theories Until 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 Let 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 Let 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 A 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 Let 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 If is a model for a set of clauses, then every corresponding Herbrand interpretation is a model for Theorem 4 A 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.