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 $ℐ$ for $F$ and $G$, $ℐ(F)=ℐ(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:

$\mathrm{\neg }\mathrm{\forall }xF$ $\equiv$ $\mathrm{\exists }x\mathrm{\neg }F$

$\mathrm{\neg }\mathrm{\exists }xF$ $\equiv$ $\mathrm{\forall }x\mathrm{\neg }F$

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

$\mathrm{\forall }xF\wedge G$ $\equiv$ $\mathrm{\forall }x(F\wedge G)$

$\mathrm{\forall }xF\vee G$ $\equiv$ $\mathrm{\forall }x(F\vee G)$

$\mathrm{\exists }xF\wedge G$ $\equiv$ $\mathrm{\exists }x(F\wedge G)$

$\mathrm{\exists }xF\vee G$ $\equiv$ $\mathrm{\exists }x(F\vee G)$

$\mathrm{\forall }xF\wedge \mathrm{\forall }xG$ $\equiv$ $\mathrm{\forall }x(F\wedge G)$

$\mathrm{\exists }xF\vee \mathrm{\exists }xG$ $\equiv$ $\mathrm{\exists }x(F\vee G)$

$\mathrm{\forall }x\mathrm{\forall }yF$ $\equiv$ $\mathrm{\forall }y\mathrm{\forall }xF$

$\mathrm{\exists }x\mathrm{\exists }yF$ $\equiv$ $\mathrm{\exists }y\mathrm{\exists }xF$

Proof: We will prove only the equivalence

$\mathrm{\forall }xF\wedge G\equiv \mathrm{\forall }x(F\wedge G)$

with $x$ has no free occurrence in $G$, as an example. Assume an interpretation $ℐ=(U,𝒜)$ such that

$ℐ(\mathrm{\forall }xF\wedge G)=true$

$\text{iff }ℐ(\mathrm{\forall }xF)=true\text{ and }ℐ(G)=true$

$\text{iff }\text{ for all }d\in U:{ℐ}_{[x/d]}(F)=true\text{ and }ℐ(G)=true$

$\text{iff }\text{ for all }d\in U:{ℐ}_{[x/d]}(F)=true\text{ and }{ℐ}_{[x/d]}(G)=true\text{ (x = does not occur free in = G)}$

$\text{iff }\text{ for all }d\in U:{ℐ}_{[x/d]}((F\wedge G))=true$

$\text{iff }ℐ(\mathrm{\forall }x(F\wedge G))=true.$

Note that the following symmetric cases do not hold:

$\mathrm{\forall }xF\vee \mathrm{\forall }xG$ is not equivalent to $\mathrm{\forall }x(F\vee G)$

$\mathrm{\exists }xF\wedge \mathrm{\exists }xG$ is not equivalent to $\mathrm{\exists }x(F\wedge 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:

$(\mathrm{\neg }(\mathrm{\exists }xP(x,y)\vee \mathrm{\forall }zQ(z))\wedge \mathrm{\exists }wP(f(a,w)))$

$\equiv ((\mathrm{\neg }\mathrm{\exists }xP(x,y)\wedge \mathrm{\neg }\mathrm{\forall }zQ(z))\wedge \mathrm{\exists }wP(f(a,w)))$

$\equiv ((\mathrm{\forall }x\mathrm{\neg }P(x,y)\wedge \mathrm{\exists }z\mathrm{\neg }Q(z))\wedge \mathrm{\exists }wP(f(a,w)))$

$\equiv (\mathrm{\exists }wP(f(a,w))\wedge (\mathrm{\forall }x\mathrm{\neg }P(x,y)\wedge \mathrm{\exists }z\mathrm{\neg }Q(z)))$

$\equiv \mathrm{\exists }w(P(f(a,w))\wedge \mathrm{\forall }x(\mathrm{\neg }P(x,y)\wedge \mathrm{\exists }z\mathrm{\neg }Q(z)))$

$\equiv \mathrm{\exists }w(\mathrm{\forall }x(\mathrm{\exists }z\mathrm{\neg }Q(z)\wedge \mathrm{\neg }P(x,y))\wedge P(f(a,w)))$

$\equiv \mathrm{\exists }w(\mathrm{\forall }x\mathrm{\exists }z(\mathrm{\neg }Q(z)\wedge \mathrm{\neg }P(x,y))\wedge P(f(a,w)))$

$\equiv \mathrm{\exists }w\mathrm{\forall }x\mathrm{\exists }z((\mathrm{\neg }Q(z)\wedge \mathrm{\neg }P(x,y))\wedge 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.

$ℐ(F[x/t])={ℐ}_{[x/ℐ(t)]}(F)$

Lemma 2 (Bounded Renaming)

Let $F=QxG$ be a formula, where $Q\in \{\mathrm{\forall },\mathrm{\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=\mathrm{\forall }x\mathrm{\exists }yp(x,f(y))\wedge \mathrm{\forall }x(q(x,y)\vee r(x))$

has the equivalent and proper formula

$G=\mathrm{\forall }x\mathrm{\exists }y(p(x,f(y)))\wedge \mathrm{\forall }z(q(z,u)\vee 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 \{\mathrm{\forall },\mathrm{\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:

$\mathrm{\forall }x\mathrm{\exists }y(p(x,g(y,f(x)))\vee \mathrm{\neg }q(z))\vee \mathrm{\neg }\mathrm{\forall }xr(x,z)$

$\mathrm{\forall }x\mathrm{\exists }y(p(x,g(y,f(x))\vee \mathrm{\neg }q(z))\vee \mathrm{\exists }x\mathrm{\neg }r(x,z)$

$\mathrm{\forall }x\mathrm{\exists }y(p(x,g(y,f(x))\vee \mathrm{\neg }q(z))\vee \mathrm{\exists }v\mathrm{\neg }r(v,z)$

$\mathrm{\forall }x\mathrm{\exists }y\mathrm{\exists }v(p(x,g(y,f(x))\vee \mathrm{\neg }q(z))\vee \mathrm{\neg }r(v,z)$

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

• $F=\mathrm{\neg }{F}_0$: There is a $G_0=Q_1{y}_1\cdots Q_n{y}_n{G}^{\prime }$ with $Q_i\in \{\mathrm{\forall },\mathrm{\exists }\}$, which is equivalent to $F_0$. Hence we have
  
  $F\equiv \overline{Q_1}{y}_1\cdots \overline{Q_n}{y}_n\mathrm{\neg }{G}^{\prime }$

where $\overline{Q_i}=\{\begin{array}{cc}\mathrm{\exists }& if{Q}_i=\mathrm{\forall }\\ \mathrm{\forall }& if{Q}_i=\mathrm{\exists }\end{array}$

• $F=F_1\circ F_2$ with $\circ \in \{\wedge ,\vee \}$. 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}^{\prime }$
$G_2={Q_1}^{\prime }{z}_1\cdots {Q_l}^{\prime }{z}_l{G_2}^{\prime }$

where

$\{y_1,\cdots ,y_n\}\cap \{z_1,\cdots ,z_l\}=\mathrm{\varnothing }$

and hence

$F\equiv Q_1{y}_1\cdots Q_k{y}_k{Q_1}^{\prime }{z}_1\cdots {Q_l}^{\prime }{z}_l({G_1}^{\prime }\circ {G_2}^{\prime })$

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 $\mathrm{\exists }$-Quantifier, do the following transformation:

$F$ has the form

$\mathrm{\forall }{y}_1,\cdots \mathrm{\forall }{y}_n\mathrm{\exists }zG$

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

Let $F$ be

$\mathrm{\forall }{y}_1,\cdots \mathrm{\forall }{y}_{n}G[z/f(y_1,\cdots ,y_n)]$

If there exists no more $\mathrm{\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=\mathrm{\forall }{y}_1\cdots \mathrm{\forall }{y}_n\mathrm{\exists }zG$; after one transformation according to the while-loop we have

$F^{\prime }=\mathrm{\forall }{y}_1\cdots \mathrm{\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^{\prime }$ is satisfiable. than there exists a model $ℐ$ for $F^{\prime }$ $ℐ$ is an interpretation for $F$. From the model property we have for all $u_1,\cdots ,u_n\in U_{ℐ}$

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

From Lemma 1 we conclude

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

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

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

and hence we have, that $ℐ(\mathrm{\forall }{y}_1\cdots \mathrm{\forall }{y}_n\mathrm{\exists }zG)=true$, which means, that $ℐ$ is a model for $F$.

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

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

Let ${ℐ}^{\prime }$ be an interpretation, which deviates from $ℐ$ only, by the fact that it is defined for the function symbol $f$, where $ℐ$ is not defined. We assume that $f^{{ℐ}^{\prime }}(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_{ℐ}}^{\prime }$

$ℐ{\text{'}}_{[y_1/u_1]\cdots [y_n/u_n][z/f^{{ℐ}^{\prime }}(u_1,\cdots ,u_n)]}(G)=true$

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

$ℐ{\text{'}}_{[y_1/u_1]\cdots [y_n/u_n]}(G[z/f^{(}{y}_1,\cdots ,y_n)])=true$

which means, that ${ℐ}^{\prime }(\mathrm{\forall }{y}_1\cdots \mathrm{\forall }{y}_{n}G[z/f(y_1,\cdots ,y_n)])=true$, and hence ${ℐ}^{\prime }$ is a model for $F^{\prime }$.

The above results can be used to transform a Formula into a set of clauses, its clause normal form:

Template:Box

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

$◻$

Problem 7 (Predicate)

Show the following semantic equivalences:

1. $\mathrm{\forall }x(p(x)\to (q(x)\wedge r(x)))\equiv \mathrm{\forall }x(p(x)\to q(x))\wedge \mathrm{\forall }x(p(x)\to r(x))$
2. $\mathrm{\forall }x(p(x)\to (q(x)\vee r(x)))\equiv ̸\mathrm{\forall }x(p(x)\to q(x))\vee \mathrm{\forall }x(p(x)\to r(x))$

$◻$

Problem 8 (Predicate)

Show the following semantic equivalences:

1. $(\mathrm{\forall }xp(x))\to q(b)\equiv \mathrm{\exists }x(p(x)\to q(b))$
2. $(\mathrm{\forall }xr(x))\vee (\mathrm{\exists }y\mathrm{\neg }r(y))\equiv (\mathrm{\forall }xr(x))\to (\mathrm{\exists }yr(y))$

$◻$

Problem 9 (Predicate)

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

1. $\mathrm{\forall }x(F\vee G)\equiv ̸\mathrm{\forall }xF\vee \mathrm{\forall }xG$
2. If $G=F[x/t]$, than $G\models \mathrm{\exists }xF$.

$◻$