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

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?

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

• I don't understand what 3 and 6 are supposed to mean, with $x$ being unquantified. Or is that the $\forall$ intro in 7? (I'm not familiar with natural deduction in particular.) – Ian Jan 6 '16 at 20:12
• @Ian - see Natural Deduction for an explanation of the rules. – Mauro ALLEGRANZA Jan 6 '16 at 20:15
• @Ian - 3) and 6) are formula with free variables. They are not "specific" of ND; every first-order language has formulae with free vars. – Mauro ALLEGRANZA Jan 6 '16 at 20:16