Conversion from FOL formula into CNF

Question

I need some help to convert the following FOL formula into CNF?:

∀x((duck(x)∧∀y(duckling(y,x)→cannotswim(y)))→worried(x))

My attempt:

Step 1: ∀x((duck(x)∧∀y (¬duckling(y,x)∨ cannotswim(y))→worried(x))

Step 2: ∀x∀y((duck(x)∧ ¬(¬duckling(y,x)∨ cannotswim(y)) ∨ worried(x))

Step 3: ∀x∀y ¬duck(x)∧ duckling(y,x) ∨ ¬cannotswim(y)∨ worried(x)

Step 4: After removinf universal quantifier and introducing Skolem constant:

R1) duckling(A,B) ∨ ¬cannotswim(B)∨ worried(A)

R2) ¬duck(A)

Is this correct or do I seem to be doing it OK??

2nd Attempt:

Step 1:∀x ((duck(x)→ ∃y (¬duckling(y,x) ∨ cannotswim(y))) → worried(x))

Step 2: ∃x (¬duck(x)∨ (∃Y (¬duckling(y,x)∨ cannotswim(y))) → worried(x))

Step 3: ¬(∃x (¬duck(x)∨ (∃Y (¬duckling(y,x)∨ cannotswim(y))) ∨ worried(x))

Step 4: ∀x ∀y(¬duck(x) ∧ duckling(y,x) ∧ ¬cannotswim(y) ∨ worried(x))

Answer 1

∀x((duck(x)∧∀y(duckling(y,x)→cannotswim(y)))→worried(x))

You are rushing and confusing yourself. Be like a doctor: have patience, and opperate on one bit at a time.

Also, for clarrity abbreviate so you are not looking at (and copying) a long string.

$0.\qquad\forall x~\Big(\big(Dx\wedge \forall y~(Lyx \to Cy)\big)\to Wx\Big)$

The first step should be to use conditional equivalence: $\phi\to \psi\iff \neg \phi\vee\psi$. To avert confusion, do one application at a time.

$1.\qquad{\forall x~\Big(\color{red}\neg\big(Dx\wedge \forall y~(Lyx \to Cy)\big)\color{red}\vee Wx\Big)}$

Don't rush ahead to negate anything yet.   We may as well apply conditional equivalence again.

$2.\qquad{\forall x~\Big(\neg\big(Dx\wedge \forall y~(\underline{\phantom{\color{red}\neg Lyx \color{red}\vee Cy}})\big)\vee Wx\Big)}$

Now should be to use DeMorgan's Rule for the negation of a conjunction: $\neg(\phi\wedge \psi) \iff (\neg \phi\vee\neg\psi)$.

$3.\qquad\phantom{\forall x~\Big(\big(\color{red}\neg Dx\color{red}\vee \color{red}\neg\forall y~(\neg Lyx \vee Cy)\big)\vee Wx\Big)}$

Dual negate that inner quantifier. $\neg\forall z~\varphi \iff \exists z~\neg \varphi$

$4.\qquad\phantom{\forall x~\Big(\big(\neg Dx \vee \color{red}\exists y~\color{red}\neg(\neg Lyx \vee Cy)\big)\vee Wx\Big)}$

Apply deMorgan's Rule for negation of a disjunction. $\neg(\phi\vee \psi) \iff (\neg\phi\wedge\neg\psi)$.

$5.\qquad\phantom{\forall x~\Big(\big(\neg Dx \vee \exists y~(\color{red}\neg\neg Lyx \color{red}\wedge\color{red}\neg Cy)\big)\vee Wx\Big)}$

Apply double negation elimination if you got them.

$6.\qquad\phantom{\forall x~\Big(\big(\neg Dx \vee \exists y~(Lyx \wedge \neg Cy)\big)\vee Wx\Big)}$

You may distribute the quantifier if you want to.

$7.\qquad\phantom{\forall x~\color{red}{\exists y}~\Big(\big(\neg Dx \vee (Lyx \wedge \neg Cy)\big)\vee Wx\Big)}$

Disjunction is associative, so some bracktets can be considered redundant; but not all of them.

$8.\qquad\forall x~{\exists y}~\Big(\neg Dx \vee (Lyx \wedge \neg Cy)\vee Wx\Big)$

Answer 2

You made three mistakes:

First, the relevant equivalence is:

$$\forall x \varphi(x) \rightarrow \psi \Leftrightarrow \exists x ( \varphi(x) \rightarrow \psi)$$

Why? This is because:

$$\forall x \ \varphi(x) \rightarrow \psi \Leftrightarrow $$

$$\neg \forall x \ \varphi(x) \lor \psi \Leftrightarrow $$

$$\exists x \ \neg \varphi(x) \lor \psi \Leftrightarrow $$

$$\exists x (\neg \varphi(x) \lor \psi) \Leftrightarrow $$

$$\exists x ( \varphi(x) \rightarrow \psi)$$

So, your $\forall y$ will end up as a $\exists y$ once it's in the front.

Second, you treated the body as if it were of the form $P \land (Q \rightarrow R)$ (and hence you changed it into $P \land (\neg Q \lor R)$), but the body is of them form $(P \land Q) \rightarrow R$

Third, you only get Skolem constants for existentials, not universals. So, you shouldn't have gotten any Skolem constants in Step 4.