Search code examples
logicfirst-order-logic

can you help me to transform forall FO logical formula to it equivalent not exist formula?

i have this formula

∀x ∀y (A(x,y) V A(y,x) → B(y,c1) ∧ B(x,c2) ∧ c1≠c2)

to the equivalent formula that by using existential quantifier ?

Solution

  • ∀x ∀y X is the same as ¬∃(x, y) ¬X

    'X → Y' is the same as 'There is no counterexample when X but not Y'

    ¬(A(x,y) V A(y,x) → B(x,c1) ∧ B(x,c2) ∧ c1≠c2) = (A(x,y) V A(y,x)) ∧ ¬(B(x,c1) ∧ B(x,c2) ∧ c1≠c2)) - our counterexample. If we put negation of the second part in it and collect everything together, we get:

    ¬∃(x, y) (A(x,y) V A(y,x)) ∧ (¬B(x,c1) v ¬B(x,c2) v c1 = c2)

    Update: replaced ¬∃x ¬∃ y with ¬∃(x, y). I suppose that's what you originally meant, right?