[Math] Nat Deduction Proof – Distributive property

logicnatural-deductionproof-verificationpropositional-calculus

I need to prove (P v Q) ^ (P v R) |- P v (Q ^ R) using natural deduction and propositional logic. I should be able to do it using only AND and OR rules, but I am stuck on how to assume Q and R. This is what I have:

(P v Q) ^ (P v R)________premise

P v Q________________^e1___1

P v R________________^e2___1

…P__________________assumption

…P v (Q ^ R)___________vi1___4

I know this is right so far. I just don't know how to introduce my assumptions for Q and R. Do I assume ~P? If so, which rule is applied, and what is the process, to conclude Q ^ R? Thanks for any help you can give me

Best Answer

It's easier to show $\wedge$ distributes over $\vee$ than vice-versa. And the latter follows straightforwardly from the former. So you might first try showing $(Q \vee R) \wedge P \vdash (Q \wedge P) \vee (R \wedge P)$, and use those arguments or the fact itself in the needed proof. To show $\wedge$ distributes over $\vee$, make use of $P \wedge Q \vdash R$ if and only if $P \vdash Q \rightarrow R$. (This shows that $ \_ \wedge Q$ is a left adjoint of $Q \rightarrow \_$, and left adjoints preserve joins. For "and" to distribute over "or" means the same thing as the "and" operator to preserve binary disjunction, a join.) In formal deduction of $(Q \vee R) \wedge P \vdash (Q \wedge P) \vee (R \wedge P)$, you can use the inference law I mentioned to isolate $Q \vee R$ to the left of $\vdash$ and deal with $Q$ and $R$ separately. Even if you want to show the needed result directly, the idea is that whenever you need to show an inference with a hypothesis that is a conjunction where one conjunct is a disjunction, use the inference law I mentioned to create an equivalent inference with hypothesis the disjunction, which inference can be broken up into simpler inferences each involving as hypothesis a disjunct, and each of these inferences can be dealt with by using the reverse direction of the inference law to remove the implication that was created.