First-order logic equivalence proof 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.$)
 A: $
\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}
}
$
A: 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$$
