# Natural deduction proof: {A → B, B → (C & D), ¬C v ¬D} ⊢ ¬A

Prove using natural deduction: $${A → B, B → (C \land D), ¬C \vee ¬D} ⊢ ¬A$$

Our work (so far):

$$1- A → B$$

$$2- B → (C \land D)$$

$$3- ¬¬A$$

$$4- A$$

$$5- B$$ (from 1,4) $$→E$$

$$6- B$$

$$7- C \land D$$ (from 2,6) $$→E$$

This is where I've been for the past 6 hours. Help me out if you can. Thanks.

• Now use $\lor$-$\text{Elim}$ on $\neg C\lor \neg D$. Find a contradiction in each case to infer a contradiction in the outermost level inside the $A$ assumption. – Git Gud May 21 '15 at 21:34
• can you give me more explanation – user155971 May 21 '15 at 21:37

Get the contra-positives of 1&2 as $\neg B\rightarrow \neg A$ and $\neg C \,\,V\neg D \rightarrow \neg B$. Use $\neg C \,\,V\neg D \rightarrow \neg B, \,\,\,\, \neg B \rightarrow \neg A$ and the result follows.

This proof expands on Git Gud's comment, "Now use ∨-Elim on ¬C∨¬D. Find a contradiction in each case to infer a contradiction in the outermost level inside the A assumption", since the OP asked for "more explanation".

The contra-positive approach that OKPALA MMADUABUCHI offered would also work although it would not with the proof checker I am using for my answer since that rule is not an option provided with the proof checker.

The problem with the OP's approach to the problem is the third premise seems to have been missed. It should have been line 3. Also one could approach the negation of $$¬A$$ as either $$¬¬A$$ or $$A$$. In the first case one would use an indirect proof; in the second, negation introduction. For my proof I used $$A$$ on line 4. Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/