I would want to check with you guys if I've done the following natural deduction correct. The reason being that I haven't gotten any answer sheet for this task.
Task
Solve the following with natural deduction.
$\vdash \exists x\neg P(x) \iff \neg \forall xP(x)$
Answer
As earlier posted similar tasks for this to be correct I have to prove $A \vdash B$ and $B \vdash A$, where $A = \exists x \, \lnot P(x)$ and $B = \lnot \forall x \, P(x)$.
$A \vdash B$: https://i.sstatic.net/woKow.jpg
$B \vdash A$: https://i.sstatic.net/mYVEU.jpg
Thank you!
Best Answer
Your proof of $\exists x \, \lnot P(x) \vdash \lnot \forall x \, P(x)$ is perfect. However, your attempt for proving $\lnot \forall x \, P(x) \vdash \exists x \, \lnot P(x)$ is wrong, the rule $\forall_i$ on the top is not correctly instantiated because it does not respect the proviso about free variables: indeed, when you apply the rule $\forall_i$, $u$ is a free variable of an undischarged hypothesis, which is not allowed as explained here. (Note that this proviso is crucial to get only correct derivations, otherwise you could prove $\exists x \, P(x) \vdash \forall x \, P(x)$, which is not correct).
A correct derivation of $\lnot \forall x \, P(x) \vdash \exists x \, \lnot P(x)$ in natural deduction is the following:
$$ \dfrac{\dfrac{\lnot \forall x \, P(x) \qquad \dfrac{\dfrac{\dfrac{[\lnot \exists x \, \lnot P(x)]^* \qquad \dfrac{[\lnot P(x)]^{**}}{\exists x \, \lnot P(x)}\exists_i}{\bot}\lnot_e}{P(x)}RAA^{**}}{\forall x \, P(x)}\forall_i}{\bot}\lnot_e} {\exists x \, \lnot P(x)}RAA^* $$
Note that in this derivation the rule $\forall_i$ is correctly instantiated, since $x$ is not free in the (undischarged) hypothesis.
There is also a derivation using only one instance of the rule RAA, but it is longer and awkward, not really interesting.