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 .

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 \}}$

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)}$