predicate logic in clause form

Question

can somebody tell me how to convert a formula to its corresponding clause form step by stepi?

$¬(∀x∃y P(x,y) → (∀y∃z ¬Q(x,z)∧∀y¬∀z R(y,z))$

i know the formua has to be transformed into cnf fisrt im a bit confused on the first step which is to transform the original formula to rectified form. my teacher told me the only thing i have to do is to check if there is any same variable with quantifiers. then rename it. is it true? can somebody answer the above question step by step so i can watch and learn??

Answer 1

See Mordechai Ben-Ari, Mathematical Logic for Computer Science (3rd ed - 2012), page 174.

In order to get the CNF for a closed formula of f-o logic, we have to :

Step 1: Rename bound variables so that no variable appears in two quantifiers

Step 2: Eliminate all binary Boolean operators other than ∨ and ∧

Step 3: Push negation operators inward, collapsing double negation, until they apply to atomic formulas only.

Step 4: Extract quantifiers from the matrix. Choose an outermost quantifier, that is, a quantifier in the matrix that is not within the scope of another quantifier still in the matrix. Repeat until all quantifiers appear in the prefix and the matrix is quantifier-free.

Step 5: Use the distributive laws to transform the matrix into CNF.

Now with your example : rename bound variables :

$\lnot (∀x∃yP(x,y)→(∀v∃u¬Q(v,u)∧∀w¬∀zR(w,z)))$ --- I suppose that $∀y∃z¬Q(x,z)∧...$ is a misprint for $∀x∃z¬Q(x,z)∧...$

remove $\rightarrow$ [we have tu use the equivalence between : $p \rightarrow q$ and $\lnot p \lor q$] :

$\lnot (\lnot ∀x∃yP(x,y) \lor (∀v∃u¬Q(v,u)∧∀w¬∀zR(w,z)))$

push $\lnot$ inwards [we have to use (more than one time) De Morgan laws and the equivalence between $\lnot \forall$ and $\exists \lnot$, etc. and, of course, double negation] :

$∀x∃yP(x,y) \land \lnot ((∀v∃u¬Q(v,u)∧∀w∃z\lnot R(w,z)))$

and again :

$∀x∃yP(x,y) \land (∃v∀uQ(v,u) \lor ∃w∀zR(w,z))$

Then we have to move the quantifiers upfront :

$∀x∃yP(x,y) \land (∃v∀u∃w∀z(Q(v,u) \lor R(w,z))$

$∀x∃y∃v∀u∃w∀z(P(x,y) \land (Q(v,u) \lor R(w,z)))$.