How to prove (PvQ) & (RvS) : ((P&R) v (P&S)) v ((Q&R) v (Q&S)) by Natural deduction

Question

Another of Tomassi's exercises I can't solve (Logic, page 109, Revision exercise III, 3)

(P v Q) & (R v S) : ((P & R) v (P & S)) v ((Q & R) v (Q & S))

I have to use natural deduction and the only rules I know are:

• assumptions,

• modus ponendo ponens,

• modus tollendo tollens,

• double negation,

• reductio ad absurdum,

• conditional proof,

• v-introduction,

• v-elimination,

• and introduction,

• and elimination.

Tomassi's proof consists of 15 steps.

My answer so far is:

{1} 1. (P v Q) & (R v S) Premise

{1} 2. (P v Q) 1 &E

{1} 3. (R v S) 1 &E

{4} 4. P Assumption for vE

{5} 5. R Assumption for vE

{4,5} 6. P & R 4,5 &I

{4,5} 7. (P & R) v (P & S) 6 vI

{4,5} 8. ((P & R) v (P & S)) v ((Q & R) v (Q & S))

{9} 9. Q Assumption for vE

{10} 10. S Assumption for vE

{9,10} 11. Q & S 9,10 &I

{9,10} 12. ((Q & R) v (Q & S)) 11 vI

{9,10} 13. ((P & R) v (P & S)) v ((Q & R) v (Q & S)) 13 vI

{1,4,9} 14. ((P & R) v (P & S)) v ((Q & R) v (Q & S)) 3,5,8, 10, 13 vE for second conjunct (discharging 5 and 10)

{1,4,5} 15. ((P & R) v (P & S)) v ((Q & R) v (Q & S)) 2,4,8,9,14 vE for first conjunct

What did I get wrong?

Am I allowed to use the conclusion at 14 for both disjuncts of the first disjunction?

Many thanks for your help.

Answer 1

Here is a way to format the proof so that it might make it easier to see the structure. I basically followed your lead.

The question appears to be this:

Am I allowed to use the conclusion at 14 for both disjuncts of the first disjunction?

For the disjunction P∨Q, I used disjunction elimination on RvS first when considering P and then once again when considering the Q side of the disjunction. It seems like a duplication of effort, but each side of the first disjunction required eliminating the second disjunction in a similar way.

---

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/