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 F and G are called (semantically) equivalent, if for all interpretations \mathcal{I} for F and G, \mathcal{I}(F)= \mathcal{I}(G). We write F \equiv G.

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:

 \lnot \forall x F  \equiv  \exists x  \lnot F

 \lnot \exists x F  \equiv  \forall x \lnot F

If x does not occur free in G:

 \forall x  F \land G  \equiv  \forall x ( F \land G)

 \forall x  F \lor G \equiv  \forall x ( F \lor G)

 \exists x  F \land G \equiv  \exists x ( F \land G)

 \exists x  F \lor G \equiv  \exists x ( F \lor G)


\forall x F \land \forall x G  \equiv  \forall x  (F  \land G)

\exists  x F \lor \exists x G  \equiv \exists x  (F \lor G)

\forall x \forall y \; F \equiv  \forall y \forall x F

\exists x \exists y \; F  \equiv \exists y \exists x F


Proof: We will prove only the equivalence

 \forall x  F \land G \equiv \forall x ( F \land G)

with x has no free occurrence in G, as an example. Assume an interpretation \mathcal{I}= (U,\mathcal{A}) such that

 \mathcal{I}( \forall x  F \land G) = true
\text{iff } \mathcal{I}(\forall x F)= true \text{ and } \mathcal{I}(G) = true
\text{iff }  \text{ for all }  d \in U : \mathcal{I}_{[x/d]}(F) = true   \text{ and } 
\mathcal{I}(G) = true
\text{iff } \text{ for all }  d \in U : \mathcal{I}_{[x/d]}(F) = true   \text{ and } 
\mathcal{I}_{[x/d]}(G) = true \text{ (x = does not occur free in = G)}
\text{iff }  \text{ for all }  d \in U : \mathcal{I}_{[x/d]}((F \land G))= true
\text{iff } \mathcal{I}( \forall x ( F \land G)) = true.


Note that the following symmetric cases do not hold:

\forall  x F \lor \forall x G is not equivalent to \forall x  (F \lor G)

\exists  x F \land \exists x G is not equivalent to \exists x  (F \land G)

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:


 (\lnot ( \exists x  P(x,y) \lor \forall z Q(z)) \land \exists w  P(f(a,w)))

\equiv ((\lnot  \exists x P(x,y) \land \lnot \forall z Q(z)) \land \exists w  P(f(a,w)))

\equiv ((\forall x \lnot  P(x,y) \land \exists z \lnot Q(z)) \land \exists w  P(f(a,w)))

\equiv ( \exists w  P(f(a,w)) \land (\forall x \lnot  P(x,y) \land \exists z \lnot Q(z)))

\equiv \exists w ( P(f(a,w)) \land \forall x  (\lnot  P(x,y) \land \exists z \lnot Q(z)))

\equiv \exists w ( \forall x  ( \exists z \lnot Q(z) \land \lnot  P(x,y)) \land  P(f(a,w)))

\equiv  \exists w ( \forall x   \exists z (\lnot Q(z) \land \lnot  P(x,y)) \land  P(f(a,w)))

\equiv  \exists w  \forall x   \exists z ((\lnot Q(z) \land \lnot  P(x,y)) \land  P(f(a,w)))

Definition 7[edit]

Let F be a formula, x a variable and t a term. F[x/t] is obtained from F by substituting every free occurrence of x by t.
Note, that this notion can be iterated: F[x/t_1][y/t_2] and that t_1 may contain free occurrences of y.

Lemma 1[edit]

Let F be a formula, x a variable and t a term.

\mathcal{I}(F[x/t]) = \mathcal{I}_{[x/\mathcal{I}(t)]}(F)

Lemma 2 (Bounded Renaming)[edit]

Let F= Q x G be a formula, where Q \in \{\forall, \exists\} and y a variable without an occurrence in G, then F \equiv Q y G[x/y]

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 F there is a formula G which is proper and equivalent to F.
Proof: Follows immediately by bounded renaming.
Example:


F = \forall x \exists y\; p(x, f(y)) \land \forall x (q(x, y) \lor r(x))


has the eqiuvalent and proper formula


G=  \forall x \exists y\;( p(x, f(y))) \land \forall z(q(z, u) \lor r(z)

Definition 9[edit]

A formula is called in prenex form if it has the form  Q_1 \cdots Q_n F, where Q_i \in \{\forall, \exists\} with no occurrences of a quantifier in F

Theorem 2[edit]

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

\forall x \exists y\;( p(x, g(y, f(x))) \lor \lnot q(z))  \lor \lnot \forall x \;r(x,z)


\forall x \exists y\;( p(x, g(y, f(x)) \lor \lnot q(z)) \lor \exists x \;  \lnot  r(x,z)


\forall x \exists y\;( p(x, g(y, f(x)) \lor \lnot q(z)) \lor \exists v \lnot   r(v,z)


\forall x \exists y \exists v\; ( p(x, g(y, f(x)) \lor \lnot q(z)) \lor  \lnot   r(v,z)

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

  • F = \lnot F_0: There is a G_0 = Q_1 y_1 \cdots Q_n y_n G' with Q_i \in \{ \forall, \exists\} , which is equivalent to F_0. Hence we have

    F \equiv  \overline{Q_1} y_1 \cdots \overline{Q_n} y_n \lnot G'

where \overline{Q_i} = \begin{cases} 
\;\;\,\exists & if Q_i = \forall \\
\;\;\, \forall & if Q_i = \exists  
\end{cases}

  • F = F_1 \circ F_2 with \circ \in \{\land, \lor\} . There exists G_1, G_2 which are proper and in prenex form and G_1 \equiv F_1 and G_2 \equiv F_2. With bounded renaming we can construct
 G_1 =   Q_1 y_1 \cdots Q_k y_k G_1'
G_2  =  Q_1' z_1 \cdots Q_l' z_l G_2'

where \{y_1, \cdots , y_n\} \cap \{z_1, \cdots , z_l\} = \emptyset and hence


F \equiv Q_1 y_1 \cdots Q_k y_k Q_1' z_1 \cdots Q_l' z_l ( G_1' \circ G_2')


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

Definition 10[edit]

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

F has the form

 \forall y_1, \cdots \forall y_n \exists z\; G

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

Let F be

 \forall y_1, \cdots \forall y_n\;  G[z/f(y_1, \cdots ,y_n)]

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

Theorem 3[edit]

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

Proof: Let F = \forall y_1 \cdots \forall y_n \exists z\; G; after one transformation according to the while-loop we have



F' =  \forall y_1 \cdots \forall y_n \; G [z/ f(y_1, \cdots , y_n)


where f is a new function symbol. We have to prove that this transformation is satisfiability preserving: Assume F' is satisfiable. than there exists a model \mathcal{I} for F' \mathcal{I} is an interpretation for F. From the model property we have for all u_1, \cdots , u_n \in U_\mathcal{I}



\mathcal{I}_{[y_1/u_1] \cdots [y_n/u_n]}(G[z/f(y_1, \cdots , y_n)]) = true


From Lemma 1 we conclude



\mathcal{I}_{[y_1/u_1] \cdots [y_n/u_n] [z/v]} (G) = true


where v = \mathcal{I}(f(u_1, \cdots , u_n). Hence we have, that for all u_1,
\cdots , u_n \in U_\mathcal{I} there is a  v \in U_\mathcal{I}, where



\mathcal{I}_{[y_1/u_1] \cdots [y_n/u_n] [z/v]} (G) = true


and hence we have, that \mathcal{I}(\forall y_1 \cdots \forall y_n \exists z\; G) = true, which means, that \mathcal{I} is a model for F.

For the opposite direction of the theorem, assume that F has a model \mathcal{I}. Then we have, that for all u_1, \cdots , u_n \in U_\mathcal{I}, there is a  v \in U_\mathcal{I}, where



\mathcal{I}_{[y_1/u_1] \cdots [y_n/u_n] [z/v]} (G) = true


Let \mathcal{I'} be an interpretation, which deviates from \mathcal{I} only, by the fact that it is defined for the function symbol f, where \mathcal{I} is not defined. We assume that f^{\mathcal{I}'}(u_1, \cdots, u_n) = v, where v is chosen according to the above equation.

Hence we have that for all u_1, \cdots , u_n \in U_\mathcal{I}'



\mathcal{I}'_{[y_1/u_1] \cdots [y_n/u_n][z/f^{\mathcal{I}'}(u_1, \cdots, u_n)]}(G) = true


and from Lemma 1 we conclude that for all u_1, \cdots , u_n \in U_\mathcal{I}



\mathcal{I}'_{[y_1/u_1] \cdots [y_n/u_n]}(G[z/f^(y_1, \cdots, y_n)]) = true


which means, that \mathcal{I}'(\forall y_1 \cdots \forall y_n \; G[z/f(y_1, \cdots , y_n)]) =
true, and hence \mathcal{I}' is a model for F'.

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 F.

  • Transform F into an equivalent proper F_1 by bounded renaming.
  • Let y_1, \cdots , y_k the free variables from F_1. Transform F_1 into F_2 = \exists y_1 \cdots \exists y_k \; F_1
  • Transform F_2 into an equivalent prenex form F_3.
  • Transform F_3 into its Skolemform F_4 = \forall x_1 \cdots \forall x_l   \; G
  • Transform G into its CNF G\prime = (\bigwedge^n_{i=1} ~(\bigvee^m_{j=1} ~L_{i,j})) where L_{ij} is a literal. This results in F_5 =  \forall   x_1 \cdots \forall x_l   \; G\prime
  • Write F_5 as a set of clauses:
    F_6 =  \{C_1, \cdots , C_n\}
where C_i = \{L_{i,1}, \cdots , L_{i,m}\}


Problems[edit]

Problem 6 (Predicate)[edit]

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

\Box

Problem 7 (Predicate)[edit]

Show the following semantic equivalences:

  1. \forall x (p(x) \to (q(x) \land r(x))) \equiv \forall x (p(x) \to q(x)) \land \forall x (p(x) \to r(x))
  2. \forall x (p(x) \to (q(x) \lor r(x))) \not\equiv \forall x (p(x) \to q(x)) \lor \forall x (p(x) \to r(x))


\Box

Problem 8 (Predicate)[edit]

Show the following semantic equivalences:

  1. (\forall x p(x)) \to q(b) \equiv \exists x (p(x) \to q(b))
  2. (\forall x r(x)) \lor (\exists y \lnot r(y)) \equiv (\forall x r(x)) \to (\exists y r(y))


\Box

Problem 9 (Predicate)[edit]

Show that for arbitrary formulae F and G, the following holds:

  1. \forall x (F \lor G) \not\equiv \forall x F \lor \forall x G
  2. If G = F[x/t], than G \models \exists x F.


\Box