# Herbrand's theorem

The Herbrand's Theorem is a set of mathematical logic , which in 1930 by the French logician Jacques Herbrand was published. It makes a statement about when a predicate logic formula without equality is generally valid or satisfiable and allows a reduction to general validity or satisfiability in propositional logic .

The sentence says:

Let be a closed predicate logic formula without equality.${\ displaystyle \ varphi}$
Then there is a quantifier-free formula (which can be calculated from ) such that: is a tautology if and only if there are variable-free substitution instances of such that${\ displaystyle \ varphi}$ ${\ displaystyle \ psi}$${\ displaystyle \ varphi}$${\ displaystyle \ psi _ {1}, \ psi _ {2}, \ dots, \ psi _ {n}}$${\ displaystyle \ psi}$
${\ displaystyle \ psi _ {1} \ vee \ psi _ {2} \ vee \ dots \ vee \ psi _ {n}}$
is a propositional tautology.

## Evidence sketch

Let a closed predicate logic formula be given. This is first converted into an equivalent prenex normal form . In this formula, similar to Skolemization , all universal quantifiers are eliminated by replacing the bound variable with a term that consists of a new function sign and the bound variables of all existential quantifiers further out as arguments. For example, if the formula has the form ${\ displaystyle \ varphi}$${\ displaystyle \ varphi '}$

${\ displaystyle \ varphi '= \ exists x_ {1} \ forall x_ {2} \ exists x_ {3} \ forall x_ {4} \ theta (x_ {1}, x_ {2}, x_ {3}, x_ {4})}$

( quantifier-free), it is converted into ${\ displaystyle \ theta}$

${\ displaystyle \ varphi '' = \ exists x_ {1} \ exists x_ {3} \ theta (x_ {1}, f (x_ {1}), x_ {3}, g (x_ {1}, x_ { 3}))}$

It can be shown that there is a tautology if and only if there is a tautology. Be now . Obviously, if a disjunction of substitution instances of is a tautology, then it is also a tautology. The non-trivial direction now consists in showing that the general validity of already implies the existence of a generally valid disjunction of instances of . Assume that no disjunction of variable-free instances of is a tautology. Then the crowd ${\ displaystyle \ varphi}$${\ displaystyle \ varphi ''}$${\ displaystyle \ psi = \ theta (x_ {1}, f (x_ {1}), x_ {3}, g (x_ {1}, x_ {3}))}$${\ displaystyle \ psi}$${\ displaystyle \ varphi ''}$${\ displaystyle \ varphi ''}$${\ displaystyle \ psi}$${\ displaystyle \ psi}$

${\ displaystyle \ {\ neg \ sigma | \ sigma {\ text {is a variable-free instance of}} \ psi \}}$

consistent and is fulfilled by a Herbrand structure , the elements of which are exactly the terms in the language of . is a model of . So neither is nor a tautology. ${\ displaystyle {\ mathfrak {M}}}$${\ displaystyle \ psi}$${\ displaystyle {\ mathfrak {M}}}$${\ displaystyle \ neg \ varphi ''}$${\ displaystyle \ varphi ''}$${\ displaystyle \ varphi}$

Other evidence is known as well. Thus, the set can be proved theoretically by the entirety of the cut-free sequences calculus show, by the introductions of quantifiers are eliminated from a cut-free derivation, so that one obtains the derivation of a sequence of quantifier instances.

## Corollaries

• A closed formula can only be fulfilled if it has a Herbrand model.
• A set of clauses is unsatisfiable if and only if there is an unsatisfiable finite set of basic instances of clauses .${\ displaystyle \ Gamma}$${\ displaystyle \ Gamma}$
• A formula in Skolem form is unsatisfiable if and only if there is an unsatisfiable finite conjunction of substitution instances.

## Application of Herbrand's theorem

The sentence forms the basis of a semi-decision procedure for the unsatisfiability of predicate logic formulas. We are looking for a (simple) sub-class of structures / models so that a formula becomes unsatisfiable (or satisfiable) if it has no (or a) model in this sub-class.

If one wants to prove the unsatisfiability of an arbitrary predicate logic formula F, one first brings it into an adjusted form by means of bound renaming . Then the existence termination is formed in order to remove the free variables and thus to obtain a closed formula. The quantifiers are shifted to the left so that a prenex normal form is obtained. Then the existential quantifiers are removed to obtain a Skolem shape . The formula F ', which is obtained after these transformation steps, is no longer equivalent , but satisfiable equivalent to the initial formula F. This rather weak property is sufficient to prove that F cannot be fulfilled .

Now a Herbrand universe , a Herbrand structure and, based on this, a Herbrand expansion are formed for Formula F ' . Each element of the expansion can be identified by means of a propositional formula. To do this, one assigns a propositional variable to each predicate. The occupancy function bel assigns 1 to a propositional variable if and only if the predicate also has the truth value 1. The propositional formula can therefore be fulfilled exactly if the predicate logic formula F 'can also be fulfilled.

With Gilmore's algorithm one can then show the unsatisfiability of F 'and thus also of F.