# Logic for Computer Scientists/Predicate Logic/Herbrand Theories

## Herbrand TheoriesEdit

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 11Edit

Let ${\displaystyle S}$  be a set of clauses. The Herbrand universe ${\displaystyle U_{H}}$  for ${\displaystyle S}$  is given by:

• All constants which occur in ${\displaystyle S}$  are in ${\displaystyle U_{H}}$  (if no constant appears in ${\displaystyle S}$ , we assume a single constant, say ${\displaystyle a}$  to be in ${\displaystyle U_{H}}$ ).
• For every ${\displaystyle n}$ -ary function symbol ${\displaystyle f}$  in ${\displaystyle S}$  and every ${\displaystyle t_{1},\cdots ,t_{n}\in U_{H}}$ , ${\displaystyle f(t_{1},\cdots ,t_{n})\in U_{H}}$ .

Examples: Given the clause set ${\displaystyle S_{1}=\{P(a),\lnot P(x)\lor P(f(x))\}}$ , we construct the Herbrand universe

${\displaystyle U_{H}=\{a,f(a),f(f(a)),f(f(f(a))),\cdots \}}$

For the clause set ${\displaystyle S_{2}=\{P(x)\lor Q(x),R(z)\}}$  we get the Herbrand universe ${\displaystyle U_{H}=\{a\}}$ .

## Definition 12Edit

Let ${\displaystyle S}$  be a set of clauses. An interpretation ${\displaystyle {\mathcal {I}}=(U_{\mathcal {I}},A_{\mathcal {I}})}$  is an Herbrand interpretation iff

• ${\displaystyle U_{\mathcal {I}}=U_{H}}$
• For every ${\displaystyle n}$ -ary function symbol (${\displaystyle n\geq 0}$ ) ${\displaystyle f}$  and ${\displaystyle t_{1},\cdots ,t_{n}\in U_{H}}$
${\displaystyle f^{\mathcal {I}}(t_{1},\cdots ,t_{n})=f(t_{1},\cdots ,t_{n})}$

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 ${\displaystyle U_{H}}$ ).

In order to discuss the interpretation of predicate symbols, we need the notion of Herbrand basis.

## Definition 13Edit

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 ${\displaystyle S}$  is the set of ground atoms ${\displaystyle p(t_{1},\ldots ,t_{n})}$ , where ${\displaystyle p}$  is a ${\displaystyle n}$ -ary predicate symbol from ${\displaystyle S}$  and ${\displaystyle t_{1},\ldots ,t_{n}\in U_{H}}$

We will notate the assignments of relations to predicate symbols by simply giving a set ${\displaystyle I=\{m_{1},m_{2},\cdots ,m_{n},\cdots \}}$ , where each element is a literal with its atom is from the Herbrand basis.

Examples:

• ${\displaystyle S=\{p(x)\lor q(x),r(f(y))\}}$
• ${\displaystyle U_{H}=\{a,f(a),f(f(a)),\ldots \}}$
• ${\displaystyle I=\{p(a),q(a),r(a),p(f(a)),q(f(a)),r(f(a)),\cdots \}}$

## Definition 14Edit

Let ${\displaystyle {\mathcal {I}}=(U_{\mathcal {I}},A_{\mathcal {I}})}$  be an interpretation for a set of clauses ${\displaystyle S}$ ; the Herbrand interpretation ${\displaystyle {\mathcal {I}}^{*}}$  corresponding to ${\displaystyle {\mathcal {I}}}$  is a Herbrand interpretation satisfying the following condition: Let ${\displaystyle t_{1},\ldots ,t_{n}}$  be Elements from the Herbrand universe ${\displaystyle U_{H}}$  for ${\displaystyle S}$ . By the interpretation ${\displaystyle {\mathcal {I}}}$  every ${\displaystyle t_{i}}$  is mapped to a ${\displaystyle d_{i}\in U_{\mathcal {I}}}$ . If ${\displaystyle p^{\mathcal {I}}(d_{1},\ldots ,d_{n})=true(false)}$ , then ${\displaystyle p(t_{1},\ldots ,t_{n})}$  have to be assigned ${\displaystyle true(false)}$  in ${\displaystyle {\mathcal {I}}^{*}}$ .

Let us now state a simple, very obvious lemma, which will help us, to focus on Herbrand interpretation in the following.

## Lemma 4Edit

If ${\displaystyle {\mathcal {I}}}$  is a model for a set of clauses, then every corresponding Herbrand interpretation ${\displaystyle {\mathcal {I}}^{*}}$  is a model for ${\displaystyle S}$

## Theorem 4Edit

A set of clauses ${\displaystyle S}$  is unsatisfiable iff there is no Herbrand model for ${\displaystyle S}$ .

Proof: If ${\displaystyle S}$  is unsatisfiable, there is obviously no Herbrand model for ${\displaystyle S}$ .
Assume that there is no Herbrand model for ${\displaystyle S}$  and that ${\displaystyle S}$  is satisfiable. Then, there is a model ${\displaystyle {\mathcal {I}}}$  for ${\displaystyle S}$  and according to lemma 4 the corresponding Herbrand interpretation ${\displaystyle {\mathcal {I}}^{*}}$  is a model for ${\displaystyle S}$ , which is a contradiction.