Proof for $∃xA⇔¬∀x¬A$

Question

I want to prove, that $∃xA⇔¬∀x¬A$, using classic axioms. I think, I have to start with the following step:

$∃xA⇔∃x¬¬A$

But I do not know, how to make this step, using axioms:

$∃x¬¬A⇔¬∀x¬A$

Answer 1

It is quite easy with Natural Deduction.

(i) $∃xA(x) \rightarrow ¬∀x¬A(x)$

(1) $∀x¬A(x)$ --- assumed [a]

(2) $¬A(x)$ --- from (1) by $\forall$-E

(3) $∃xA(x)$ --- assumed [b]

(4) $A(x)$ --- assumed [c] for $\exists$-E

(5) $\bot$ --- from (4) and (2) by $\rightarrow$-E

(6) $\bot$ --- from (3), (4) and (5) by $\exists$-E, discharging [c]

(7) $¬∀x¬A(x)$ --- from (1) and (7) by $\rightarrow$-I, discharging [a]

(8) $∃xA(x) \rightarrow ¬∀x¬A(x)$ --- from (3) and (7) by $\rightarrow$-I, discharging [b]

---

(ii) $¬∀x¬A(x) \rightarrow ∃xA(x)$

(1) $¬∃xA(x)$ --- assumed [a]

(2) $A(x)$ --- assumed [b]

(3) $∃xA(x)$ --- from (2) by $\exists$-I

(4) $\bot$ --- from (1) and (3) by $\rightarrow$-E

(5) $¬A(x)$ --- from (2) and (4) by $\rightarrow$-I, discharging [b]

(6) $∀x¬A(x)$ --- from (5) by $\forall$-I

(7) $¬∀x¬A(x)$ --- assumed [c]

(8) $\bot$ --- from (6) and (7) by $\rightarrow$-E

(9) $∃xA(x)$ --- from (1) and (8) by Double Negation, discharging [a]

(10) $¬∀x¬A(x) \rightarrow ∃xA(x)$ --- from (7) and (9) by $\rightarrow$-I, discharging [c]