# Herbrand expansion

The Herbrand expansion represents a set of predicate logic formulas that can be derived from a given formula F through a special type of substitution . With the help of this set of formulas, the unsatisfiability of a predicate logic formula can be mapped in a propositional form. The Herbrand expansion was named after the French logician Jacques Herbrand .

## definition

Let be a closed formula in Skolem form , F * denote the quantifier-free matrix . ${\ displaystyle F = \ forall y_ {1} \ forall y_ {2} ... \ forall y_ {n} F ^ {*}}$ For F the Herbrand expansion E (F) is defined as:

${\ displaystyle E \ left (F \ right) = \ left \ {F ^ {*} \ left [y_ {1} / t_ {1} \ right] \ left [y_ {2} / t_ {2} \ right ] ... \ left [y_ {n} / t_ {n} \ right] | t_ {1} ... t_ {n} \ in D \ left (F \ right) \ right \}}$ D (F) is the Herbrand universe by F.

Colloquially: All variables in the matrix F * are replaced by terms from D (F), all possibilities are played through. One also speaks of the set of instances of the formula F.

## example

Be ${\ displaystyle F = \ forall x \ forall y \ forall zP (x, f (y), g (z, x))}$ Then see Herbrand Universe . ${\ displaystyle D \ left (F \ right) = \ {a, f (a), g (a, a), f (g (a, a)), g (f (a), f (a)) , ... \}}$ The simplest formulas in are: ${\ displaystyle E \ left (F \ right)}$ ${\ displaystyle P \ left (a, f (a), g (a, a) \ right)}$ With ${\ displaystyle \ left [x / a \ right] \ left [y / a \ right] \ left [z / a \ right]}$ ${\ displaystyle P \ left (f (a), f (a), g (a, f (a)) \ right)}$ With ${\ displaystyle \ left [x / f (a) \ right] \ left [y / a \ right] \ left [z / a \ right]}$ ${\ displaystyle P \ left (a, f (a), g (g (a, a), a) \ right)}$ With ${\ displaystyle \ left [x / a \ right] \ left [y / a \ right] \ left [z / g (a, a) \ right]}$ Note that in this case is infinite. The formulas can now be treated like propositional formulas ( propositional logic ) because they do not contain any variables. ${\ displaystyle E \ left (F \ right)}$ 