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

  • 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 May 22 '18 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 May 22 '18 at 19:04

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


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.

  • 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 Jun 20 '18 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 Jun 20 '18 at 14:08
  • Also, it is not a solver, it is a checker. – Graham Kemp Oct 22 '19 at 3:21

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.