3

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

3
|  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
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
1

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.

enter image description here


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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.