Removing Implication in the Conversion of WFF to Clausal Form

155 Views Asked by At

I understand the conversion algorithm, my concern is regarding the first step of 'Removing Implication'.

Example: In the following figure when one removes implication, the negation comes before ∀z.

However, in other example (given below) the negation when removing implies comes after ∀x and before ∃z.

∀x [Roman(x) ∧ know(x, Marcus)] → [hate(x, Caesar) ∨ (∀y ∃z hate(y, z) → thinkCrazy(x, y))]

∀x ~[Roman(x) ∧ know(x, Marcus)] ∨ [hate(x, Caesar)  ∨ (∀y ~(∃z hate(y, z)) ∨ thinkCrazy(x, y))]

I found a similar example here where ~ is placed after .

I am confused about the placement of ~ while performing the first step during the conversion. What is the criteria of negating the implication when there exists either of the two quantifiers?

1

There are 1 best solutions below

1
On

It depends on the order of operations by which you parse $\forall x~\phi\to \psi$

$$\color{crimson}(\forall x~\phi\color{crimson})~\to~\psi\iff \lnot\color{crimson}(\forall x~\phi\color{crimson})~\lor~\psi\\\forall x~~\color{crimson}(\phi\to \psi\color{crimson})\iff \forall x~~\color{crimson}(\lnot \phi\lor \psi\color{crimson})$$

The former is the usual convention, but it looks like your other source uses the later.

Unfortunately different authors use different conventions, so it can often be confusing if they don't clearly establish which operation has priority.

When it is ambiguous, use parenthesis.