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 by replacing all variables with some ground terms from .
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 is true in , then is also true in ( is a consequence of ).
We expand entire set: \[
expand(S) = \bigcup_{C \in S} expand(C)
\]
Clauses in the expansion have no variables, they are ground clauses.
Constructing a Propositional Model
We can view the set as a set of propositional formulas whose propositional variables have “long names”.
For an expansion of clause we can construct the corresponding propositional formula .
Example Let's consider the expanded formula , then
Define propositional model 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 is a model of , then is a model of .
Instead of searching for a model, we can search for a propositional model.
If we prove there is no propositional model for , then there is no model for .
What if there is a model ? Could it still be the case that is unsatisfiable?
Constructing Herbrand Model
For we define so that evaluates ground formulas same as in (and thus same as in ).
We ensure that atomic formulas evaluate the same:
How does it evaluate non-ground formulas?
Lemma: If is a model for , then is a model for .
Herbrand's Theorem
Theorem: The following statements are equivalent:
- set has a model
- set has a propositional model
- set has a model with domain