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

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?

-
What does $???$ mean ? – Amr Apr 14 '14 at 5:25
@Amr well... I just don't know what to put down as a reason. – user3109672 Apr 14 '14 at 5: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 5:27
@Amr I'm not sure. Propositional logic, perhaps? Here's a list of rules I'm given: maths.usyd.edu.au/u/UG/SM/MATH3066/r/DeductionRules.pdf – user3109672 Apr 14 '14 at 5:28

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

-

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

-