Converting predicate logic formulas into Skolem Normal Form

Question

I would like to transform the following predicate logic formulas into Skolem Normal Form, simplifying them as much as possible. I am trying to show my working clearly, writing each step in a line of its own and indicating how it was obtained. However I am not sure if I am doing correctly (simplifying in right places, removing enough brackets etc.) and efficiently.

I am trying to use the following skolemization algorithm:

1. Replace all occurrences of →, ↔, ⊕.
2. Move negation inwards.
3. Standardize variables apart.
4. Rewrite existential quantifiers using Skolem Functions.
5. Move universal quantifiers to front.
6. Use the Distributivity Law.

a) $∃x (dog(x) ∧ ∀y (dog(y) → admires(y, x)))$

$$∃x \space (dog(x) ∧ \neg∀y \space (dog(y)\wedge admires(y, x))) \qquad \text{(def. →)}$$ $$∃x \space (dog(x) ∧ ∃y\space \neg(dog(y)\wedge admires(y, x))) \qquad \text{(De Morgan)}$$ $$∃x \space (dog(x) ∧ ∃y\space (\neg dog(y)\vee \neg admires(y, x))) \qquad \text{(De Morgan)}$$ $$∃x_1 \space (dog(x_1) ∧ ∃y_1\space (\neg dog(y_1)\vee \neg admires(y_1, x_1))) \qquad \text{(Standardize)}$$ $$((dog(dog\_x) ∧ (\neg dog(dog\_y)\vee \neg admires(dog\_y, dog\_x))) \qquad \text{(Skolemize)}$$ $$((dog(dog\_x) ∧ (\neg dog(dog\_y))) \vee (dog(dog\_x) ∧ \neg admires(dog\_y, dog\_x))) \qquad \text{(Distributivity)}$$ ... some conversion from Disjunctive to Conjunctive normal form? (unsure how)

b) $∀x (∀y (dog(y) → admires(y, x)) ↔ ∀y (dog(y) → stronger(x, y)))$

$$∀x (∀y (\neg dog(y) \vee admires(y, x)) ↔ ∀y (\neg dog(y) \vee stronger(x, y))) \qquad \text{(def. →)}$$ $$∀x (∀y (\neg dog(y) \vee admires(y, x)) → ∀y (\neg dog(y) \vee stronger(x, y)) )\space ∧ \space (∀y (\neg dog(y) \vee stronger(x, y)) → ∀y (\neg dog(y) \vee admires(y, x))) \qquad \text{(def. ↔)}$$ $$∀x (\neg ∀y (\neg dog(y) \vee admires(y, x)) \vee ∀y (\neg dog(y) \vee stronger(x, y)) )\space ∧ \space (\neg ∀y (\neg dog(y) \vee stronger(x, y)) \vee (∀y (\neg dog(y) \vee admires(y, x))) \qquad \text{(def. →)}$$ $$∀x (∃x \neg(\neg dog(y) \vee admires(y, x)) \vee ∀y (\neg dog(y) \vee stronger(x, y)) )\space ∧ \space (∃x \neg(\neg dog(y) \vee stronger(x, y)) \vee (∀y (\neg dog(y) \vee admires(y, x))) \qquad \text{(De Morgan)}$$ $$∀x (∃x (\neg\neg dog(y) ∧ \neg admires(y, x)) \vee ∀y (\neg dog(y) \vee stronger(x, y)) )\space ∧ \space (∃x (\neg\neg dog(y) ∧ \neg stronger(x, y)) \vee (∀y (\neg dog(y) \vee admires(y, x))) \qquad \text{(De Morgan)}$$ $$∀x (∃x (dog(y) ∧ \neg admires(y, x)) \vee ∀y (\neg dog(y) \vee stronger(x, y)) )\space ∧ \space (∃x (dog(y) ∧ \neg stronger(x, y)) \vee (∀y (\neg dog(y) \vee admires(y, x))) \qquad \text{(Double Negation)}$$ $$∀x (∃x_1 (dog(y) ∧ \neg admires(y, x_1)) \vee ∀y (\neg dog(y) \vee stronger(x_1, y)) )\space ∧ \space (∃x_2 (dog(y) ∧ \neg stronger(x_2, y)) \vee (∀y (\neg dog(y) \vee admires(y, x_2))) \qquad \text{(Standardize)}$$ $$∀x ((dog(y) ∧ \neg admires(y, dog\_x)) \vee ∀y (\neg dog(y) \vee stronger(dog\_x, y)) )\space ∧ \space ((dog(y) ∧ \neg stronger(dog\_z, y)) \vee (∀y (\neg dog(y) \vee admires(y, dog\_z))) \qquad \text{(Skolemize)}$$ ... some distributive step to bring universal quantifiers to front and make matrix conjunctive normal form? (unsure how)

---

Second attempt after reviewing answers: a)

$$∃x \space (dog(x) ∧ ∀y (dog(y) → admires(y, x)))$$

$$∃x \space (dog(x) ∧ ∀y \space (\neg dog(y) ∨ admires(y, x))) \qquad \text{(def. →)}$$

$$∃x ∀y \space (dog(x) ∧ \space (\neg dog(y) ∨ admires(y, x))) \qquad \text{(by Prenex Law)}$$

$$∃x_1 ∀y \space (dog(x_1) ∧ \space (\neg dog(y) ∨ admires(y, x_1))) \qquad \text{(Standardize)}$$

$$∀y \space (dog(dog_x) ∧ \space (\neg dog(y) ∨ admires(y, dog_x))) \qquad \text{(Skolemize) Done!}$$

b)

$$∀x (∀y (dog(y) → admires(y, x)) ↔ ∀y (dog(y) → stronger(x, y)))$$

$$∀x (∀y (\neg dog(y) ∨ admires(y, x)) ↔ ∀y (\neg dog(y) ∨ stronger(x, y))) \qquad \text{(def. →)}$$

$$∀x ((∀y (\neg dog(y) \vee admires(y, x)) → ∀y (\neg dog(y) \vee stronger(x, y)) )\space ∧ \space (∀y (\neg dog(y) \vee stronger(x, y)) → ∀y (\neg dog(y) \vee admires(y, x)))) \qquad \text{(def. ↔)}$$

$$∀x ((\neg ∀y (\neg dog(y) \vee admires(y, x)) \vee ∀y (\neg dog(y) \vee stronger(x, y)) )\space ∧ \space (\neg ∀y (\neg dog(y) \vee stronger(x, y)) \vee ∀y (\neg dog(y) \vee admires(y, x)))) \qquad \text{(def. →)}$$

$$∀x ((∃y \neg(\neg dog(y) \vee admires(y, x)) \vee ∀y (\neg dog(y) \vee stronger(x, y)) )\space ∧ \space (∃y \neg(\neg dog(y) \vee stronger(x, y)) \vee ∀y (\neg dog(y) \vee admires(y, x)))) \qquad \text{(De Morgan)}$$

$$∀x ((∃y (\neg\neg dog(y) ∧ \neg admires(y, x)) \vee ∀y (\neg dog(y) \vee stronger(x, y)) )\space ∧ \space (∃y (\neg\neg dog(y) ∧ \neg stronger(x, y)) \vee ∀y (\neg dog(y) \vee admires(y, x)))) \qquad \text{(De Morgan)}$$

$$∀x ((∃y (dog(y) ∧ \neg admires(y, x)) \vee ∀y (\neg dog(y) \vee stronger(x, y)) )\space ∧ \space (∃y (dog(y) ∧ \neg stronger(x, y)) \vee ∀y (\neg dog(y) \vee admires(y, x)))) \qquad \text{(Double Negation)}$$

$$∀x ∀y (∃y(dog(y) ∧ \neg admires(y, x)) \vee (\neg dog(y) \vee stronger(x, y)) )\space ∧ \space (∃y (dog(y) ∧ \neg stronger(x, y)) \vee (\neg dog(y) \vee admires(y, x)) \qquad \text{(Scope Change)}$$

$$∀x ∀y (∃y_1(dog(y_1) ∧ \neg admires(y_1, x)) \vee (\neg dog(y) \vee stronger(x, y)) )\space ∧ \space (∃y_2 (dog(y_2) ∧ \neg stronger(x, y_2)) \vee (\neg dog(y) \vee admires(y, x)) \qquad \text{(Standardize)}$$

$$∀x ∀y ((dog(dog\_y1) ∧ \neg admires(dog\_y1, x)) \vee (\neg dog(y) \vee stronger(x, y)) )\space ∧ \space ((dog(dog\_y2) ∧ \neg stronger(x, dog\_y2)) \vee (\neg dog(y) \vee admires(y, x)) \qquad \text{(Skolemize)}$$

(distribute ?)

Answer 1

a)

you make a mistake in the very first step:

$\exists x (dog(x) \land \forall y (dog(y) \rightarrow admires(y,x))) \Leftrightarrow $ (by def. $\rightarrow$)

$\exists x (dog(x) \land \forall y (\neg dog(y) \lor admires(y,x)))$

I note that in your algorithm you skolemize the existentials before bringing out (to the front) the quantifiers .. But in the process of binging them out the quantifiers may change (see Prenex 7 and 8 belo). So: first bring out the quantifier and then skolemize. Tip: try and get the existentials out first.

Also, when at the end you have something of the form $P \land (Q \lor R)$ it is already in CNF ... So do not distribute at that point.

Finally, here are some basic rules for pulling a quantifier outside logical operators, where P does not contain any free variables x:

Prenex 1: $P \lor \forall x \: \phi(x) \Leftrightarrow \forall x (P \lor \phi(x))$

Prenex 2: $P \lor \exists x \: \phi(x) \Leftrightarrow \exists x (P \lor \phi(x))$

Prenex 3: $P \land \forall x \: \phi(x) \Leftrightarrow \forall x (P \land \phi(x))$

Prenex 4: $P \land \exists x \: \phi(x) \Leftrightarrow \exists x (P \land \phi(x))$

Prenex 5: $P \rightarrow \forall x \: \phi(x) \Leftrightarrow \forall x (P \rightarrow \phi(x))$

Prenex 6: $P \rightarrow \exists x \: \phi(x) \Leftrightarrow \exists x (P \rightarrow \phi(x))$

Prenex 7: $\forall x \: \phi(x) \rightarrow P \Leftrightarrow \exists x (\phi(x) \rightarrow P)$

Prenex 8: $\exists x \: \phi(x) \rightarrow P \Leftrightarrow \forall x (\phi(x) \rightarrow P)$

So take care of those last two: the quantifier changes if you pull it outside a conditional, and it is the antecedent of that conditional!

And because of the latter, there is no simple equivalence involving pulling a quantifier outside a biconditional.

OK, so for b)

You're good up to this point:

$$∀x ((∃y (dog(y) ∧ \neg admires(y, x)) \vee ∀y (\neg dog(y) \vee stronger(x, y)) )\space ∧ \space (∃y (dog(y) ∧ \neg stronger(x, y)) \vee ∀y (\neg dog(y) \vee admires(y, x))))$$

Now you want to pull your quantifiers out, but first you should rename the variables, otherwise quantifiers will 'capture' variables that they were not quantifying. So:

$$∀x ((∃y_1 (dog(y_1) ∧ \neg admires(y_1, x)) \vee ∀y_2 (\neg dog(y_2) \vee stronger(x, y_2)) )\space ∧ \space (∃y_3 (dog(_3) ∧ \neg stronger(x, y_3)) \vee ∀y_4 (\neg dog(y_4) \vee admires(y_4, x))))$$

OK, since you worked everything down to the boolean connectives $\land$, $\lor$, and $\not$, and you have worked any $\not$'s inside the quantifiers, we can pull the quantifiers out as they are. Again, I recoemmend pulling out the existentials first. So:

$$∀x ∃y_1 ∃y_3 ∀y_2 ∀y_4 (( (dog(y_1) ∧ \neg admires(y_1, x)) \vee (\neg dog(y_2) \vee stronger(x, y_2)) )\space ∧ \space ( (dog(_3) ∧ \neg stronger(x, y_3)) \vee (\neg dog(y_4) \vee admires(y_4, x))))$$

And yes, for you final step, distribute any $\lor$'s over $\land$'s:

$$∀x ∃y_1 ∃y_3 ∀y_2 ∀y_4 (( (dog(y_1) \lor (\neg dog(y_2) \vee stronger(x, y_2))) ∧ (\neg admires(y_1, x) \vee (\neg dog(y_2) \vee stronger(x, y_2))) )\space ∧ \space ( (dog(_3) \vee (\neg dog(y_4) \vee admires(y_4, x))) ∧ (\neg stronger(x, y_3) \vee (\neg dog(y_4) \vee admires(y_4, x))))$$

And we can drop some parentheses because of association:

$$∀x ∃y_1 ∃y_3 ∀y_2 ∀y_4 ( (dog(y_1) \lor \neg dog(y_2) \vee stronger(x, y_2) ∧ (\neg admires(y_1, x) \vee \neg dog(y_2) \vee stronger(x, y_2) ) \space ∧ \space (dog(_3) \vee \neg dog(y_4) \vee admires(y_4, x)) ∧ (\neg stronger(x, y_3) \vee \neg dog(y_4) \vee admires(y_4, x))$$

Answer 2

For $(a)$ you can use truth tables. Compute the whole truth table of your formula: \begin{array} pp & q & r & s & (p\wedge\neg q)\vee(r\wedge \neg s) & CNF\\ 0 & 0 & 0 & 0 & \underline0 & \_\_\_\_\_ \\ 0 & 0 & 0 & 1 & \underline0 & \_\_\_\_\_ \\ 0 & 0 & 1 & 0 & \underline1 & \_\_\_\_\_ \\ 0 & 0 & 1 & 1 & \underline0 & \_\_\_\_\_ \\ 0 & 1 & 0 & 0 & \underline0 & \_\_\_\_\_ \\ 0 & 1 & 0 & 1 & \underline0 & \_\_\_\_\_ \\ 0 & 1 & 1 & 0 & \underline1 & \_\_\_\_\_ \\ 0 & 1 & 1 & 1 & \underline0 & \_\_\_\_\_ \\ 1 & 0 & 0 & 0 & \underline1 & \_\_\_\_\_ \\ 1 & 0 & 0 & 1 & \underline1 & \_\_\_\_\_ \\ 1 & 0 & 1 & 0 & \underline1 & \_\_\_\_\_ \\ 1 & 0 & 1 & 1 & \underline1 & \_\_\_\_\_ \\ 1 & 1 & 0 & 0 & \underline0 & \_\_\_\_\_ \\ 1 & 1 & 0 & 1 & \underline0 & \_\_\_\_\_ \\ 1 & 1 & 1 & 0 & \underline1 & \_\_\_\_\_ \\ 1 & 1 & 1 & 1 & \underline0 & \_\_\_\_\_ \\ \end{array} Now, knowing the values, you can construct your function in CNF.

For $(b)$, you made an error in the fourth step (from Def $\rightarrow$ to De Morgan) you changed the variable $y$ for an $x$. If you correct that i think you can, straightforward, get the universal quantifiers to the front and use the same principle to bring it to $CNF$.