# Prove (¬P ∨ Q) ↔ (P → Q)

How can one use a standard logic proof to prove this without using any premises? I've tried doing subproofs and splitting up ¬P and Q to try to get to P → Q but I'm very stuck!

• Do you have inference rules to use? – Logikal Oct 24 '17 at 18:28
• We can't use Ana Con, FO Con, or Taut Con if that's what you mean. – Livia Seiler Oct 24 '17 at 18:40
• What rules do yoy have? Do you have material implication as a rule? – Logikal Oct 24 '17 at 18:48

```{1}     1.  ~P ∨ Q                         Assum.
{2}     2.  ~P                             Assum. (1 1st Disj.)
{3}     3.  P                              Assum.
{4}     4.  ~Q                             Assum.
{3,4}   5.  P & ~Q                         3,4 &I
{3,4}   6.  P                              5 &E
{3}     7.  ~Q → P                         4,6 CP
{2,3}   8.  ~~Q                            2,7 MT
{2,3}   9.  Q                              8 DNE
{2}     10. P → Q                          3,9 CP (1 1st Conc.)
{11}    11. Q                              Assum (1 2nd Disj)
{3,11}  12. P & Q                          3,11 &I
{3,11}  13. Q                              12 &E
{11}    14. P → Q                          3 13 CP (1 2nd Conc.)
{1}     15. P → Q                          1,2,10,11,14 ∨E
-       16. (~P ∨ Q) → (P → Q)             1,15 CP
{17}    17. P → Q                          Assum.
{4,17}  18. ~~P                            4,17 MT
{4,17}  19. P                              18 DNE
{4,17}  20. Q                              17,19 MP
{4,17}  21. Q & ~Q                         4,20 &I
{17}    22. ~~Q                            4,21 RAA
{17}    23. Q                              22 DNE
{17}    24. ~P ∨ Q                         23 ∨I
-       25. (P → Q) → (~P ∨ Q)             17,25 CP
-       26. (~P ∨ Q) ↔ (P → Q)             16,25 ↔I
```
• Thank you so much for this, it's been very helpful, although I'm a little confused as to where your subproofs start and end, could you please indicate this? – Livia Seiler Oct 24 '17 at 19:57
• The main subproofs are lines 1-16 and lines 17-25. There are also subproofs for each half of the disjunction of line 1: lines 2-10 and lines 11-14. Something else to notice is that I reused my assumption (~Q) from line 4 to invoke modus tollens on line 18. This assumption leads to a contradiction on line 21 so that I can conclude Q on line 23. Hope that helps. – user3017 Oct 24 '17 at 20:41

Prove ~P ˅ Q entails P → Q, by assuming P and demonstrating that eliminating the disjunction will derive Q by means of explosion (P,~P ├ Q) and reiteration (P, Q ├ Q).

Prove the converse, that P → Q entails ~P ˅ Q, either by (1) excluding the middle and introducing an appropriate disjunctive in each case, or (2) reducing to absurdity (assume ~(~P ˅ Q) and derive a contradiction).

Here is one approach to proving "(¬P ∨ Q) ↔ (P → Q)" without using any premises.

Lines 1 to 8 show "(¬P ∨ Q) → (P → Q)" and lines 9 to 15 show "(P → Q) → (¬P ∨ Q)".

I used the following rules: negation introduction (¬I), explosion (X), disjunction elimination (vE), conditional introduction (→I), conditional elimination (→E), law of excluded middle (LEM) and biconditional introduction (↔I). Explanations of these may be found in forall x: Calgary Remix.

References

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

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/