How to prove these using natural deduction I'd like to prove the following logical equivalence by using natural deduction:
$$(\exists x)(p(x) \implies q) \dashv\vdash (\forall x)(p(x)) \implies q.$$
As far as I'm concerned to show that two statements are equivalent we should show proofs for both of the sides. Can anyone help. Thanks in advance
 A: For the first direction, $(\exists x)(p(x)\implies q) \vdash (\forall x)(p(x))\implies q$, we could reason as follows (in a natural deduction system):


*

*$(\exists x)(p(x)\implies q)\quad {\sf P}\quad$ 1

*$p(a)\implies q \quad {\sf EI(1)}\quad$ 1

*$(\forall x)(p(x))\quad{\sf P}\quad$ 3

*$p(a)\quad {\sf UI(3)}\quad$ 3

*$q \quad {\sf MP(2,4)}\quad$ 1,3

*$(\forall x)(p(x))\implies q\quad {\sf CondI(3,5)}\quad$ 1


For the converse (which you state to have proven already -- this is just for completeness' sake), we could do:


*

*$(\forall x)(p(x)) \lor \neg (\forall x)(p(x))\quad {\sf LEM}\quad$

*$(\forall x)(p(x)) \implies q\quad{\sf P}\quad$ 2

*$(\forall x)(p(x))\quad{\sf P}\quad$ 3

*$q\quad\sf MP(2,3)\quad$ 2,3

*$p(a)\quad\sf P\quad$ 5

*$p(a)\implies q\quad\sf CondI(5,4)\quad$ 2,3

*$(\exists x)(p(x)\implies q)\quad\sf EG(6)\quad$ 2,3

*$(\forall x)(p(x)) \implies (\exists x)(p(x)\implies q)\quad \sf CondI(3,7)\quad$ 2

*$\neg(\forall x)(p(x))\quad\sf P\quad$ 9

*$(\exists x)(\neg p(x))\quad\sf TI(9)\quad$ 9

*$\neg p(a)\quad\sf EI(10)\quad$ 9

*$p(a)\quad\sf P\quad$ 12

*$\bot\quad\sf BI(11,12)\quad$ 9,12

*$q\quad\sf BE(13)\quad$ 9,12

*$p(a)\implies q\quad\sf CondI(12,14)\quad$ 9

*$(\exists x)(p(x)\implies q)\quad\sf EG(15)\quad$ 9

*$\neg(\forall x)(p(x))\implies (\exists x)(p(x)\implies q)\quad\sf CondI(9,16)$

*$(\exists x)(p(x)\implies q)\quad \sf DisjE(1,8,17)\quad$ 2


Where at line 10, the (somewhat tedious to prove) equivalence between $\neg(\forall x)(p(x))$ and $(\exists x)(\neg p(x))$ was used to keep the proof reasonably short.
The abbreviations used for the respective rules should be easily readable to anyone familiar with natural deduction. If someone would appreciate them being explained explicitly, please let me know in the comments.
The lines in above derivations follow the scheme:

Line number. Formula$\quad$Rule$\quad$Undischarged premises


Added: It is worthwhile to note that the invocation of the Law of Excluded Middle is used essentially in the second proof. The two propositions are inequivalent in intuitionistic logic (the logic which accepts everything from classical logic except LEM (and its sister DNE, $\neg\neg p \vdash p$)).
We also have proven the drinker paradox as a special case (with $q = (\forall x)(p(x))$). It's fun to read about.
A: Here is a similar proof using a Fitch-style proof checker:

On line 9, rather than taking the negation of the goal, I tool the negation of the material implication equivalence of the goal.  It was (perhaps) easier to reach a contradiction using that technique. Regardless, from that result on line 14, I still had to derive the desired goal.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
