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

Equivalence and Normal Forms Equivalence of formulae is defined as in the propositional case: Definition 6 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 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 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 Let be a formula, a variable and a term. Lemma 2 (Bounded Renaming) Let be a formula, where and a variable without an occurrence in , then Definition 8 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) 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 A formula is called in prenex form if it has the form , where with no occurrences of a quantifier in Theorem 2 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 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 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: where Problems Problem 6 (Predicate) 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) Show the following semantic equivalences: Problem 8 (Predicate) Show the following semantic equivalences: Problem 9 (Predicate) Show that for arbitrary formulae and , the following holds: If , than .