2

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}     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
1

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

0

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

enter image description here

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/

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.