# Equivalence in Natural deduction in First-order logic 2

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.

Solve the following with natural deduction.

$\vdash \exists x\neg P(x) \iff \neg \forall xP(x)$

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.stack.imgur.com/woKow.jpg

$B \vdash A$: https://i.stack.imgur.com/mYVEU.jpg

Thank you!

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.
• How come you can do $P(x)$ to $\forall xP(x)$ with the same x? I thought the rule was that you had to use a free variable for $\forall$ introduction? Aug 23, 2018 at 10:38
• @FredrikAndersson - The rule $\forall_i$ claims that if $\varphi(x)$ is derivable then $\forall x \, \varphi(x)$ is derivable, on the proviso that the variable $x$ does not occur free in any undischarged hypothesis (see for instance here, p. 32; or Van Dalen, Logic and Structure, 5th ed., 2012, p. 86). The idea is that if you can prove $\varphi(x)$ without any specific assumption on $x$, then $\varphi(x)$ holds for every $x$. Aug 23, 2018 at 13:36