2
$\begingroup$

I have to prove the following logical equivalence, also known as one of the two distributive laws:

$$ P \vee (Q \wedge R) \equiv (P \vee Q) \wedge (P \vee R) $$

I have solved the first part, $P \lor (Q \land R) \to (P \lor Q) \land (P \lor R)$, like so:

enter image description here

But now that I'm trying to solve the next part, $(P \lor Q) \land (P \lor R) \rightarrow P \lor (Q \land R)$, I keep getting stuck somewhere with a disjunction elimination where I'm trying to prove something like $P$ with only $Q$ and $(P ∨ Q) ∧ (P ∨ R)$.

So how can I prove $(P \lor Q) \land (P \lor R) \rightarrow P \lor (Q \land R)$ using a proof tree, like shown above? Thanks!

$\endgroup$
2
  • $\begingroup$ Unpack the premise with $\land$-elim; then two "nested" $\lor$-elim. Three cases : 1) $P$ : done. 2) $Q$ then $P$ : done. 3) $Q$ then $R$ : done. $\endgroup$ – Mauro ALLEGRANZA Sep 7 '18 at 20:11
  • $\begingroup$ @MauroALLEGRANZA Thank you for commenting, but I'm not sure I understand. After I've used implication introduction on the premise ($P∨(Q∧R)$), wouldn't I have to use disjunction elimination before being able to do a conjunction elimination as you suggest? $\endgroup$ – tobloef Sep 7 '18 at 20:43
2
$\begingroup$

Let $A = (P \lor Q) \land (P \lor R)$ and $B = P \lor (Q \land R)$.

The following is a derivation in natural deduction of $B$ from $A$.

$$ \dfrac{\dfrac{A}{P \lor Q}\land_{e_1} \quad \dfrac{[P]^*}{B}\lor_{i_1} \quad \dfrac{\dfrac{A}{P \lor R}\land_{e_2} \quad \dfrac{[P]^{**}}{B}\lor_{i_1} \quad \dfrac{\dfrac{[Q]^* \quad [R]^{**}}{Q \land R}\land_i}{B}\lor_{i_2}}{B}\lor_e^{**}}{B} \lor_e^* $$

Note that the derivation above is based on two nested applications of the rule $\lor_e$.

From the derivation above you obtain the derivation of $A \to B$ (without assumptions) by adding a $\to_i$ rule as last rule, discharging the two occurrences of $A$.

$\endgroup$
1
  • $\begingroup$ Thank you so much. Re-writing your answer in the same style as my previous example results in this final proof tree. $\endgroup$ – tobloef Sep 7 '18 at 23:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.