Derivation of Quantifier Negation: $(\exists x)Px \vdash -(\forall x) -Px$

Question

I am trying to figure out the derivation of: $(\exists x)Px \vdash -(\forall x)-Px$

This is my thought process so far is to establish a contradiction on Px and -Px, but i'm struggling with an assumption to contradict to get.

Here's my though process so far:

$ (\exists x) Px\\ -Px\\ Px \wedge -Px\\ contradiction? $

But Im not quite sure how to go from a contradiction on that to $-(\forall x)-Px$, I feel like it would just get me back to $--Px$.

Can anyone provide any suggestions or assistance on how to proceed?

Answer 1

$\def\fitch#1#2{~~~~\begin{array}{|l} #1 \\\hline #2\end{array}}$ That is almost correct, but a negation introduction subproof require assumption of the position you seek to negate.

That is: assume $\forall x~\lnot P(x)$.

$$\fitch{~~1.~\exists x~P(x)}{\fitch{~~2.~\forall x~\lnot P(x)}{\fitch{~~3.~\boxed a~P(a)}{~~4.~\lnot P(a)\hspace{10ex}\forall\mathsf E~2\\~~5.~\bot\hspace{14ex}\neg\mathsf E~3,4}\\~~6.~\bot\hspace{18ex}\exists\mathsf E~1,3{-}5}\\~~7.~\lnot\forall x~\lnot P(x)\hspace{12ex}\neg\mathsf I~2{-}6}$$