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

${\displaystyle \lnot \forall xF}$ ${\displaystyle \equiv }$ ${\displaystyle \exists x\lnot F}$

${\displaystyle \lnot \exists xF}$ ${\displaystyle \equiv }$ ${\displaystyle \forall x\lnot F}$

If ${\displaystyle x}$ does not occur free in ${\displaystyle G}$:

${\displaystyle \forall xF\land G}$ ${\displaystyle \equiv }$ ${\displaystyle \forall x(F\land G)}$

${\displaystyle \forall xF\lor G}$ ${\displaystyle \equiv }$ ${\displaystyle \forall x(F\lor G)}$

${\displaystyle \exists xF\land G}$ ${\displaystyle \equiv }$ ${\displaystyle \exists x(F\land G)}$

${\displaystyle \exists xF\lor G}$ ${\displaystyle \equiv }$ ${\displaystyle \exists x(F\lor G)}$

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

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

${\displaystyle \forall x\forall y\;F}$ ${\displaystyle \equiv }$ ${\displaystyle \forall y\forall xF}$

${\displaystyle \exists x\exists y\;F}$ ${\displaystyle \equiv }$ ${\displaystyle \exists y\exists xF}$

Proof: We will prove only the equivalence

${\displaystyle \forall xF\land G\equiv \forall x(F\land G)}$

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

${\displaystyle {\mathcal {I}}(\forall xF\land G)=true}$
${\displaystyle {\text{iff }}{\mathcal {I}}(\forall xF)=true{\text{ and }}{\mathcal {I}}(G)=true}$
${\displaystyle {\text{iff }}{\text{ for all }}d\in U:{\mathcal {I}}_{[x/d]}(F)=true{\text{ and }}{\mathcal {I}}(G)=true}$
${\displaystyle {\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)}}}$
${\displaystyle {\text{iff }}{\text{ for all }}d\in U:{\mathcal {I}}_{[x/d]}((F\land G))=true}$
${\displaystyle {\text{iff }}{\mathcal {I}}(\forall x(F\land G))=true.}$

Note that the following symmetric cases do not hold:

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

${\displaystyle \exists xF\land \exists xG}$ is not equivalent to ${\displaystyle \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:

${\displaystyle (\lnot (\exists xP(x,y)\lor \forall zQ(z))\land \exists wP(f(a,w)))}$
${\displaystyle \equiv ((\lnot \exists xP(x,y)\land \lnot \forall zQ(z))\land \exists wP(f(a,w)))}$
${\displaystyle \equiv ((\forall x\lnot P(x,y)\land \exists z\lnot Q(z))\land \exists wP(f(a,w)))}$
${\displaystyle \equiv (\exists wP(f(a,w))\land (\forall x\lnot P(x,y)\land \exists z\lnot Q(z)))}$
${\displaystyle \equiv \exists w(P(f(a,w))\land \forall x(\lnot P(x,y)\land \exists z\lnot Q(z)))}$
${\displaystyle \equiv \exists w(\forall x(\exists z\lnot Q(z)\land \lnot P(x,y))\land P(f(a,w)))}$
${\displaystyle \equiv \exists w(\forall x\exists z(\lnot Q(z)\land \lnot P(x,y))\land P(f(a,w)))}$
${\displaystyle \equiv \exists w\forall x\exists z((\lnot Q(z)\land \lnot P(x,y))\land P(f(a,w)))}$

## Definition 7

Let ${\displaystyle F}$ be a formula, ${\displaystyle x}$ a variable and ${\displaystyle t}$ a term. ${\displaystyle F[x/t]}$ is obtained from ${\displaystyle F}$ by substituting every free occurrence of ${\displaystyle x}$ by ${\displaystyle t}$.
Note, that this notion can be iterated: ${\displaystyle F[x/t_{1}][y/t_{2}]}$ and that ${\displaystyle t_{1}}$ may contain free occurrences of ${\displaystyle y}$.

## Lemma 1

Let ${\displaystyle F}$ be a formula, ${\displaystyle x}$ a variable and ${\displaystyle t}$ a term.

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

## Lemma 2 (Bounded Renaming)

Let ${\displaystyle F=QxG}$ be a formula, where ${\displaystyle Q\in \{\forall ,\exists \}}$ and ${\displaystyle y}$ a variable without an occurrence in ${\displaystyle G}$, then ${\displaystyle 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 ${\displaystyle F}$ there is a formula ${\displaystyle G}$ which is proper and equivalent to ${\displaystyle F}$.
Proof: Follows immediately by bounded renaming.
Example:

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

has the equivalent and proper formula

${\displaystyle 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 ${\displaystyle Q_{1}\cdots Q_{n}F}$, where ${\displaystyle Q_{i}\in \{\forall ,\exists \}}$ with no occurrences of a quantifier in ${\displaystyle F}$

## Theorem 2

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

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

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

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

${\displaystyle \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.

• ${\displaystyle F=\lnot F_{0}}$: There is a ${\displaystyle G_{0}=Q_{1}y_{1}\cdots Q_{n}y_{n}G'}$ with ${\displaystyle Q_{i}\in \{\forall ,\exists \}}$, which is equivalent to ${\displaystyle F_{0}}$. Hence we have

${\displaystyle F\equiv {\overline {Q_{1}}}y_{1}\cdots {\overline {Q_{n}}}y_{n}\lnot G'}$

where ${\displaystyle {\overline {Q_{i}}}={\begin{cases}\;\;\,\exists &ifQ_{i}=\forall \\\;\;\,\forall &ifQ_{i}=\exists \end{cases}}}$

• ${\displaystyle F=F_{1}\circ F_{2}}$ with ${\displaystyle \circ \in \{\land ,\lor \}}$. There exists ${\displaystyle G_{1},G_{2}}$ which are proper and in prenex form and ${\displaystyle G_{1}\equiv F_{1}}$ and ${\displaystyle G_{2}\equiv F_{2}}$. With bounded renaming we can construct
${\displaystyle G_{1}=Q_{1}y_{1}\cdots Q_{k}y_{k}G_{1}'}$
${\displaystyle G_{2}=Q_{1}'z_{1}\cdots Q_{l}'z_{l}G_{2}'}$

where ${\displaystyle \{y_{1},\cdots ,y_{n}\}\cap \{z_{1},\cdots ,z_{l}\}=\emptyset }$ and hence

${\displaystyle 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 ${\displaystyle F}$ be a PPF. While ${\displaystyle F}$ contains a ${\displaystyle \exists }$-Quantifier, do the following transformation:

${\displaystyle F}$ has the form

${\displaystyle \forall y_{1},\cdots \forall y_{n}\exists z\;G}$

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

Let ${\displaystyle F}$ be

${\displaystyle \forall y_{1},\cdots \forall y_{n}\;G[z/f(y_{1},\cdots ,y_{n})]}$

If there exists no more ${\displaystyle \exists }$-quantifier, ${\displaystyle F}$ is in Skolem form.

## Theorem 3

Let ${\displaystyle F}$ be a PPF. ${\displaystyle F}$ is satisfiable iff the Skolem form of ${\displaystyle F}$ is satisfiable.

Proof: Let ${\displaystyle F=\forall y_{1}\cdots \forall y_{n}\exists z\;G}$; after one transformation according to the while-loop we have

${\displaystyle F'=\forall y_{1}\cdots \forall y_{n}\;G[z/f(y_{1},\cdots ,y_{n})}$

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

${\displaystyle {\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

${\displaystyle {\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/v]}(G)=true}$

where ${\displaystyle v={\mathcal {I}}(f(u_{1},\cdots ,u_{n})}$. Hence we have, that for all ${\displaystyle u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}}$ there is a ${\displaystyle v\in U_{\mathcal {I}}}$, where

${\displaystyle {\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/v]}(G)=true}$

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

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

${\displaystyle {\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/v]}(G)=true}$

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

Hence we have that for all ${\displaystyle u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}'}$

${\displaystyle {\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 ${\displaystyle u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}}$

${\displaystyle {\mathcal {I}}'_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}]}(G[z/f^{(}y_{1},\cdots ,y_{n})])=true}$

which means, that ${\displaystyle {\mathcal {I}}'(\forall y_{1}\cdots \forall y_{n}\;G[z/f(y_{1},\cdots ,y_{n})])=true}$, and hence ${\displaystyle {\mathcal {I}}'}$ is a model for ${\displaystyle 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 ${\displaystyle F}$.

• Transform ${\displaystyle F}$ into an equivalent proper ${\displaystyle F_{1}}$ by bounded renaming.
• Let ${\displaystyle y_{1},\cdots ,y_{k}}$ the free variables from ${\displaystyle F_{1}}$. Transform ${\displaystyle F_{1}}$ into ${\displaystyle F_{2}=\exists y_{1}\cdots \exists y_{k}\;F_{1}}$
• Transform ${\displaystyle F_{2}}$ into an equivalent prenex form ${\displaystyle F_{3}}$.
• Transform ${\displaystyle F_{3}}$ into its Skolemform ${\displaystyle F_{4}=\forall x_{1}\cdots \forall x_{l}\;G}$
• Transform ${\displaystyle G}$ into its CNF ${\displaystyle G\prime =(\bigwedge _{i=1}^{n}~(\bigvee _{j=1}^{m}~L_{i,j}))}$ where ${\displaystyle L_{ij}}$ is a literal. This results in ${\displaystyle F_{5}=\forall x_{1}\cdots \forall x_{l}\;G\prime }$
• Write ${\displaystyle F_{5}}$ as a set of clauses:
${\displaystyle F_{6}=\{C_{1},\cdots ,C_{n}\}}$
where ${\displaystyle C_{i}=\{L_{i,1},\cdots ,L_{i,m}\}}$

## Problems

#### Problem 6 (Predicate)

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

${\displaystyle \Box }$

#### Problem 7 (Predicate)

Show the following semantic equivalences:

1. ${\displaystyle \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. ${\displaystyle \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))}$

${\displaystyle \Box }$

#### Problem 8 (Predicate)

Show the following semantic equivalences:

1. ${\displaystyle (\forall xp(x))\to q(b)\equiv \exists x(p(x)\to q(b))}$
2. ${\displaystyle (\forall xr(x))\lor (\exists y\lnot r(y))\equiv (\forall xr(x))\to (\exists yr(y))}$

${\displaystyle \Box }$

#### Problem 9 (Predicate)

Show that for arbitrary formulae ${\displaystyle F}$ and ${\displaystyle G}$, the following holds:

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

${\displaystyle \Box }$