# Classical logic derivation question

Premise 1: R∨T

Premise 2: ∼P↔(∼P→Q)

Prove: (R∨S)∨(T∧Q), using only R, DN, MP, MT, S, ADJ, MTP, ADD, BC, CB, CDJ, DM.

Here's what I got so far:

1. Show (R∨S)∨(T∧Q)
1. R∨T______________________________________PR1

2. ∼P↔(∼P→Q)______________________________PR2

3. ∼P→(∼P→Q)______________________________3 BC

4. (∼P→Q)→∼P______________________________3 BC

1. Show ~P→Q
1. ~P_____________________________ASS CD

2. ∼P→Q_________________________4 7 MP

3. Q______________________________7 8 MP

4. _______________________________9 CD

1. ~P_______________________________________5 6 MP

2. Q________________________________________6 11 MP

Now, I'm not sure how to find the answer. I'm pretty sure that I have to either prove R or T by indirect derivation, but I can't seem to find a way to have a contradiction. Is there another way?

If you are allowed to divide an "OR" into two hypotheticals (discharged by showing the same result for both) this is easy at this point. On the left, you assume R, and then you can build R V S and (R V S) V (T & Q) both by OR introduction. On the right, assume T, and you already have Q, so you are good to go there as well.

If you don't have access that rule, your best bet is to assume the opposite of your conclusion, ~ [(R V S) V (T & Q)]

From there, yield ~(R V S) & ~(T & Q) Assume T Then you have T & Q which contradicts ~(T & Q). Discharge your assumption and yield T. From there you can build the entire statement that directly contradicts your assumption.

• I've already shown that ~P and Q is true for the main show line. I need to show P or ~Q, but your method does not provide a contradiction. Not sure how you can show P when ~Q would not be reproducible.
– YSR
Oct 23, 2015 at 14:32
• Sorry, I didn't really check your original work very carefully and provided an entirely different method of getting to the conclusion. I've edited to provide one that picks up where you left off. Oct 23, 2015 at 16:02

ASS ID: Assume Indirect Derivation PR: Premise BC: Biconditional-Conditional ASS CD: Assume Conditional Derivation MP: Modes Ponens DM: De Morgan's law ADJ: Adjunction S: Simplification MTP: Modus Tollendo Ponens ADD: Addition

I skip the use of Latex for practical reasons and the so called formal methods. Use the equivalence of A and B is the same as 'A and B' or 'not A and not B'. Apply it and you will find Q. Then Given R or T. Assume R, then by weakening 'R, thus R or S'. Assume T as the other possibility, then T and Q. Hence two possibilites are left: R or S, or, T and Q. Now it is possible to formalize it, to my opinion.

• This is very hard to follow, unless you already understand the problem and how to solve it. The sentence about equivalence is especially confusing, I had to read it several times before I understood your intent. The advantage to the formal methods is they make the mechanics clear. Oct 26, 2015 at 13:18

Here is a proof using disjunction elimination on the first premise.

The case for T may require some explanation. To get Q I first derived the conditional ¬P→Q on lines 7-9. Given that and the biconditional premise, I could derive Q.

Only introduction (I) and elimination (E) rules were used for conjunction (∧), disjunction (∨), conditional (→) and biconditional (↔).

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/