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

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?

• $t$ is a term whatever of the language. We have at least variables as terms. – Mauro ALLEGRANZA Apr 7 at 19:13
• This isn't a constructively true statement, so start with $\phi \lor \lnot \phi$ and do proof by cases (which is or elimination). – DanielV Apr 7 at 21:24

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].

• Many thanks for the proof. – Sha Vuklia Apr 7 at 19:13