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 .
Note that if is true in , then is also true in ( is a consequence of ).
We expand entire set:
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
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 .
Theorem: The following statements are equivalent:
- set has a model
- set has a propositional model
- set has a model with domain
Example: Take the first three clauses our example (from Normal Forms for First-Order Logic):
Taking as domain the set of natural numbers, the structure is a model of the conjunction of these three clauses, where is given by:
This model induces an Herbrand model , in which is a set of ground terms and is a relation on ground terms, .
To determine, for example, whether we check the truth value of the formula
in the original interpretation . The truth value of the above formula in reduces to , which is true. Therefore, we define to contain the pair of ground terms . On the other hand, evaluates to false in , so we define so that it does not contain the pair .