What is the formal proof for distributive law, from the other side of the equation?

Question

How does one prove that

(P ∨ Q) ∧ (P ∨ R) ⊢ P ∨ (Q ∧ R)

Is this a well formed proof?

(P ∨ Q) ∧ (P ∨ R) (premise)
(P ∨ Q)
(P ∨ R)            (and-elimination)
~P-> Q
~P-> R              (???)
~P                  (assumption)
Q
R                   (Modus Ponens)                    
Q ∧ R               (and-introduction)
~P -> (Q ∧ R)       (conditional proof, discarding assumption ~P)
P ∨ (Q ∧ R)         (???)

How are you supposed to do it otherwise?

Thanks

EDIT: The first answer to this question does use this equivalence: Proof of the distributive law in implication?

Is it something that's acceptable in propositional logic?

@Amr well... I just don't know what to put down as a reason. — Einheri, Apr 14 '14 at 05:25
If you don't know the reason for a step in a formal proof then don't that step. What proof system are you using ? — Amr, Apr 14 '14 at 05:27
@Amr I'm not sure. Propositional logic, perhaps? Here's a list of rules I'm given: http://www.maths.usyd.edu.au/u/UG/SM/MATH3066/r/DeductionRules.pdf — Einheri, Apr 14 '14 at 05:28

score 3 · Accepted Answer · answered Apr 14 '14 at 05:52

After you get $P\lor Q, P\lor R$ start a 2 nested proofs by cases ($\lor$-elimination) as follows:

If $P$

$\,\,\,\,\,$then $P\lor (Q \land R)\,\,\,$ ($\lor$-Intro)

If $Q$

$\,\,\,\,\,$If $P$

$\,\,\,\,\,\,\,\,\,\,$then $P\lor (Q\land R)\,\,\,$ ($\lor$-Intro)

$\,\,\,\,\,$If $R$

$\,\,\,\,\,\,\,\,\,\,$then $Q\land R$$\,\,\,(\land-Intro$, because in this subcase of a case we have both $Q,R$ as premises)

$\,\,\,\,\,\,\,\,\,\,$then $P\lor (Q\land R)$ $\,\,\,(\lor-Intro)$

$\,\,\,\,\,$$P\lor (Q\land R)$ $\,\,\,(\lor-Elim$ from the subproofs that start with $Q,R$ and we use the premise $P\lor R$)

$P\lor (Q\land R)$$\,\,\,(\lor-Elim$ from the subproofs that start with $P,Q$ and we use the premise $P\lor Q$)

Doug Spoonwood · Answer 2 · 2014-04-14T06:01:09.147

I use Polish notation.

 1      KApqApr  premise
 2      Apq      1 K-e (conjunction elimination)
 3      Apr      1 K-e
 4 |    NApNp  assumption
 5 ||   p assumption
 6 ||   ApNp  5 A-i 
 7 ||   KApNpNApNp 6, 4 K-i
 8 |    Np 5-7 RAA
 9 |    ApNp 8 A-i
10 |    KApNpNApNp 9, 4 K-i
11      NNApNp  4-10 RAA
12      ApNp    11 DN
13 |    p  assumption
14 |    ApKqr 13 A-i
15 |    Np assumption
16 ||   p assumption
17 |||  Nq assumption
18 |||  KpNp 16, 15 K-i
20 ||   NNq 18-19 RAA
21 ||   q 20 DN
22 ||   q assumption
23 |    q 2, 16-21, 22-22 A-e
24 ||   p assumption
25 |||  Nr assumption
26 |||  KpNp 24, 15 K-i
27 ||   NNr 25-26 RAA
28 ||   r  27 DN
29 ||   r assumption
30 |    r 3, 24-28, 29-29 A-e
31 |    Kqr 23, 30 K-i
32 |    ApKqr 31 A-i
33      ApKqr 12, 13-14, 15-32 A-e

What is the formal proof for distributive law, from the other side of the equation?

2 Answers2