# How to prove the validity of $¬∃x P(x) ⊢ ∀x ¬P(x)$ in predicate logic

I think that I need to assume $¬∀x ¬P(x)$ and then do a proof by contradiction but I am not sure if that is correct or how to go about it.

We need contradiction in the proof (but it is not a poof by contradiction) :

1) $\lnot \exists x \ Px$ --- premise

2) $\quad\quad| \quad Px$ --- assumed [a]

3) $\quad\quad| \quad \exists x \ Px$ --- from 2) by $\exists$-intro

4) $\quad\quad| \quad\bot$ --- contradiction! from 1) and 3)

5) $\lnot Px$ --- from 2)-4) by $\lnot$-intro, discharging [a]

6) $\forall x \ \lnot Px$ --- from 5) by $\forall$-intro.

• Would steps 2-4 be a subproof? If I make that a subproof and assume $[a]P(a)$ then step 5 - $¬Px$ is not a sentence. – Daryn Wilkinson Mar 7 '18 at 8:36
• In step 5 I am not able to cite steps 2 and 4. I have to select the whole sub proof which doesn't work. – Daryn Wilkinson Mar 7 '18 at 8:53
• @DarynWilkinson - you can freely modify the proof to adapt it to your needs... :-) – Mauro ALLEGRANZA Mar 7 '18 at 8:55
• ∀-intro needs a sub proof cited. I can't just reference step 5. – Daryn Wilkinson Mar 7 '18 at 8:58
• @DarynWilkinson The subproof is the introduction of an arbitrary element $c$, for which is proven must be $\neg Pc$. – Graham Kemp Mar 7 '18 at 9:00

Here is a proof for that in Fitch. Exact same idea as Mauro's proof but it does not have free variables anywhere which, it seems, your proof system does not want either:

We have for any proposition $Q$ not containing $x$ free, $(\exists x.P(x))\to Q\vdash \forall x.(P(x)\to Q)$. This is constructively true. Assume $P(c)$ for some arbitrary $c$, then use modus ponens on the assumption after introducing an existential, then generalize as $c$ is arbitrary. As a lambda term, it is basically currying. If you choose $Q\equiv\bot$, you get your statement using the fact that (even constructively) $\neg P\equiv P\to \bot$.