# Prove A ∨ D from A ∨ (B ∧ C) and (¬ B ∨ ¬ C) ∨ D ( LPL Q6.26) without using --> or material implication

This is a repeated question: 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

The LPL textbook has not yet introduced material implication or the implies "-->" symbol and the answer given in the above link does NOT satisfy the question in the book and I was surprised the user accepted the answer as appropriate.

The answer is valid until step 22, since the textbook has not introduced those forms of steps. Is there a way to use this proof and using other rules to show the implication that ~A --> D and A --> ~D therefore A V D ?

How would I go about solving this proof in Fitch without --> or material implication?

Rules you can use:

• V intro, elim (disjunction)

• ^ intro, elim (conjunction)

• ~ intro, elim (negation)

• = intro, elim

|  1) A ∨ (B ∧ C) --- premise
|_ 2) (¬ B ∨ ¬ C) ∨ D --- premise
|  |_ 3) A --- assumed [a] from 1) for ∨-elim
|  |  4) A ∨ D --- from 3) by ∨-intro
|  /
|  |_ 5) (B ∧ C) --- assumed [b] [from 1) for ∨-elim
|  |  |_ 6) D --- assumed [c] from 2) for ∨-elim
|  |  |  7) A ∨ D --- from 6) by ∨-intro
|  |  /
|  |  |_ 8) (¬ B ∨ ¬ C) --- assumed [d] from 2) for ∨-elim
|  |  |  9) B --- from 5) by ∧-elim
|  |  | 10) C --- from 5) by ∧-elim


Now, with a third ∨-elim we derive ⊥ (the contradiction) from both 8), 9) and 8), 10); thus :

|  |  | 11) ⊥ --- from 8) by ∨-elim
|  |  | 12) A ∨ D --- from 11) by ⊥-elim


Having derived A ∨ D from both 6) D and 8) (¬ B ∨ ¬ C), we have :

|  | 13)  A ∨ D --- from 2) by ∨-elim discharging assumptions [c] and [d]


Having derived A ∨ D from both 3) A and 5) (B ∧ C), we have :

| >14)  A ∨ D --- from 1) by ∨-elim discharging assumptions [a] and [b].


Conclusion :

A ∨ (B ∧ C), (¬ B ∨ ¬ C) ∨ D ⊢ A ∨ D --- from 1), 2) and 14).

• I do not understand where the subproofs start and end or how deeply nested they are from this answer, if you look at the original answer from philosophy.stackexchange.com/questions/15651/… and could format it like that, that would be very helpful – Billy Bob Feb 24 '15 at 0:51
• Like, what does " A --- assumed [a] from 1) for ∨-elim" mean, sounds like, Assume A, therefore A because v elim from step 1. This doesn't check out. – Billy Bob Feb 24 '15 at 6:17
• The subproof starts with the assumptions [a] and [b] : needed for ∨-elim from 1), and ends at step 14) with the discharge of the two assumptions. See here for an explanation. – Mauro ALLEGRANZA Feb 24 '15 at 20:22

The proof is going to be a big v-elim on A v (B ^ C). You could just have easily done the v-elim on (~B v ~C) v D, however. I've tried to make the notation match what's in the textbook, though I admit that it is rather atrocious. Might be worthwhile to copy it out by hand just so you can see how the scoping works for the subproofs.

 1. |A v (B ^ C)         Premise
2. |(~B v ~C) v D       Premise
---------------
3. ||A                  Assumption for v-elim
---------------
4. ||A v D              3, v-intro
|
5. ||B ^ C              Assumption
---------------
6. ||B                  5, ^-elim
7. ||C                  6, ^-elim
8. |||D                 Assumtion
---------------
9. |||A v D             8, v-intro
||
10. |||~B v ~C           Assumption
---------------
11. ||||~B               Assumption
---------------
12. ||||| ~D             Assumption (for reductio)
---------------
13. ||||| falsum         falsum-intro, 6, 11
14. ||||~~D              ~-intro, 12 - 13
15. |||| D               ~-elim, 14
16. ||||~C               Assumption
--------------
17. |||||~D              Assumption (for reductio)
--------------
18. ||||| falsum         falsum-intro, 7, 16
19. ||||~~D              ~-intro, 17-18
20. |||| D               ~-elim, 19
21. |||D                 v-elim, 10, 11-15, 16-20
22. |||A v D             v-intro, 21
23. || A v D             v-elim, 2, 8-9, 10-22
24. |A v D               v-elim, 1, 3-4, 5 - 23


This is a similar proof to the one provided by possibleWorld except that it starts with the second premise rather than the first and illustrates it with a different Fitch-style proof checker.

The proof uses disjunction introduction (∨I), conjunction elimination (∧E), contradiction introduction (⊥I), explosion (X), and conjunction elimination (∨E). For details about these rules see forall x: Calgary Remix.

The use of explosion may make this not an answer, but the OP does say that "Contradiction intro,elim" are permitted. Because of that, I am assuming explosion is also permitted. If not, it provides another illustration how one might proceed with the addition of the explosion rule.

References

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/

• "Contradiction Elimination" is an alias for "Explosion" -- See "Rules for Cambridge". Also ... Tip: You are able to explode immediately to A v D, without needing to go through A. – Graham Kemp Aug 22 '18 at 1:40
• Good observation about "contradiction elimination" being an alias for "explosion". You are right about not needing lines 12 and 17. @GrahamKemp – Frank Hubeny Aug 22 '18 at 1:52