I did it with using truth tables but I am inquisitive about how to proof the distributive property without using truth tables (i.e using the other rules of replacement or inference).

$$ (P \land (Q \lor R)) \Leftrightarrow ((P \land Q) \lor (P \land R))$$


$$ (P \lor (Q \land R)) \Leftrightarrow ((P \lor Q) \land (P \lor R)) $$


Here's a hint how you might start constructing a proof of the first biconditional in a standard natural deduction system.

You need to prove the two halves of the conditional separately. So, to go left to right, assume the antecedent $(P \land (Q \lor R))$ and aim for the consequent $(P \land (Q \lor R)) \to ((P \land Q) \lor (P \land R))$. Plainly you need to extract the two conjuncts $P$ and $(Q \lor R)$ from your assumption. And now obviously the only way forward is to use $\lor$-elimination.

So you now need to fill in the following schematic proof:

$\quad|\quad(P \land (Q \lor R)) \quad\quad\text{assumption}\\ \quad|\quad P \\ \quad|\quad(Q \lor R))\\ \quad|\quad|\quad Q \quad\quad\quad\quad\quad\text{ assumption}\\ \quad|\quad|\quad ...\\ \quad|\quad|\quad ((P \land Q) \lor (P \land R))\\ \quad|\quad|\quad --\\ \quad|\quad|\quad R\quad\quad\quad\quad\quad\text{ assumption}\\ \quad|\quad|\quad ...\\ \quad|\quad|\quad ((P \land Q) \lor (P \land R))\\ \quad|\quad ((P \land Q) \lor (P \land R))\quad\text{ by or-elimination, discharging assumptions}\ Q,\ R\\ \quad (P \land (Q \lor R)) \to ((P \land Q) \lor (P \land R)) \quad\text{by conditional proof}\\ $

Do you see understand this sort of proof strategy? Do you see how to fill in the gaps??

If you do, then you'll easily be able to produce similar proofs for the reverse conditional, and likewise for the two halves of your other biconditional.

If you don't, then have a look e.g. at Paul Teller's Formal Logic Primer, freely available online.

  • $\begingroup$ I can understand $P$ and $(Q \lor R) $ via [simplification](en.wikipedia.org/wiki/Simplification_logic) on $(P \land (Q \lor R))$. However I am not sure how $Q$ is followed?! $\endgroup$
    – Quixotic
    Oct 27 '12 at 18:09
  • 1
    $\begingroup$ It doesn't follow. it is a new supposition. Check out how or-elimination works in ND. $\endgroup$ Oct 27 '12 at 18:28

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.