I have a question on how to prove $$(\neg \forall x \, P(x)) \rightarrow (\exists x \, \neg P(x)) $$ with a natural deduction proof, where $P$ is a predicate.
I especially have problems with what to do about the negation in front of $\forall$.
In general, how should I go about the problem if I have a negation in front of the formula, especially if that is an assumption? I am asking this in the context of a natural deduction proof, like the one above (or eg. $\neg \exists ..., etc.$)
On
Here are some propositions and theire negation $$\exists x P(x) \;\;,\;\; \forall x \lnot P(x)$$
$$\forall x \exists y :P(x,y)\;\;;\;\; \exists x\forall y \lnot P(x,y)$$
$$P \vee Q \;\;,\;\; \lnot P \wedge \lnot Q$$
$$P \wedge Q \;\;,\;\; \lnot P \vee \lnot Q$$
$$P\implies Q \;\;,\;\; P \wedge \lnot Q$$
$$a>b \;\;,\;\; a\le b$$
$ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\} \def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\} \def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\} \def\R#1{\qquad\mathbf{R} \: #1 \\} \def\ci#1{\qquad\mathbf{\land I} \: #1 \\} \def\ce#1{\qquad\mathbf{\land E} \: #1 \\} \def\oi#1{\qquad\mathbf{\lor I} \: #1 \\} \def\oe#1{\qquad\mathbf{\lor E} \: #1 \\} \def\ii#1{\qquad\mathbf{\to I} \: #1 \\} \def\ie#1{\qquad\mathbf{\to E} \: #1 \\} \def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\} \def\bi#1{\qquad\mathbf{\leftrightarrow I} \: #1 \\} \def\qi#1{\qquad\mathbf{=I}\\} \def\qe#1{\qquad\mathbf{=E} \: #1 \\} \def\ne#1{\qquad\mathbf{\neg E} \: #1 \\} \def\ni#1{\qquad\mathbf{\neg I} \: #1 \\} \def\IP#1{\qquad\mathbf{IP} \: #1 \\} \def\x#1{\qquad\mathbf{X} \: #1 \\} \def\DNE#1{\qquad\mathbf{DNE} \: #1 \\} $ You don't specify what set of rules are you using but I will assume the ones found in forallx: Calgary book.
We want to prove a sentence without premises. The first thing would be to ask what is the main logical connective. In this case, an implication. So, Implication Introduction rule has the following schema:
$ \fitch{}{ \fitch{i.\mathcal A}{ j. \mathcal B }\\ \mathcal{A \to B} \qquad\mathbf{\to I}\,i-j } $
In our case,
$ \fitch{}{ \fitch{\lnot \forall xP(x)}{ \vdots\\ \exists x \lnot P(x) }\\ \lnot \forall x P(x) \to \exists x \lnot P(x) \ii{} } $
We could try assuming $P(a)$ and attempting to use Universal Introduction rule...
$ \fitch{}{ \fitch{1.\,\lnot \forall xP(x)}{ \fitch{2.\lnot P(a)}{ 3. \forall xP(x)\\ \bot\\ }\\ \exists x \lnot P(x) }\\ \lnot \forall x P(x) \to \exists x \lnot P(x) } $
but we immediately see that its application is forbidden because name a already occurs in an undischarged assumption (line 2).
An indirect approach seems reasonable. If we intend to use IP (Indirect Proof) rule to derive $\exists x\lnot P(x)$, assuming $\lnot \exists x\lnot P(x)$ and reaching $\bot$, would allow the application of that rule.
Full proof:
$ \fitch{}{ \fitch{1.\,\lnot \forall xP(x)}{ \fitch{2.\,\lnot \exists x \lnot P(x)}{ \fitch{3.\,\lnot P(a)}{ 4.\,\exists x \lnot P(a) \Ei{3} 5.\,\bot \ne{2,4} }\\ 6.\,P(a) \IP{3-5} 7.\,\forall xP(x) \Ai{6} 8.\,\bot \ne{1,7} }\\ 9.\,\exists x \lnot P(x) \IP{2-8} }\\ 10.\,\lnot \forall x P(x) \to \exists x \lnot P(x) \ii{1-9} } $