# 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

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

Let

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

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 .