Equivalence of formulae is defined as in the propositional case:
The formulae
and
are called (semantically)
equivalent, if for all interpretations
for
and
,
. We write
.
The equivalences from the propositional case in theorem 4
equivalences hold and in addition we have the following
cases for quantifiers.
The following equivalences hold:
If
does not occur free in
:
Proof: We will prove only the equivalence
with
has no free occurrence in
, as an example.
Assume an interpretation
such that
![{\displaystyle {\text{iff }}{\mathcal {I}}(\forall xF)=true{\text{ and }}{\mathcal {I}}(G)=true}](https://wikimedia.org/api/rest_v1/media/math/render/svg/896d24f453cfc1891636ff62c7c8e71c9a76b045)
![{\displaystyle {\text{iff }}{\text{ for all }}d\in U:{\mathcal {I}}_{[x/d]}(F)=true{\text{ and }}{\mathcal {I}}(G)=true}](https://wikimedia.org/api/rest_v1/media/math/render/svg/859b5f3c48e626bee90d1ae81310579fc245ebf3)
![{\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)}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/19df559bef7a1455f0e34db2cfffed4a0f8f1b2d)
![{\displaystyle {\text{iff }}{\text{ for all }}d\in U:{\mathcal {I}}_{[x/d]}((F\land G))=true}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e886699d28ee1ee66d2bab1c55e7cfc0778775c6)
![{\displaystyle {\text{iff }}{\mathcal {I}}(\forall x(F\land G))=true.}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ba47570c4b4bf583951111d9e287b66717679e6c)
Note that the following symmetric cases do not hold:
is not equivalent to
is not equivalent to
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 \equiv ((\lnot \exists xP(x,y)\land \lnot \forall zQ(z))\land \exists wP(f(a,w)))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2574dec14d09039104bbdcfc4fea440955914a86)
![{\displaystyle \equiv ((\forall x\lnot P(x,y)\land \exists z\lnot Q(z))\land \exists wP(f(a,w)))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d019cb70a1a1dc994baa686bbc8ea37e7b5ff9eb)
![{\displaystyle \equiv (\exists wP(f(a,w))\land (\forall x\lnot P(x,y)\land \exists z\lnot Q(z)))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7ecceb692f707cea822e69c91392ff54e38957c1)
![{\displaystyle \equiv \exists w(P(f(a,w))\land \forall x(\lnot P(x,y)\land \exists z\lnot Q(z)))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ff6cec2230a6faa4e5530963ca50ac2312403a7c)
![{\displaystyle \equiv \exists w(\forall x(\exists z\lnot Q(z)\land \lnot P(x,y))\land P(f(a,w)))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2e87a971edcb5e9bc438567327c340aff2160156)
![{\displaystyle \equiv \exists w(\forall x\exists z(\lnot Q(z)\land \lnot P(x,y))\land P(f(a,w)))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/53e245563dacdf779337443a06283f797aecf422)
![{\displaystyle \equiv \exists w\forall x\exists z((\lnot Q(z)\land \lnot P(x,y))\land P(f(a,w)))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/6b2019a95fcf78faec79be705288632a037db9d0)
Let
be a formula,
a variable and
a term.
is
obtained from
by substituting every free occurrence of
by
.
Note, that this notion can be iterated:
and that
may contain free occurrences of
.
Let
be a formula,
a variable and
a term.
Let
be a formula, where
and
a variable without an occurrence in
, then
A formula is called proper if there is no variable which
occurs bound and free and after every quantifier there is a distinct
variable.
For every formula
there is a formula
which is proper and
equivalent to
.
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))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9f1263d466430893a0972598b9aebbb80a0e688f)
has the equivalent and proper formula
A formula is called in prenex form if it has the form
, where
with no
occurrences of a quantifier in
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)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2b845cbd0c014bd08073aec42cad7fce6309f93f)
![{\displaystyle \forall x\exists y\;(p(x,g(y,f(x))\lor \lnot q(z))\lor \exists x\;\lnot r(x,z)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/12e039510daf06ecc7b522910eafe9db7c05ed57)
![{\displaystyle \forall x\exists y\;(p(x,g(y,f(x))\lor \lnot q(z))\lor \exists v\lnot r(v,z)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/85f973f132af38534a74c77a914b11e636da4bba)
![{\displaystyle \forall x\exists y\exists v\;(p(x,g(y,f(x))\lor \lnot q(z))\lor \lnot r(v,z)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8bcd0c72754cd3b407e1902457b11ca239ab5519)
Proof: Induction over the structure of the formula gives us
the theorem for an atomic formula immediately.
: There is a
with
, which is equivalent to
. Hence we have
![{\displaystyle F\equiv {\overline {Q_{1}}}y_{1}\cdots {\overline {Q_{n}}}y_{n}\lnot G'}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0006066f5137ff2fb7ba2e37353bd5a07c66cf74)
where
with
. There exists
which are proper and in prenex form and
and
. With bounded renaming we can construct
![{\displaystyle G_{1}=Q_{1}y_{1}\cdots Q_{k}y_{k}G_{1}'}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8f3e2025cfdce200f9184cdd35a0824b4f90a398)
![{\displaystyle G_{2}=Q_{1}'z_{1}\cdots Q_{l}'z_{l}G_{2}'}](https://wikimedia.org/api/rest_v1/media/math/render/svg/de4532ba55e1db456422976ffa1469129328ae82)
where
and hence
In the following we call proper formulae in prenex form PP-formulae or PPF’s.
Let
be a PPF. While
contains a
-Quantifier, do the
following transformation:
has the form
where
is a PPF and
is a
-ary function symbol, which does
not occur in
.
Let
be
If there exists no more
-quantifier,
is in
Skolem form.
Let
be a PPF.
is satisfiable iff the Skolem form of
is
satisfiable.
Proof: Let
; 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})}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8d1c37f359b70da1ed57431e7e4086dcbdd1544c)
where
is a new function symbol.
We have to prove that this transformation is satisfiability
preserving:
Assume
is satisfiable. than there exists a model
for
is an interpretation for
. From the model
property we have for all
![{\displaystyle {\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}]}(G[z/f(y_{1},\cdots ,y_{n})])=true}](https://wikimedia.org/api/rest_v1/media/math/render/svg/18e8949c811b23af57043b23815659158c2af296)
From Lemma 1 we conclude
![{\displaystyle {\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/v]}(G)=true}](https://wikimedia.org/api/rest_v1/media/math/render/svg/219ab93a1d75b18afa03e4925afe072b5daea370)
where
. Hence we have, that for all
there is a
, where
![{\displaystyle {\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/v]}(G)=true}](https://wikimedia.org/api/rest_v1/media/math/render/svg/219ab93a1d75b18afa03e4925afe072b5daea370)
and hence we have, that
, which
means, that
is a model for
.
For the opposite direction of the theorem, assume that
has a
model
. Then we have, that for all
,
there is a
, where
![{\displaystyle {\mathcal {I}}_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/v]}(G)=true}](https://wikimedia.org/api/rest_v1/media/math/render/svg/219ab93a1d75b18afa03e4925afe072b5daea370)
Let
be an interpretation, which deviates from
only, by the
fact that it is defined for the function symbol
, where
is
not defined. We assume that
, where
is chosen according to the above equation.
Hence we have that for all
![{\displaystyle {\mathcal {I}}'_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}][z/f^{{\mathcal {I}}'}(u_{1},\cdots ,u_{n})]}(G)=true}](https://wikimedia.org/api/rest_v1/media/math/render/svg/193d17c81a1c9c2797dc9338e29dca5b13d1f764)
and from Lemma 1 we conclude that for all
![{\displaystyle {\mathcal {I}}'_{[y_{1}/u_{1}]\cdots [y_{n}/u_{n}]}(G[z/f^{(}y_{1},\cdots ,y_{n})])=true}](https://wikimedia.org/api/rest_v1/media/math/render/svg/c82b162a69a8aa0c26ba99eb3b2f547f3b5520a0)
which means, that
, and hence
is a model for
.
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
.
- Transform
into an equivalent proper
by bounded renaming.
- Let
the free variables from
. Transform
into ![{\displaystyle F_{2}=\exists y_{1}\cdots \exists y_{k}\;F_{1}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/00124ec77d383e00943cf2e4e9e3e85ebedf86fa)
- Transform
into an equivalent prenex form
.
- Transform
into its Skolemform ![{\displaystyle F_{4}=\forall x_{1}\cdots \forall x_{l}\;G}](https://wikimedia.org/api/rest_v1/media/math/render/svg/153eb4fd6360399f84d326785ca2391774bea35b)
- Transform
into its CNF
where
is a literal. This results in ![{\displaystyle F_{5}=\forall x_{1}\cdots \forall x_{l}\;G\prime }](https://wikimedia.org/api/rest_v1/media/math/render/svg/b85d6774636f6702d7f89fa6bb817b145d5ef3ca)
- Write
as a set of clauses:
where
Let
be a formula,
a variable and
a term. Then
denotes the formula which results from
by replacing every free
occurrence of
by
. Give a formal definition of this three argument function
, by induction over the structure of
the formula
.
Show the following semantic equivalences:
![{\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))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a8f694c8699c35e4f572435035260d397446008a)
![{\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))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/698150b6e3c8a4c96b45ac92d5f44e338093c9eb)
Show the following semantic equivalences:
![{\displaystyle (\forall xp(x))\to q(b)\equiv \exists x(p(x)\to q(b))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8b0598ed6a39e775314428d5019a23b1c0393f10)
![{\displaystyle (\forall xr(x))\lor (\exists y\lnot r(y))\equiv (\forall xr(x))\to (\exists yr(y))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f539b759dd577b6aa914463efe1ac88f303efea9)
Show that for arbitrary formulae
and
, the following holds:
![{\displaystyle \forall x(F\lor G)\not \equiv \forall xF\lor \forall xG}](https://wikimedia.org/api/rest_v1/media/math/render/svg/d5208c798e42e5e51967a2625434aedd0802b0d2)
- If
, than
.