Logic for Computer Scientists/Predicate Logic/Equivalence and Normal Forms
Contents
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.
Example:
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.
Example:
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
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 PPformulae 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 whileloop 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:
Given a first order formula .

Problems[edit]
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:
 If , than .