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

Question

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)

• Contradiction intro,elim

• = intro, elim

Answer 1

|  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).

Answer 2

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

Answer 3

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/