Herbrand's theorem

The set of Herbrand is a set of mathematical logic, was published in 1930 by the French logician Jacques Herbrand. He makes a statement about when a predicate logic formula is generally valid or satisfiable and allows a reduction to universal validity or satisfiability in propositional logic.

The theorem states:

Sketch of proof

Be given a closed predicate logic formula. This is first converted into an equivalent prenex normal form. In this formula will now be similar to Skolemization, all universal quantifiers eliminated by the bound variable is replaced by a term which consists of a new function symbols and arguments as the bound variables of all further outside existential. For example, if the formula in the form

( Quantifier ), has to be converted into

It can be shown that iff is a tautology, if a tautology. Let now. Obviously, if a disjunction of substitution instances of a tautology is also a tautology. The non-trivial direction now is to show that from the generality of already implies the existence of a universal disjunction of instances of. Assuming no disjunction of variable-free instances of is a tautology. Then the amount of

Consistent and satisfied by a Herbrand structure whose elements are exactly the terms in the language of. is a model of. This is not a tautology and well.

There are also known other evidence. Thus, for the set of proof theoretically demonstrated by the completeness of the cut -free sequent calculus by the introductions of quantifiers are eliminated from a cut -free derivation, so that we obtain the derivation of a sequence of quantifier instances.

Corollaries

• A closed formula is satisfiable if it has a Herbrand model.

• A set of clauses is unsatisfiable if and only if there is an unsatisfiable finite set of ground instances of clauses from.

• A formula in Skolem 's exactly then unsatisfiable if there is a finite unsatisfiable conjunction of substitution instances.

Application of the theorem of Herbrand

The set forms the basis of a semi - decision procedure for the unsatisfiability of predicate logic formulas. We are looking for a (simple ) subclass of structures / models, so that a formula is unsatisfiable iff (or satisfiable ), if it has no (or an ) model in this subclass.

If you want to prove by any predicate logic formula F unsatisfiable, bringing them first by renaming bound in an adjusted form. Then, it is the existence of completion to remove the free variables and thus obtain a closed formula. The quantifiers be switched to the left, so as to obtain a prenex normal form. Then, the existential be removed in order to obtain a Skolem. The formula F ', obtained after this transformation steps is no longer equivalent, but erfüllbarkeitsäquivalent to the initial formula F. This is sufficient rather weak property to prove unsatisfiability of F.

Now it is the formula F 'is a Herbrand universe, a Herbrand structure and, based on a Herbrand expansion. Each element of the expansion is identifiable by a propositional formula. For this purpose, each predicate is a propositional variable to. The assignment function bel has a propositional variable if and only one, albeit the predicate has the truth value 1. The propositional formula is thus satisfiable, even if the predicate logic formula F ' is satisfiable.

With the algorithm of Gilmore you can then show the unsatisfiability of F ', and thus also F.