# 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 $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

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

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

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)

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

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 $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

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

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

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

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

#### Problem 6 (Predicate)

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)

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)

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)

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$