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 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[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=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[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 &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 PPformulae 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 whileloop 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:
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:
 $\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))$
 $\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:
 $(\forall xp(x))\to q(b)\equiv \exists x(p(x)\to q(b))$
 $(\forall xr(x))\lor (\exists y\lnot r(y))\equiv (\forall xr(x))\to (\exists yr(y))$
$\Box$
Problem 9 (Predicate)[edit]
Show that for arbitrary formulae $F$ and $G$, the following holds:
 $\forall x(F\lor G)\not \equiv \forall xF\lor \forall xG$
 If $G=F[x/t]$, than $G\models \exists xF$.
$\Box$