# Language Logic and Proof Q. 6.26

Using the natural deduction rules, give a formal proof of
A ∨ D
from the premises
1. A ∨ (B ∧ C)
2. (¬ B ∨ ¬ C) ∨ D

Now my approach is to prove that when ¬A then (B ∧ C). Then I want to prove that ¬(B ∧ C) = (¬ B ∨ ¬ C) and then through disjunction introduction A ∨ (B ∧ C) ∨ D. Which then through disjunction elimination get to A ∨ D

But I am getting nowhere with this approach. Can somebody point me in the right direction here

¬(B ∧ C) = (¬ B ∨ ¬ C) is DeMorgan's Law.

``````1. A ∨ (B ∧ C)         Premise
2. (¬ B ∨ ¬ C) ∨ D     Premise
3. | ¬A                Assumption
4. | (B ∧ C)           DS 3,1
5. | ¬¬(B ∧ C)         DN 4
6. | ¬(¬ B ∨ ¬ C)      DeM 5
7. | D                 DS 2,6
8. ¬A -> D             Proof 3-6
9. ¬¬A v D             Mat. Imp 8
10. A v D              DN 9
``````

Without DeMorgan's,

``````1. A ∨ (B ∧ C)         Premise
2. (¬ B ∨ ¬ C) ∨ D     Premise
3. | ¬A                Assumption
4. | (B ∧ C)           DS 3,1
5. | |  ¬ B ∨ ¬ C      Assumption
6. | |  B              CE 4
7. | |  ¬¬B            DN 6
8. | |  ¬ C            DS 5,7
9. | | C               CE 4
10.| ¬(¬ B ∨ ¬ C)      Proof by contradiction 5-9
11.| D                 DS 2,10
12. ¬A -> D            Proof 3-11
13. ¬¬A v D            Mat. Imp 12
14. A v D              DN 13
``````

I'm not super-familiar with Fitch, which apparently requires two proofs by assumption and a v to do vE. but DS and vE are not identical. But in any case, we can do without both:

``````1. A ∨ (B ∧ C)         Premise
2. (¬ B ∨ ¬ C) ∨ D     Premise
3. | ¬A                Assumption
4. | | (B ∧ C)         Assumption
5. | | (B ∧ C)         R
----
6. | | A               Assumption
7. | | A ∧ ¬A          ∧I 3,6
8. | | [Contra. Intr.] 7
9. | | (B ∧ C)         Contra Elim 8
10.| (B ∧ C)           vE 1,9,5
11.| |  ¬ B ∨ ¬ C      Assumption
12.| | | ¬ B           Assumption
13.| | | B              CE 10
14.| | | B ∧ ¬ B       ∧ Introduction
15.| | | D       Contradiction Elimination 14
------------------
15.| | | ¬ C             Assumption
16.| | | C               CE 10
17.| | | C  ∧ ¬ C      ∧ Introduction
18.| | | D       Contradiction Elimination 17
19.| | D            vE 11,15,18
--------------------
20.| | D               Assumption
21.| | D               Repetition
22.| D                 vE 2,19,21
23. ¬ A -> D            Proof 3-22
24. ¬¬ A v D             Material Implication 23
25. A v D                DN 24
``````

And that's closer but looking at Fitch, you may not have access to material implication.

• you beat me to it. – shane Sep 3 '14 at 11:59
• My problem is that Fitch for some reason does not allow step 4. I used disjunction elim 3, 1 – Leon Sep 3 '14 at 12:17
• @Leon I've never used Fitch so I can't say, but vE / DS is valid in normal sentential logic and one of the most basic forms. I guess if it doesn't have that, then change it to an implication first, through material implication. – virmaior Sep 3 '14 at 13:22
• @Leon did it without DS. Still using material implication. – virmaior Sep 3 '14 at 15:19
• Disjunctive Syll : ¬B ∨ C, B ⊢ C is easily derived in Natural Deduction with ∨-E : C ⊢ C and ¬B, B ⊢ ⊥ ⊢ C. Thus, from C ⊢ C and ¬B, B ⊢ C, we conclude by ∨-E with : ¬B ∨ C, B ⊢ C. – Mauro ALLEGRANZA Sep 3 '14 at 15:40

This will be very similar to the above poster, but I will share it too. Corrections are welcome:

1. A v (B ^ C)
2. (~B v ~C) v D / A v D
3. ~(B ^ C) v D 2, De M.
4. (B ^ C) > D 3, Impl.
5. ~A > (B ^ C) 1, Impl.
6. ~A > D 4, 5, H.S.
7. A v D 6, Impl.