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

## Equivalence and Normal Forms[edit | edit source]

Equivalence of formulae is defined as in the propositional case:

## Definition 6[edit | edit source]

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 | edit source]

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 | edit source]

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 | edit source]

Let be a formula, a variable and a term.

## Lemma 2 (Bounded Renaming)[edit | edit source]

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

## Definition 8[edit | edit source]

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 | edit source]

For every formula there is a formula which is proper and
equivalent to .

**Proof:** Follows immediately by bounded renaming.

Example:

has the equivalent and proper formula

## Definition 9[edit | edit source]

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

## Theorem 2[edit | edit source]

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

Example:

**Proof:** Induction over 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

where

- 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 | edit source]

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 | edit source]

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:

## Problems[edit | edit source]

#### Problem 6 (Predicate)[edit | edit source]

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 | edit source]

Show the following semantic equivalences:

#### Problem 8 (Predicate)[edit | edit source]

Show the following semantic equivalences:

#### Problem 9 (Predicate)[edit | edit source]

Show that for arbitrary formulae and , the following holds:

- If , than .