Valid Formula in First Order Logic

Question

I am a little confused about the validity of first order logic formulas.

How we can using formal notation to prove the following is VALID?

$ \exists x \exists y p(x,y) \to \neg \forall x \forall y \neg p(x,y)$

Answer 1

You have to note that : $\lnot \forall$ is equivalent to $\exists \lnot$.

Thus the formula :

$∃x∃yp(x,y) \to ¬∀x∀y¬p(x,y)$ is equivalent to :

$∃x∃yp(x,y) → ∃x∃y¬¬p(x,y)$.

By double negation, this amounts to the valid formula :

$∃x∃yp(x,y) → ∃x∃yp(x,y)$.

---

For a "formal" proof we can use Natural Deduction to show that :

$∃x∃yp(x,y) \vdash ¬∀x∀y¬p(x,y)$.

Answer 2

Proof: Just switch both quantifiers and remove the resulting double negation.

1. $\exists x: \exists y: P(x,y)$ (Premise)

2. $\neg \forall x: \neg \exists y: P(x,y)$ (Switch Quantifier)

3. $\neg \forall x: \neg \neg \forall y: \neg P(x,y)$ (Switch Quantifier)

4. $\neg \forall x: \forall y: \neg P(x,y)$ (Remove $\neg\neg$)

5. $\exists x: \exists y: P(x,y)\implies \neg \forall x: \forall y: \neg P(x,y)$ (Conclusion)