[Math] How to prove these using natural deduction

discrete mathematicslogicpropositional-calculus

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

Best Answer

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):

  1. $(\exists x)(p(x)\implies q)\quad {\sf P}\quad$ 1
  2. $p(a)\implies q \quad {\sf EI(1)}\quad$ 1
  3. $(\forall x)(p(x))\quad{\sf P}\quad$ 3
  4. $p(a)\quad {\sf UI(3)}\quad$ 3
  5. $q \quad {\sf MP(2,4)}\quad$ 1,3
  6. $(\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:

  1. $(\forall x)(p(x)) \lor \neg (\forall x)(p(x))\quad {\sf LEM}\quad$
  2. $(\forall x)(p(x)) \implies q\quad{\sf P}\quad$ 2
  3. $(\forall x)(p(x))\quad{\sf P}\quad$ 3
  4. $q\quad\sf MP(2,3)\quad$ 2,3
  5. $p(a)\quad\sf P\quad$ 5
  6. $p(a)\implies q\quad\sf CondI(5,4)\quad$ 2,3
  7. $(\exists x)(p(x)\implies q)\quad\sf EG(6)\quad$ 2,3
  8. $(\forall x)(p(x)) \implies (\exists x)(p(x)\implies q)\quad \sf CondI(3,7)\quad$ 2
  9. $\neg(\forall x)(p(x))\quad\sf P\quad$ 9
  10. $(\exists x)(\neg p(x))\quad\sf TI(9)\quad$ 9
  11. $\neg p(a)\quad\sf EI(10)\quad$ 9
  12. $p(a)\quad\sf P\quad$ 12
  13. $\bot\quad\sf BI(11,12)\quad$ 9,12
  14. $q\quad\sf BE(13)\quad$ 9,12
  15. $p(a)\implies q\quad\sf CondI(12,14)\quad$ 9
  16. $(\exists x)(p(x)\implies q)\quad\sf EG(15)\quad$ 9
  17. $\neg(\forall x)(p(x))\implies (\exists x)(p(x)\implies q)\quad\sf CondI(9,16)$
  18. $(\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.

Related Question