# Natural deduction proof: $A \vee (B \wedge C) ├ (A \vee B) \wedge (A \vee C)$

I assume that I need to set a hypothesis somewhere in the process, but I don't know how.

1   A V (B Ʌ C)     Premiss
2   B Ʌ C           1 (VE)
3   B               2 (ɅE)
4   C               2 (ɅE)
5   A V B           3 (VI)


The above is the formulas that I have written so far, but I'm clearly stuck and not sure where / how to continue. (I also doubt if line 5 ($$A \vee B$$) is the right one)

How should I tackle this problem?

1. You got the $$\lor E$$ rule wrong. From $$A \lor (B \land C)$$ you can not directly infer $$A$$ and $$(B \land C)$$ - that would be $$\land E$$. Instead, you need to open two subproofs where you assume $$A$$ and $$B \land C$$ respectively, then when both subproofs yield the same conclusion $$(A \lor B) \land (A \lor C)$$, this will be the conclusion of $$\lor E$$, where the assumptions $$A$$ and $$B \land C$$ can be discarded. The idea is "If we know that either $$A$$ or $$B \land C$$ hold, and from both scenarios proposition $$(A \lor B) \land (A \lor C)$$ would follow, then we can conclude $$(A \lor B) \land (A \lor C)$$."
2. To continue the proof, you proceed in the same way for $$C$$ as you did for $$B$$.

Full proof:

• Thanks for pointing out my errors. I had the idea correct, but as I stated in my response the formalism was not correct. I don't know the field enough to state my response as clearly as you have. Nice job. – JacobCheverie Apr 24 at 13:16
• Thank you for the explanation! – Shinichi Takagi Apr 24 at 18:56

Apparently you wanted to eliminate A from A v ( B&C) , but you can do this only if you first have ~A. Since ~ A is not given as premise, the best way is to introduce ~A as hypothesis, and then to use the disjunctive syllogism rule inside a conditional proof.

Here by " disjunctive syllogism" I mean the rule

" from X v Y and ~X, infer : Y "

• This is not a properly layed out syntactic proof according to the rules of natural deduction. – lemontree Apr 24 at 13:14
• @lemontree. Do you mean that I did not correctly use the conditional proof rule or that conditional proof is not an available proof in natural deduction. ( I thought that the mathod taught in logic manuals like The Logic Book or Teller's Modern Logic was called " natural deduction") – Eleonore Saint James Apr 24 at 13:28
• With your edit the proof looks fine formally. However, I doubt most natural deduction systems would accept disjunctive syllogism, the replacement rule for $\to$ and double negation elemination in a subformula as primitive rules. – lemontree Apr 24 at 14:09

$$\frac{\frac{A\vdash A\lor B \; \; A\vdash A\lor C}{A\vdash (A\lor B)\land (A\lor C)} \;\;\frac{\frac{B\land C\vdash B \;\; B\vdash A\lor B}{B\land C\vdash A\lor B} \frac{B\land C\vdash C \;\; C\vdash A\lor C}{B\land C\vdash A\lor C}}{B\land C\vdash (A\lor B)\land (A\lor C)}}{A\lor(B\land C)\vdash (A\lor B)\land (A\lor C)}$$

This is a proof using sequent calculus, which may not be what you're looking for; but all proof systems at this level are essentially the same, and so if you can identify the rules that I'm using, and relate them to the rules of the system you want to use, then it can help you nonetheless

• You should be mentioning that this is a natural-deduction style proof in the sequent calculus. I assume OP is more intrested in a (Fitch-style) natural deduction proof. – lemontree Apr 24 at 14:07
• @lemontree yes, I thought initially that it would look "cooler" to just throw the deduction tree like this but I'll add context – Max Apr 24 at 14:08
• There's also tree-style natural deduction without sequents, which can be more or less directly translated to Fitch style. So if you'd like to present an alternative using trees, there is no actual need to switch to sequents. – lemontree Apr 24 at 14:10
1   A V (B Ʌ C)     Premiss
2   B Ʌ C           1 (VE)
3   B               2 (ɅE)
4   C               2 (ɅE)
5   A V B           3 (VI)
6   A V C           4 (VI)
7   (A V B) Ʌ (A V C)  5,6
8   A               1 (VE)
9   A V B           8 (VI)
10  A V C           8 (VI)
11  (A V B) Ʌ (A V C)  9,10


I'm not correct on the formalism but you were just about there.

• Your use of the $\lor E$ rule is incorrect. $A$ and $B \land C$ are not conclusions obtained from $\lor E$, but assumptions in new subproofs, each of which end in $(A \lor B) \land (A \lor C)$ (your lines 7 and 11). The final step is then an application of $\lor E$ on lines 1, 7, 11 to derive the conclusion formula $(A \lor B) \land (A \lor C)$ on the outermost level. – lemontree Apr 24 at 13:13