Propositional Logic - There Exists dual

[Goldenwind]

Propositional Logic - "There Exists" dual

Homework Statement

"State and prove the $\exists$-dual of 6.1.8"

Section 6.1.8 shows how to change $\vdash (\forall x)(\forall y)A \equiv (\forall y)(\forall x)A$ via this method:

(Line 1) $(\forall x)(\forall y)A$ (Hypothesis)
(Line 2) $(\forall y)A$ (Line 1 + spec)
(Line 3) $A$ (Line 2 + spec)
(Line 4) $(\forall x)A$ (Line 3 + gen; Line 1 has no free x)
(Line 5) $(\forall y)(\forall x)A$ (Line 4 + gen; Line 1 has no free y)

The $\exists$-dual of this would be to show $\vdash (\exists x)(\exists y)A \equiv (\exists y)(\exists x)A$.

Homework Equations

A crucial formula here is that $(\forall x)A \equiv \neg (\exists x) \neg A$

The Attempt at a Solution

I potentially solved it, but something seems off.

This is what I did:

$\vdash (\exists x)(\exists y)A \equiv (\exists y)(\exists x)A$

(Line 1) $(\exists x)(\exists y)A$
(Line 2) $\neg (\forall x)\neg (\exists y)A$ Definition of $\exists$
(Line 3) $\neg (\forall x)\neg \neg (\forall y)\neg A$ Definition of $\exists$
(Line 4) $\neg (\forall x)(\forall y)\neg A$ Double negative
(Line 5) $\neg (\forall y)\neg A$ Spec
(Line 6) $\neg \neg A$ Spec
(Line 7) $\neg (\forall x)\neg A$ Gen
(Line 8) $\neg (\forall y)(\forall x)\neg A$ Gen
(Line 9) $\neg (\forall y)\neg \neg (\forall x)\neg A$ Double negative
(Line 10) $\neg (\forall y)\neg (\exists x)A$ Definition of $\forall$
(Line 11) $(\exists y)(\exists x)A$ Definition of $\forall$

What worries me is going from Line 5 to 6, what happens to the first $\neg$ symbol? Can I just leave it there, and then insert my $(\forall x)$ between the two $\neg$s in Line 7 like that?

 

[mighty2000]

Thank you for your post on propositional logic and the dual of "there exists." I would like to provide a response as a scientist in this field.

Firstly, your attempt at a solution is on the right track. However, there is a small error in your reasoning. In line 5, you correctly apply the specialization rule to remove the existential quantifier for y. This gives you \neg (\forall y)\neg A. However, in line 6, you have incorrectly applied the specialization rule again. Instead, you should use the double negation rule to get \neg \neg A. This is because the negation of a universal quantifier is equivalent to a double negation.

After this, you can continue with your proof and follow the same steps as you did in the original proof for the dual of "for all." The final lines of your proof should be:

(Line 10) \neg (\forall y)\neg (\exists x)A (Definition of \forall)
(Line 11) (\exists y)(\exists x)A (Definition of \exists)

To address your concern about the first negation symbol, you can simply leave it there or remove it using the double negation rule. Both ways are valid.

I hope this helps in understanding the dual of "there exists." Remember, when dealing with propositional logic, it is important to carefully apply the rules and laws to ensure a valid proof. Keep up the good work and continue exploring the fascinating world of logic!