quantifier negation proof with natural deduction?

Question

How can I derive ∃¬()⊢¬∀()? I know that I need to derive some sort of contradiction, but what do I assume?

Answer 1

$ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\ni#1{\qquad\mathbf{\neg I} \: #1 \\} $

How can I derive $\exists x\neg P(x) \vdash \neg \forall xP(x)$ ?

You are trying to find a proof of $\neg \forall xP(x)$. This sentence is going to be the last line of your proof. Look at $\neg \forall xP(x)$ and see what the introduction rule for its main logical connective is (the last connective used when building the sentence. In this case, it is a negation. Looking at Negation Introduction rule schema, where $\mathcal A$ is a metavariable standing for any sentence:

$ \fitch{}{ \fitch{i.\, \mathcal A}{ j. \bot }\\ \neg \mathcal A \ni{i-j} } $

We see that, assuming $\forall xP(x)$ and reaching a contradiction it is enough to justify its application. Your main proof should have roughly this skeleton:

$ \fitch{1.\, \exists x\neg P(x)}{ \fitch{2.\, \forall x P(x)}{ \vdots\\ \bot }\\ \neg \forall xP(x) } $

Can you continue the proof ?

EDIT: I leave full proof as reference.

$ \fitch{1.\, \exists x\neg P(x)}{ \fitch{2.\, \forall x P(x)}{ \fitch{3.\, \neg P(a)}{ 4. P(a) \qquad\text{$\forall \mathbf{E}$ 2}\\ 5. \bot \qquad \neg\mathbf{E}\,3,4 }\\ 6.\,\bot \qquad \exists \mathbf{E}\,1, 3-5 }\\ \neg \forall xP(x) } $