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

Question

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.

Answer 1

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.

Answer 2

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

Answer 3

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: