Logic for Computer Scientists/Predicate Logic/Equivalence and Normal Forms

From Wikibooks, open books for an open world
< Logic for Computer Scientists‎ | Predicate Logic
Jump to: navigation, search

Equivalence and Normal Forms[edit]

Equivalence of formulae is defined as in the propositional case:

Definition 6[edit]

The formulae and are called (semantically) equivalent, if for all interpretations for and , . We write .

The equivalences from the propositional case in theorem 4 equivalences hold and in addition we have the following cases for quantifiers.

Theorem 1[edit]

The following equivalences hold:

If does not occur free in :

Proof: We will prove only the equivalence

with has no free occurrence in , as an example. Assume an interpretation such that

Note that the following symmetric cases do not hold:

is not equivalent to

is not equivalent to

The theorem for substituitivity holds as in the propositional case.

Example: Let us transform the following formulae by means of substituitivity and the equivalences from theorem 1:

Definition 7[edit]

Let be a formula, a variable and a term. is obtained from by substituting every free occurrence of by .
Note, that this notion can be iterated: and that may contain free occurrences of .

Lemma 1[edit]

Let be a formula, a variable and a term.

Lemma 2 (Bounded Renaming)[edit]

Let be a formula, where and a variable without an occurrence in , then

Definition 8[edit]

A formula is called proper if there is no variable which occurs bound and free and after every quantifier there is a distinct variable.

Lemma 3 (Proper Formula)[edit]

For every formula there is a formula which is proper and equivalent to .
Proof: Follows immediately by bounded renaming.

has the eqiuvalent and proper formula

Definition 9[edit]

A formula is called in prenex form if it has the form , where with no occurrences of a quantifier in

Theorem 2[edit]

For every formula there is a proper formula in prenex form, which is equivalent.

Proof: Induction over the the structure of the formula gives us the theorem for an atomic formula immediately.

  • : There is a with , which is equivalent to . Hence we have


  • with . There exists which are proper and in prenex form and and . With bounded renaming we can construct

where and hence

In the following we call proper formulae in prenex form PP-formulae or PPF’s.

Definition 10[edit]

Let be a PPF. While contains a -Quantifier, do the following transformation:

has the form

where is a PPF and is a -ary function symbol, which does not occur in .

Let be

If there exists no more -quantifier, is in Skolem form.

Theorem 3[edit]

Let be a PPF. is satisfiable iff the Skolem form of is satisfiable.

Proof: Let ; after one transformation according to the while-loop we have

where is a new function symbol. We have to prove that this transformation is satisfiability preserving: Assume is satisfiable. than there exists a model for is an interpretation for . From the model property we have for all

From Lemma 1 we conclude

where . Hence we have, that for all there is a , where

and hence we have, that , which means, that is a model for .

For the opposite direction of the theorem, assume that has a model . Then we have, that for all , there is a , where

Let be an interpretation, which deviates from only, by the fact that it is defined for the function symbol , where is not defined. We assume that , where is chosen according to the above equation.

Hence we have that for all

and from Lemma 1 we conclude that for all

which means, that , and hence is a model for .

The above results can be used to transform a Formula into a set of clauses, its clause normal form:

Transformation into Clause Normal Form

Given a first order formula .

  • Transform into an equivalent proper by bounded renaming.
  • Let the free variables from . Transform into
  • Transform into an equivalent prenex form .
  • Transform into its Skolemform
  • Transform into its CNF where is a literal. This results in
  • Write as a set of clauses:


Problem 6 (Predicate)[edit]

Let be a formula, a variable and a term. Then denotes the formula which results from by replacing every free occurrence of by . Give a formal definition of this three argument function , by induction over the structure of the formula .

Problem 7 (Predicate)[edit]

Show the following semantic equivalences:

Problem 8 (Predicate)[edit]

Show the following semantic equivalences:

Problem 9 (Predicate)[edit]

Show that for arbitrary formulae and , the following holds:

  1. If , than .