This is an old revision of the document!

Herbrand's Expansion Theorem

Expansion of a Clause

Recall that we do not write quantifiers in the clause, but when we say that a clause is true in a model we mean that its universal closure is true.

We obtain an instance of a clause $C$ by replacing all variables with some ground terms from $GT$ .

Define \[

 expand(C) = \{ subst(\{x_1 \mapsto t_1,\ldots,x_n \mapsto t_n\})(C) \mid FV(C) = \{x_1,\ldots,x_n\}\ \land\ t_1,\ldots,t_n \in GT \}

Note that if $C$ is true in $I$ , then $expand(C)$ is also true in $I$ ( $expand(C)$ is a consequence of $C$ ).

We expand entire set: \[

 expand(S) = \bigcup_{C \in S} expand(C)

Clauses in the expansion have no variables, they are ground clauses.

We can view the set $expand(S)$ as a set of propositional formulas whose propositional variables have “long names”.

For an expansion of clause $C_G$ we can construct the corresponding propositional formula $p(C_G)$ .

Example Let's consider the expanded formula $F=P(f(a)) \wedge R(a, f(a))$ , then $p(F)=p_1 \wedge p_4$

Define propositional model $I_P : V \to \{\it true},{\it false\}$ by \[

  I_P(p(C_G)) = e_F(C_G)(I)

Let \[

 propExpand(S) = \{ p(C_G) \mid C_G \in expand(S) \}

Lemma: If $I$ is a model of $S$ , then $I_P$ is a model of $propExpand(S)$ .

Instead of searching for a model, we can search for a propositional model.

If we prove there is no propositional model for $propExpand(S)$ , then there is no model for $I$ .

What if there is a model $propExpand(S)$ ? Could it still be the case that $S$ is unsatisfiable?

For $I = (GT,\alpha_H)$ we define $\alpha_H(R)$ so that $I_H$ evaluates ground formulas $expand(S)$ same as in $I_P$ (and thus same as in $I$ ).

We ensure that atomic formulas evaluate the same:

$\alpha_H(R) = \{ (t_1,\ldots,t_n)\ \mid$ $I_P(p(R(t_1,\ldots,t_n))) \}$

How does it evaluate non-ground formulas?

Lemma: If $I_P$ is a model for $propExpand(S)$ , then $(GT,\alpha_H)$ is a model for $S$ .

Theorem: The following statements are equivalent: