3

I'm having trouble proving the following using natural deduction:

(T > E) ^ (A > L) /... (T v A) > (E v L)

I checked the answer but I didn't quite understanding the reason why the proof progressed in a certain way (example, at some point the book used addition but I didn't understand why).

Would anyone mind walking me through this? Thank you!

The permitted rules are found here: https://www.cse.iitk.ac.in/users/cs365/2012/rulesLogic.html

The only exception is that absorption is not allowed and constructive dilemma is allowed (but I doubt that will apply to this case).

Improve this question
2
  • 1
    You sure constructive dilemma (aka proof by cases) is allowed? Because it looks to me like this is the proof of that very inference rule.
    – Canyon
    Commented May 22, 2018 at 18:21
  • Yes it's allowed, however since we have to directly prove it by starting from only the premise (T > E) ^ (A > L), it can't be immediately applied. But I agree this is clearly an exercise to prove the CD.
    – anonymous
    Commented May 22, 2018 at 19:04

2 Answers 2

Reset to default
5

Premise :

0) (T⇒E) ∧ (A⇒L).

Use Material Implication on the premise to get :

1) (~T∨E) ∧ (~A∨L)

Use Simplification to get respectively :

2) (~T∨E)

and :

3) (~A∨L)

Using Addition on 2) get :

4) (~T∨E) ∨ L

Using Association :

5) ~T ∨ (E∨L)

Using Addition on 3) get :

6) (~A∨L) ∨ E

Using Association :

7) ~A ∨ (L∨E)

and using Commutation :

8) ~A ∨ (E∨L)

Using Conjunction on 5) and 8) get :

9) [~T ∨ (E∨L)] ∧ [~A ∨ (E∨L)]

Use Distribution to get :

10) (~T ∧ ~A) ∨ (E∨L)

Use De Morgan to get :

11) ~(T∨A) ∨ (E∨L)

Use Material imlication again to get :

12) (T∨A) ⇒ (E∨L).

Improve this answer
2

I used Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker associated with the textbook by P. D. Magnus, Tim Button, J. Robert Loftis, Aaron Thomas-Bolduc, Richard Zach, forall x: Calgary Remix, to obtain the following proof.

enter image description here

The conjunction in the premise on line 1 is eliminated in lines 2 and 3.

A conditional is attempted by assuming the antecedent, T ∨ A, in a sub-proof on line 4.

The disjunction in line 4 is eliminated in line 11 by considering the two cases, one for T, lines 5 to 7, and one for A, lines 8 to 10. In both cases a disjunction was introduced to get the desired consequent, E ∨ L, on lines 7 and 10.

Since both cases produced the desired consequent, E ∨ L, the conditional can be introduced in line 12 which completes the proof.

Improve this answer
3
  • 1
    I'm wondering if this solver should be posted somewhere here under community wiki answer. It'd greatly reduce the number of homework questions regarding logic.
    – rus9384
    Commented Jun 20, 2018 at 14:03
  • @rus9384 It is licensed under a GNU General Purpose License v3 with source code available. Kevin Klement writes in the README: "To install, put the entire contents of this repository into a directory served to the web. It requires that your web server runs PHP 7."
    – Frank Hubeny
    Commented Jun 20, 2018 at 14:08
  • Also, it is not a solver, it is a checker.
    – Graham Kemp
    Commented Oct 22, 2019 at 3:21

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .