Natural deduction : $\lnot \forall x.P(x) \to \exists x. \lnot P(x)$

Question

I have to prove in the first predicate logic, using natural deduction, that $\lnot \forall x.P(x) \to \exists x. \lnot P(x)$. Any idea?

Answer 1

1) $¬∀xP(x)$ --- premise

2) $\lnot \exists x \lnot P(x)$ --- assumed [a]

3) $\lnot P(x)$ --- assumed [b]

4) $\exists x \lnot P(x)$ --- from 3) by $\exists$-intro

5) $\bot$ --- from 2) and 4)

6) $P(x)$ --- from 3) by Double Negation, discharging [b]

7) $\forall x P(x)$ --- from 6) by $\forall$-intro

8) $\bot$ --- from 1) and 7)

9) $\exists x \lnot P(x)$ --- from 2) by DN, discharging [a].