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{ ist variablenfreie Instanz von }}\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.

See also

• List of theorems of computer science

literature

• Peter G. Hinman: Fundamentals of Mathematical Logic . AK Peters, 2005.
• Joseph R. Shoenfield: Mathematical Logic . Addison-Wesley, 1967.
• Jacques Herbrand: Recherches sur la theory de la demonstration . In: Travaux de la Societe des Sciences et des Lettres de Varsovie, Class III, Sciences Mathematiques et Physiques . No. 33 , 1930.

Individual evidence

1. ↑ Gerhard Goos, Wolf Zimmermann: Lectures on computer science: Volume 1: Basics and functional programming . ISBN 3540244050 . P. 203.