Show $\neg(\forall x\phi)\vdash \exists x(\neg \phi)$ using an ND-derivation

Question

I'm trying to show that $\neg(\forall x\phi)\vdash \exists x(\neg \phi)$ through a natural deduction (ND) derivation.

I'm kind of stuck, because I don't see how I can find some $t$ such that we have $\neg\phi\frac{t}{x}$, which would give us $\exists x(\neg \phi)$ through the introduction of the existential quantifier.

I was trying to derive in some subderivation that we have $\forall x\phi$, and then that would yield $\perp$, which could maybe contradict the assumption $\phi\frac{t}{x}$, which would then yield to $\neg\phi\frac{t}{x}$ - but that's just an idea, and I can't really formalise it in an ND-derivation.

Could someone help me out?

Answer 1

Using Natural Deduction :

1) $¬(∀xϕ)$

2) $¬∃x(¬ϕ)$ --- assumed [a]

3) $¬ϕ[x/a]$ --- assumed [b]

4) $∃x(¬ϕ)$ --- from 3) by $∃$-intro

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

6) $ϕ[x/a]$ --- from 3) and 5) by Double Negation, discharging [b]

7) $∀xϕ$ --- from 6) by $∀$-intro

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

9) $∃x(¬ϕ)$ --- from 2) and 8) by Double Negation, discharging [a].