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.
- 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
- 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
( quantifier-free), it is converted into
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
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.
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 .
- 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
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
- ↑ Gerhard Goos, Wolf Zimmermann: Lectures on computer science: Volume 1: Basics and functional programming . ISBN 3540244050 . P. 203.