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 xF$ $\equiv$ $\exists x\lnot F$

$\lnot \exists xF$ $\equiv$ $\forall x\lnot F$

If $x$ does not occur free in $G$:

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

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

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

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

$\forall xF\land \forall xG$ $\equiv$ $\forall x(F\land G)$

$\exists xF\lor \exists xG$ $\equiv$ $\exists x(F\lor G)$

$\forall x\forall y\;F$ $\equiv$ $\forall y\forall xF$

$\exists x\exists y\;F$ $\equiv$ $\exists y\exists xF$

Proof: We will prove only the equivalence

$\forall xF\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 xF\land G)=true$

${\text{iff }}{\mathcal {I}}(\forall xF)=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 xF\lor \forall xG$ is not equivalent to $\forall x(F\lor G)$

$\exists xF\land \exists xG$ 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 xP(x,y)\lor \forall zQ(z))\land \exists wP(f(a,w)))$

$\equiv ((\lnot \exists xP(x,y)\land \lnot \forall zQ(z))\land \exists wP(f(a,w)))$

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

$\equiv (\exists wP(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=QxG$ be a formula, where $Q\in \{\forall ,\exists \}$ and $y$ a variable without an occurrence in $G$, then $F\equiv QyG[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 equivalent 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 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 &ifQ_{i}=\forall \\\;\;\,\forall &ifQ_{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 _{i=1}^{n}~(\bigvee _{j=1}^{m}~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 xp(x))\to q(b)\equiv \exists x(p(x)\to q(b))$
2. $(\forall xr(x))\lor (\exists y\lnot r(y))\equiv (\forall xr(x))\to (\exists yr(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 xF\lor \forall xG$
2. If $G=F[x/t]$, than $G\models \exists xF$.

$\Box$