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?– LogikalOct 24, 2017 at 18:28
-
We can't use Ana Con, FO Con, or Taut Con if that's what you mean.– Livia SeilerOct 24, 2017 at 18:40
-
What rules do yoy have? Do you have material implication as a rule?– LogikalOct 24, 2017 at 18:48
Add a comment
|
3 Answers
{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? Oct 24, 2017 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.– user3017Oct 24, 2017 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/
answered Aug 14, 2018 at 4:12
