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?

  • $\begingroup$ $t$ is a term whatever of the language. We have at least variables as terms. $\endgroup$ – Mauro ALLEGRANZA Apr 7 at 19:13
  • $\begingroup$ This isn't a constructively true statement, so start with $\phi \lor \lnot \phi$ and do proof by cases (which is or elimination). $\endgroup$ – 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].

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.