# Propositional Logic - There Exists dual

1. Dec 3, 2007

### Goldenwind

Propositional Logic - "There Exists" dual

1. The problem statement, all variables and given/known data
"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$.

2. Relevant equations
A crucial formula here is that $(\forall x)A \equiv \neg (\exists x) \neg A$

3. 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?