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 $S$ be a set of clauses. The Herbrand universe $U_{H}$ for $S$ is given by:

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

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

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

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

Definition 12

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

• $U_{\mathcal {I}}=U_{H}$
• For every $n$-ary function symbol ($n\geq 0$) $f$ and $t_{1},\cdots ,t_{n}\in U_{H}$ $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 $U_{H}$).

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

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

Examples:

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

Definition 14

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

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

Lemma 4

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

Theorem 4

A set of clauses $S$ is unsatisfiable iff there is no Herbrand model for $S$.

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